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, axiom, predicate constant, or kernel rule. Its expansion remains in the unchanged first-order language.
Definition neighborhood
Depends on conservative definitions
Used by conservative definitions
none
All transitive conservative prerequisites
Used by theorem statements or local proof propositions
TS000E prime_floor_square_strictly_below_prime TS000F prime_floor_bounded_coordinate_square_strict TS000H prime_floor_bounded_two_square_norm_below_double TS000I floor_square_successor_grid_strictly_exceeds_input TS000J floor_square_oversized_grid_exists TS000K prime_floor_bounded_divisible_norm_represents_prime TS000M floor_square_oversized_bounded_grid_not_injective TS000T floor_square_oversized_bounded_grid_collision TS000Z prime_floor_affine_residue_grid_collision TS001M prime_floor_decoded_affine_collision_represents_prime TS001N prime_floor_affine_grid_collision_represents_prime TS001O prime_mod_four_one_is_sum_of_two_squaresGrand-campaign planning vocabulary
Locate FloorSqrt in the global campaign vocabulary →
Reviewed FloorSqrt corresponds to blueprint FloorSqrt with checked argument positions [0, 1].
The global atlas describes planning vocabulary and does not itself certify a definition or theorem. The reviewed expansion and conservative dependency DAG on this page are the actual family-local reading definitions.