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

ArithPositiveEqual(F,G,N)ArithTable(N,F)SignedZeroWindow(F,k,l)DirichletPrefix(F,G,n,l,M)DirichletTable(N,F,G,H)KroneckerDeltaTable(N,E)MultiplicativePrefix(N,F)SignedIncidenceFlatPrefix(A,r,s,M,l,T)DirichletCoprimeProductData(N,F,G,m,n,A,B,T,Q,r,s)

Checked theorems using this definition

MX0004 · signed_multiplicative_coprime_productMX0005 · signed_multiplicative_introMX0008 · signed_multiplicative_restrictMX0009 · signed_multiplicative_product_values_existMX000A · signed_positive_table_entry_transportMX0010 · coprime_divisor_factor_pair_boundsMX0011 · coprime_divisor_factor_pair_exists_uniqueMX0012 · coprime_divisor_factor_pair_cofactorsMX0021 · signed_cartesian_flat_prefix_zeroMX0022 · signed_cartesian_flat_prefix_appendMX0023 · signed_cartesian_flat_prefix_existsMX0024 · signed_cartesian_product_from_flat_prefixMX0026 · signed_cartesian_product_existsMX002D · signed_cartesian_quotient_row_boundMX0040 · signed_support_incidence_flat_prefix_appendMX004F · dirichlet_multiplicative_pair_factorizationMX0050 · dirichlet_multiplicative_pair_entryMX0052 · dirichlet_coprime_grid_support_preservingMX0054 · dirichlet_coprime_grid_support_coveringMX0056 · dirichlet_coprime_product_data_constructMX0057 · dirichlet_convolution_multiplicative_values