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

BoundedPrefix(b,c,l)InjectivePrefix(b,c,l)SurjectivePrefix(b,c,l)Product(b,c,l,z)AllPrime(b,c,l)FactorListMatching(b,c,d,e,u,v,l)DivRem(n,d,q,r)

Checked theorems using this definition

AF0004 · foundation_prime_factor_list_existsAF0005 · factor_permutation_below_zero_impossibleAF0006 · factor_permutation_prefix_reflectAF0007 · factor_permutation_all_prime_entryAF000C · factor_permutation_prime_memberAF000E · factor_permutation_index_extendAF000F · factor_permutation_matching_appendAF0010 · factor_permutation_matched_appendAF0011 · factor_permutation_matched_append_existsAF0012 · factor_permutation_swap_reflect_unchangedAF0013 · factor_permutation_swap_bijectionAF0014 · factor_permutation_swap_all_primeAF0015 · factor_permutation_swap_factorizationAF0016 · factor_permutation_swapped_factorization_existsAF0017 · factor_permutation_matching_unswapAF0018 · factor_permutation_matched_unswap_existsAF0019 · prime_factor_lists_matching_by_length