PD0002

Lt(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 strict order on natural numbers.

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

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

DivRem(n,d,q,r)BoundedNonzeroInverse(m,a)FpElement(p,a)CanonicalModularResidue(m,a,r)FpAdd(p,a,b,c)FpMul(p,a,b,c)FpFieldLaws(p)FpZeroExtendedInv(p,a,b)FpAddPrefix(p,b,c,l)FpMulPrefix(p,b,c,l)FpNegPrefix(p,b,c,l)FpInvPrefix(p,b,c,l)IdentityMatrixSelector(b,c,l)FpCardinality(p,b,c)FpUnitSteps(p,b,c,n)FpCharacteristic(p)

Checked theorems using this definition

FP0002 · prime_field_zero_below_primeFP0003 · prime_field_residue_reflexiveFP0006 · prime_field_residue_bounded_valueFP0008 · prime_field_add_existsFP000A · prime_field_add_exists_uniqueFP000C · prime_field_multiply_existsFP000E · prime_field_multiply_exists_uniqueFP0014 · prime_field_add_zero_rightFP0015 · prime_field_add_zero_leftFP0016 · prime_field_multiply_one_rightFP0017 · prime_field_multiply_one_leftFP0018 · prime_field_multiply_zero_rightFP0019 · prime_field_multiply_zero_leftFP001B · prime_field_negate_existsFP001D · prime_field_negate_exists_uniqueFP001E · prime_field_inverse_existsFP0020 · prime_field_inverse_exists_uniqueFP0024 · prime_field_nonzero_coprimeFP0029 · prime_field_positive_below_modulus_not_zeroFP002B · prime_field_add_grid_value_existsFP002C · prime_field_multiply_grid_value_existsFP002D · prime_field_zero_extended_inverse_existsFP002F · prime_field_add_prefix_choiceFP0030 · prime_field_multiply_prefix_choiceFP0031 · prime_field_negate_prefix_choiceFP0032 · prime_field_inverse_prefix_choiceFP0038 · prime_field_add_grid_value_lookupFP0039 · prime_field_add_table_lookupFP003B · prime_field_multiply_grid_value_lookupFP003C · prime_field_multiply_table_lookupFP003E · prime_field_negate_table_lookupFP0040 · prime_field_inverse_table_lookupFP0042 · prime_field_add_table_commutativeFP0043 · prime_field_add_table_associativeFP0044 · prime_field_multiply_table_commutativeFP0045 · prime_field_multiply_table_associativeFP0046 · prime_field_inverse_table_zeroFP0047 · prime_field_inverse_table_nonzeroFP0048 · prime_field_left_table_distributiveFP0049 · prime_field_right_table_distributiveFP004A · prime_field_enumeration_valueFP004D · prime_field_unit_trace_recodeFP004E · prime_field_unit_trace_successorFP0050 · prime_field_unit_trace_result_boundedFP0051 · prime_field_unit_trace_exists