abs_zero_sub_eq
plain-language theorem explainer
For any signed orbit a, the absolute value of zero minus a equals the absolute value of a. Order and certificate authors cite it when reducing |−a| to |a| on the internal integer surface. The proof injects through DistinctionNat.toNat, rewrites to Int.natAbs, and uses |−n| = |n|.
Claim. For every signed orbit $a$ (a pair of distinction-natural positions interpreted as $\mathrm{pos}-\mathrm{neg}$), $\lvert 0 - a \rvert = \lvert a \rvert$, where absolute value is the orbit-level absolute difference and subtraction is the signed-orbit group operation.
background
Signed orbits are the internal model of integers in the primitive recognition calculus: a structure with two distinction-natural coordinates, intended as $\mathrm{pos}-\mathrm{neg}$. The verifier display toInt sends such a pair to $\mathbb{Z}$ by ordinary integer subtraction of the underlying naturals. Absolute value on a signed orbit is the distinction-natural absolute difference of those two coordinates, not a separate signed type.
The companion lemma abs_toNat states that this internal absolute value, read as a natural, equals Int.natAbs of the verifier integer. Subtraction of signed orbits is compatible with toInt (sub_toInt), and zero maps to $0$. The local module builds the order surface on these signed orbits (reflexivity, totality, trichotomy, sign flags) before packaging a closure certificate.
proof idea
Apply injectivity of DistinctionNat.toNat so it suffices to compare underlying naturals. Rewrite both sides with abs_toNat, then replace the left-hand signed orbit by sub_toInt and zero_toInt, obtaining Int.natAbs (0 - a.toInt). A one-line omega step gives $0 - a.toInt = -a.toInt$; finish with Int.natAbs_neg.
why it matters
Feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. Absolute-value identities are part of making the order and nonnegativity displays agree with ordinary integer arithmetic, so the certificate can expose signed_nonneg_display and related flags without a separate absolute-value axiom. In the foundation stack this is bookkeeping on the LogicInt/SignedOrbit bridge (IntegersFromLogic recovery), not a forcing-chain step; it keeps the primitive recognition calculus aligned with $\mathbb{Z}$ before higher RS landmarks (J-cost, phi ladder) are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.