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

Horner(b,c,x,ell,z)CanonicalHornerLift(b,c,l,m,a,M,r)HornerCoefficientBlend(pb,pc,nb,nc,gb,gc,h,l)SignedDerivativeUnit(p,dp,dn)CanonicalSignedHornerLift(pb,pc,nb,nc,l,m,a,M,r)Product(b,c,l,z)Repeat(b,c,a,l)

Checked theorems using this definition

HL0002 · hensel_coprime_mod_transportHL0003 · hensel_canonical_residue_existsHL0004 · hensel_lift_digit_boundHL0005 · hensel_canonical_lift_digit_decomposeHL0007 · hensel_lift_correction_of_rootHL0008 · hensel_canonical_horner_lift_exists_uniqueHL0009 · beta_horner_simple_canonical_representativeHL000A · beta_horner_simple_root_hensel_lift_exists_uniqueHL000E · hensel_canonical_horner_root_exists_uniqueHL0012 · beta_horner_hensel_iterated_exists_uniqueHL0014 · beta_horner_coefficient_blend_existsHL0025 · hensel_prime_blended_nonzero_derivative_is_unit