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.

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

Sum(b,c,l,z)Repeat(b,c,a,l)BetaPrefixEqual(b,c,d,e,l)CanonicalModularResidue(m,a,r)FpMul(p,a,b,c)BetaZeroExtend(b,c,L,i,a)PolynomialDiagonalPrefix(ab,ac,L,bb,bc,M,i,db,dc,l)FpConvolutionPrefix(p,ab,ac,L,bb,bc,M,cb,cc,l)BetaPrefixInto(b,c,l,B)

Checked theorems using this definition

PC0001 · polynomial_zero_extended_entry_existsPC0003 · polynomial_zero_extended_entry_insidePC0006 · polynomial_diagonal_term_existsPC000D · polynomial_diagonal_prefix_entryPC000F · polynomial_diagonal_prefix_from_pointwisePC0015 · prime_field_convolution_coefficient_boundedPC001B · prime_field_convolution_prefix_entryPC001D · prime_field_convolution_prefix_from_pointwisePC0025 · prime_field_polynomial_convolution_entry