balanced_both_abs_representatives_iff_balanced_zero
plain-language theorem explainer
A signed orbit is balanced against both the positive and negative absolute-value representatives exactly when it is balanced against zero. Order and certificate lemmas in the signed-orbit integer layer cite this biconditional. The proof reduces balance to integer equality via the toInt characterization and finishes with elementary omega arithmetic on absolute values.
Claim. For every signed orbit $z$, $z$ is balanced with the non-negative representative of $|z|$ and with its negation if and only if $z$ is balanced with zero.
background
In Primitive Recognition Calculus, integers are realized as signed orbits: pairs of distinction-natural positions encoding positive and negative legs. Balance of two signed orbits means their internal integer displays agree (balanced_iff_toInt_eq). The absolute value abs of a signed orbit is the distinction-natural absolute difference of its legs; ofOrbit lifts that magnitude back to a non-negative signed orbit, and negate flips sign.
The module builds the order surface on these signed orbits (reflexivity, totality, trichotomy, sign flags). Absolute-value representatives are the natural candidates for the two rays from zero. Upstream, abs_toNat ties the internal absolute value to Int.natAbs of the displayed integer, so vanishing of toInt forces the absolute magnitude to zero.
Locally this lemma is pure bookkeeping: it equates “both rays balance” with “balance at the origin,” which later order certificates treat as the zero case of the signed order.
proof idea
Bidirectional constructor.
Forward: rewrite both balance hypotheses with balanced_iff_toInt_eq, expand ofOrbit_toInt and negate_toInt, then rewrite the goal with zero_toInt. The resulting integer equalities force toInt z = 0 by omega.
Reverse: from balance with zero, obtain toInt z = 0. For each ray, rewrite balance to integer equality and use abs_toNat with Int.natAbs_zero to show the absolute magnitude is zero, so both the positive lift and its negation display as zero; omega closes each conjunct.
why it matters
Feeds three local consumers: the one-direction form balanced_zero_of_both_abs_representatives, its contrapositive not_both_abs_representatives_of_not_balanced_zero, and the package theorem integer_order_certificate (“The internal signed-orbit order surface is closed.”).
In the Recognition foundation stack, integers and their order are not postulated; they are forced from distinction orbits and ledger balance. This biconditional pins the zero case of that order: the only signed orbit that can sit on both absolute rays at once is the balanced origin. That is a necessary hinge for trichotomy, sign-flag exclusivity, and the nonnegativity display lemmas that the certificate exports.
It does not itself invoke the forcing chain T0–T8 or the J-cost, but it is part of the arithmetic substrate those later layers assume when they speak of integer rungs and signed defects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.