Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Readable signature
FloorSqrt(n,s)Exact expansion
((exists bcs_sqrt_lower_gap_bertrand_defined_floor_sqrt. bcs_sqrt_lower_gap_bertrand_defined_floor_sqrt + (s) * (s) = (n)) /\ exists bcs_sqrt_upper_gap_bertrand_defined_floor_sqrt. bcs_sqrt_upper_gap_bertrand_defined_floor_sqrt + S (n) = S (s) * S (s))This node is conservative notation, not a theorem, new axiom, predicate constant, or kernel rule. Its expansion is checked for exact first-order AST equivalence.
Definition neighborhood
Expands using
Used by definitions
none
Used by theorem statements or local proof propositions
BT00R6 floor_sqrt_lower_bound BT00R7 floor_sqrt_strict_upper_bound BT00RA floor_sqrt_total BT00RC floor_sqrt_monotone BT00RI floor_ceil_complement_budget BT00RJ floor_ceil_division_budget BT00X0 floor_sqrt_factorized_threshold_thirty_two BT00X4 bertrand_floor_power_product_le_h_from_total BT00X6 bertrand_main_inequality_factorized_from_total BT00X7 bertrand_main_inequality_factorized BT00X8 bertrand_main_inequality_nat BT00YH floor_sqrt_above_root_power_two_strict BT00YI central_binom_prime_above_floor_sqrt_valuation_le_one BT00YK no_bertrand_central_nonzero_valuation_factor_ranges BT00YL no_bertrand_central_nonzero_contribution_factor_ranges BT00YM no_bertrand_central_prime_contribution_ranges BT0108 no_bertrand_central_contribution_choice_ranges BT010B floor_sqrt_two_le_of_two_lt BT010D floor_sqrt_three_mul_le_double BT010F floor_sqrt_le_third_quotient BT010G floor_sqrt_third_quotient_gap_exists BT010J floor_third_double_gap_package BT010V no_bertrand_small_contribution_choice_le_double BT010W no_bertrand_middle_contribution_choice_le_selector BT010X no_bertrand_high_contribution_choice_eq_one BT010Y no_bertrand_small_contribution_product_le_power BT0110 no_bertrand_middle_contribution_interval_le_primorial_interval BT0111 no_bertrand_middle_contribution_interval_le_four_pow BT0112 no_bertrand_high_contribution_interval_eq_one BT0113 central_binom_factorization_small BT0114 central_binom_le_of_no_bertrand_prime BT0115 bertrand_eventually_closed_upper