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)DirichletPrefix(F,G,n,l,M)DirichletTable(N,F,G,H)SignedZeroWindow(F,k,l)ArithPositiveEqual(F,G,N)DirichletFlatPrefix(F,G,H,n,l,T)DirichletGrid(F,G,H,n,T)DirichletFactorRow(F,G,H,n,a,V)

Checked theorems using this definition

DF000B · dirichlet_grid_flat_prefix_appendDF000F · dirichlet_grid_table_lookupDF0015 · dirichlet_grid_row_sliceDF0016 · dirichlet_grid_column_sliceDF0019 · dirichlet_factor_row_sum_productDF001A · dirichlet_factor_row_nested_entryDF001B · dirichlet_grid_row_sums_convolution_prefixDF001C · dirichlet_grid_column_sums_convolution_prefixDF001D · dirichlet_convolution_fubini_interchangeDF001E · dirichlet_convolution_associative