IntegerOrderCertificate
plain-language theorem explainer
Bundles the full internal order and absolute-value surface for signed orbits and distinction naturals into one Prop certificate: display maps match ordinary integers, order is a total preorder with balanced antisymmetry, and multiplication/scaling/subtraction preserve comparison and sign flags. Anyone citing the PRC integer-order layer or the first-pass kernel certificate uses this interface. As a structure definition it has no proof body; the inhabitant is assembled elsewhere field-by-field.
Claim. A proposition packing: (i) truncated subtraction, $\leq$, and absolute difference on distinction naturals agree with the usual $\mathbb{N}$ display; (ii) nonnegativity, absolute value, $\leq$, and $<$ on signed orbits agree with the $\mathbb{Z}$ display; (iii) signed $\leq$ is reflexive, transitive, total, and antisymmetric up to balance, with trichotomy; (iv) sign flags are exclusive and exhaustive and track zero comparisons; (v) add, negate, sub, mul, and scale-by-nat are congruence maps for balance and for order/comparison under the usual sign hypotheses; (vi) reciprocal and cross-equality laws for ratio orbits close the nonzero multiplicative group.
background
Primitive Recognition Calculus builds arithmetic from distinction orbits rather than from a primitive $\mathbb{Z}$. Distinction naturals carry truncated subtraction, boolean $\mathrm{leq}$, and absolute difference; signed orbits add a sign flag pair $(\mathrm{nonnegFlag},\mathrm{negativeFlag})$, absolute value, and internal $\mathrm{le}/\mathrm{lt}/\mathrm{cmp}$. Balance is the ledger-style equality relation on orbits (two representatives count as the same integer when balanced).
Upstream, le/lt on logic naturals are the usual existential-sum orders, toNat/toInt are the recovery maps into Lean's Nat/Int, and internal cmp is defined from balance and the nonnegativity flag of a difference, not from the verifier display. The certificate's job is to assert that the internal surface is closed and that every display lemma needed by later stages is available as a named field.
The module sits in the Foundation forcing stack that eventually feeds the Recognition Composition Law and the T0–T8 chain; here the concern is purely the integer/rational order layer before cost $J$ appears.
proof idea
No proof body: this is a bare structure ... : Prop whose fields are the individual lemmas already proved in the module (reflexivity, trichotomy, flag exclusivity, mul/scale monotonicity under nonnegative nonzero factors, reverse under negative factors, abs-sub triangle inequalities, ratio reciprocal cross-equality to one, cancellation, and the large congruence families for products and differences under balance).
The companion theorem integer_order_certificate fills every field by pointing at the corresponding proved lemma (e.g. DistinctionNat.toNat_truncatedSub, SignedOrbit.nonneg_iff_toInt_nonneg, SignedOrbit.le_trans, and the ratio reciprocal suite). Downstream consumers only need to inhabit the structure once.
why it matters
This is the Step-1 certificate for the internal signed-orbit order surface. The theorem integer_order_certificate asserts that the surface is closed by producing an inhabitant. That inhabitant is then required by KernelFirstPassCertificate (K7/A2), the bundling certificate that every first-pass PRC stage has a concrete Lean object: strength tags, traces, judgments, trace logic, and this integer-order layer.
Without a single Prop packing display fidelity, total preorder laws, sign-flag calculus, and multiplicative congruence, later stages would re-prove dozens of order lemmas ad hoc. The certificate is scaffolding for inevitability, not the inevitability theorem itself: it records that the analytic specification has Lean witnesses, clearing the path toward the forcing chain (T0–T8) once cost and recognition composition are attached.
Parent consumers: integer_order_certificate and KernelFirstPassCertificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.