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

CornacchiaRoot(p,z)CornacchiaStateInvariant(p,z,a,r,u,t)CornacchiaTransitionAt(p,h,e,i)CornacchiaEuclideanRun(p,a,r,u,t,R,T,h,e,l)

Checked theorems using this definition

CN0002 · cornacchia_prime_square_strictly_aboveCN0003 · cornacchia_prime_square_comparisonCN0004 · cornacchia_division_quotient_nonzeroCN0006 · cornacchia_above_threshold_remainder_nonzeroCN000A · cornacchia_coefficient_square_below_primeCN0010 · cornacchia_stopping_state_represents_primeCN0013 · cornacchia_root_existsCN0016 · cornacchia_invariant_euclidean_stepCN0017 · cornacchia_invariant_stop_correctCN0018 · cornacchia_stopped_traceCN0019 · cornacchia_stopped_trace_existsCN001A · cornacchia_trace_extendCN001B · cornacchia_complete_from_invariant_up_to