PD0002

Lt(a,b)

Witness-defined strict order on natural numbers.

Conservative notation; not a theorem, primitive, or axiom.

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.

Definition in prerequisite notation

S a ≤ b

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
exists h. h + S a = b

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

none — first-order arithmetic only

Definitions depending on this notation

GProperNormDivisor(d,z,N)GStrictNonunitFactorization(z,N,a,b,A,B)GProductSteps(b,c,h,e,l)GAllIrreducible(b,c,l)GAllPrime(b,c,l)GFactorAssociateMatching(b,c,d,e,u,v,l)BoundedPrefix(b,c,l)InjectivePrefix(b,c,l)SurjectivePrefix(b,c,l)

Checked theorems using this definition

GF0052 · gaussian_division_divisible_remainder_zeroGF0053 · gaussian_divides_decidableGF0064 · gaussian_gcd_bezout_bounded_existsGF006E · gaussian_search_signed_code_boundGF0071 · gaussian_search_no_index_below_zeroGF0072 · gaussian_search_two_le_nonzero_not_oneGF0074 · gaussian_proper_norm_divisor_decidableGF0075 · gaussian_factor_search_coordinate_rowGF0076 · gaussian_factor_search_coordinate_rectangleGF0078 · gaussian_factor_search_completeGF0079 · gaussian_search_nonunit_norm_twoGF007A · gaussian_search_norm_factors_strictGF007B · gaussian_nonunit_factor_is_proper_norm_divisorGF007D · gaussian_proper_norm_divisor_splitGF0082 · gaussian_nonunit_divisor_strict_quotientGF0083 · gaussian_irreducible_factor_reductionGF0088 · gaussian_product_prefix_recodeGF008A · gaussian_product_successor_introGF0091 · gaussian_all_irreducible_appendGF0093 · gaussian_factorization_append_irreducibleGF0094 · gaussian_irreducible_factorization_bounded_normGF009F · gaussian_irreducible_divisor_product_memberGF00A0 · gaussian_product_replace_balanceGF00A1 · gaussian_product_replace_balance_iffGF00A2 · gaussian_product_swap_last_invariantGF00A8 · gaussian_factor_matching_appendGF00A9 · gaussian_factor_matched_appendGF00AA · gaussian_factor_swap_all_irreducibleGF00AB · gaussian_factor_matching_unswapGF00AC · gaussian_factor_matched_unswap_existsGF00AD · gaussian_factor_swap_length_transportGF00AE · gaussian_factor_swapped_product_existsGF00AF · gaussian_irreducible_products_associate_unique