PD0001

Le(a,b)

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

Witness-defined non-strict order on natural numbers.

Conservative notation; not a theorem, primitive, or axiom.

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)

Checked theorems using this definition

DV0002 · arithmetic_signed_table_equal_entry_transportDV0009 · mobius_table_appendDV000B · mobius_table_lookupDV000C · mobius_table_entry_iffDV000E · mobius_table_extensionalDV000F · mobius_table_restrictDV0013 · divisor_mask_entry_existsDV0018 · divisor_mask_prefix_appendDV0019 · divisor_mask_prefix_existsDV001A · divisor_mask_prefix_extensionalDV001B · divisor_mask_prefix_restrictDV001C · divisor_mask_positive_quotient_entryDV001D · divisor_mask_omitted_entryDV001E · divisor_mask_entry_positive_source_extensionalDV001F · divisor_mask_positive_source_extensionalDV0020 · signed_divisor_sum_existsDV0022 · signed_divisor_sum_exists_unique