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
Lt(a, b)Exact expansion
exists h. h + S a = bThis 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
none
Used by conservative definitions
PD0022 BoundedQRes PD0051 FloorSqrt PD0025 InjectivePrefix PD0028 AllPrime PD0029 Sorted PD0014 Product PD0019 Repeat PD0007 DivRem PD0024 BoundedPrefix PD0026 SurjectivePrefix PD0027 ContainsPrefixAll transitive conservative prerequisites
none
Used by theorem statements or local proof propositions
TS0009 prime_mod_four_one_bounded_divisible_two_square_norm_exists TS000A positive_multiple_below_twice_equals_base TS000B bounded_divisible_two_square_norm_equals_prime TS000E prime_floor_square_strictly_below_prime TS000F prime_floor_bounded_coordinate_square_strict TS000G two_strict_values_sum_below_double 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 TS000L finite_bounded_into_oversized_not_injective TS000M floor_square_oversized_bounded_grid_not_injective TS000N finite_bounded_into_collision_from_constructive_decision TS000O finite_prefix_collision_succ TS000P finite_prefix_last_occurrence_collision TS000Q finite_prefix_injective_extend_fresh TS000R finite_prefix_collision_or_injective TS000S finite_bounded_into_oversized_collision TS000T floor_square_oversized_bounded_grid_collision TS000U affine_grid_point_remainder_exists TS000V beta_affine_residue_grid_extend TS000W beta_affine_residue_grid_exists TS000X beta_affine_residue_grid_bounded TS000Y prime_floor_affine_residue_grid_exists TS000Z prime_floor_affine_residue_grid_collision TS001E flat_square_index_row_not_at_least_width TS001F flat_square_index_row_below_width TS001H nonzero_coordinate_pair_has_positive_square_norm TS001I distinct_flat_indices_have_positive_difference_norm TS001J strict_successor_coordinate_bound_is_weak_bound 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_squares TS002J beta_two_square_prefix_drop_last TS002K beta_witnessed_two_square_prefix_implies_pointwise TS002L beta_two_square_prefix_last_represented TS002M beta_two_square_represented_factor_product TS002N beta_witnessed_two_square_factor_product TS002P beta_all_prime_entry_is_prime TS002Q beta_admissible_prime_factor_product_is_two_square TS002R represented_factor_product_times_square_is_two_square TS002S beta_grouped_prime_square_factor_product_is_two_square TS002U beta_two_square_prefix_append_equal_pair TS002Y positive_double_at_least_two TS002Z even_positive_prime_valuation_has_square_divisor TS003C all_bad_prime_even_two_square_sufficiency_bounded TS003S prime_square_times_nonzero_strictly_increases TS003T three_mod_four_prime_two_square_norm_valuation_even_boundedGrand-campaign planning vocabulary
Locate Lt in the global campaign vocabulary →
Reviewed Lt corresponds to blueprint Lt 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.