integer_order_certificate
plain-language theorem explainer
The internal signed-orbit order and absolute-value surface is fully closed as a single certificate. Foundation authors cite it as the Step-1 order package before the kernel first-pass assembly. The proof is a structure inhabitant: each field is discharged by a prior display or order lemma on distinction naturals and signed orbits, with short intro/exact wrappers where needed.
Claim. There is an inhabited Step-1 certificate for internal signed-orbit order and absolute value: truncated subtraction, the Boolean $\le$ predicate, and absolute difference on distinction naturals display as the corresponding operations on $\mathbb{N}$; signed-orbit nonnegativity, absolute value, $\le$, and $<$ display as the integer order on the orbit's integer image; the signed order is reflexive, transitive, antisymmetric up to balanced equivalence, total, and trichotomous; sign flags are exclusive and exhaustive and match zero comparisons; and absolute value, addition, negation, subtraction, and natural scaling respect balanced equivalence with the usual triangle and betweenness laws.
background
In the primitive recognition calculus, integers are not taken as a primitive type. Distinction naturals carry a display map to $\mathbb{N}$. Signed orbits are the internal signed objects; each has an integer image, an absolute value in distinction naturals, and Boolean nonnegativity and negativity flags. Two orbits are balanced when their integer images agree; order and arithmetic are required to be well-defined on that equivalence.
IntegerOrderCertificate packages the Step-1 obligations: display identities (truncated subtraction, $\le$, absolute difference) plus the full signed-orbit order surface (reflexivity, transitivity, balanced antisymmetry, totality, trichotomy, flag laws, congruence of add/negate/sub/scale under balance, and absolute-value comparison lemmas such as the triangle inequality and betweenness).
Upstream work already proves the pieces. Arithmetic-from-logic supplies le_refl and le_trans on logic naturals. The IntegerOrder module supplies the signed-orbit lemmas wired into the certificate: absolute value zero iff balanced to zero, absolute value invariant under balance, abs_add_le_add_abs, abs_le_iff_between, and the full family of flag and congruence facts listed among the siblings.
proof idea
The proof builds one structure value field by field. Display fields are direct assignments: truncated subtraction, Boolean $\le$, and absolute difference via the corresponding DistinctionNat theorems; signed nonnegativity, absolute value, $\le$, and $<$ via the SignedOrbit display iff lemmas.
Order axioms are likewise direct: reflexivity, totality, and trichotomy are named SignedOrbit theorems; transitivity and balanced antisymmetry are one-line intro/exact wrappers around le_trans and le_antisymm_balanced. Sign-flag exclusivity, exhaustiveness, and the zero-comparison characterizations are assigned verbatim.
The long tail is congruence and absolute-value infrastructure: each balanced-congruence obligation for nonneg/negative flags, add, negate, sub (left/right/both), and scaleByNat is an intro followed by the matching SignedOrbit lemma; absolute-value facts (nonzero when not balanced zero, triangle inequality, betweenness, monotonicity) are the same pattern. No new arithmetic is invented here; the certificate only aggregates closed lemmas.
why it matters
This declaration is the closed order surface required before the kernel can claim a first-pass certificate. Downstream, kernel_first_pass_certificate (doc: "K7/A2. The first-pass kernel certificate is inhabited") wires judgment surface, trace logic, and related packages; the integer-order certificate is the order half of that foundation stack.
In Recognition Science terms this sits in the Foundation layer that reconstructs arithmetic and order from recognition primitives rather than importing classical $\mathbb{Z}$ as axiomatic. Closing the signed-orbit order (total preorder up to balance, coherent absolute value, display agreement) is a prerequisite for any later comparison, defect, or cost reasoning that talks about internal integers without leaking a verifier-only $\mathbb{Z}$ API.
It does not itself force $\phi$, the eight-tick octave, or $D=3$; those live on the T0–T8 forcing chain. Its job is narrower and earlier: make the internal integer order a proved, citable Prop so kernel and calculus layers can depend on one inhabitant rather than a scattered lemma cloud.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.