PD0001

Le(a,b)

Witness-defined non-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

a ≤ b

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

Hygienic expanded first-order definition 
exists h. h + 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

ArithTable(N,F)Squarefree(n)MobiusTable(N,M)DivisorMask(F,n,l,M)ArithPositiveEqual(F,G,N)MobiusPositiveValues(N,F)

Checked theorems using this definition

MC000B · divisor_prime_toggle_boundedMC0011 · mobius_divisor_mask_actual_valueMC0012 · mobius_divisor_mask_prime_toggle_negatesMC0016 · mobius_divisor_mask_prime_factor_sum_zeroMC0017 · mobius_divisor_sum_nonunit_value_zeroMC0018 · mobius_divisor_sum_nonunit_zeroMC001A · mobius_divisor_sum_cancellationMC001C · mobius_divisor_sum_cancellation_on_positive_values