balanced_sign_canonical
plain-language theorem explainer
Every signed orbit is balanced against the unique canonical representative built from its absolute value and its sign flag: the nonnegative case matches the positive orbit of |z|, the negative case matches its pointwise negation. Order and integer-certificate proofs cite this to pin the sign-aware normal form. The argument is a two-branch case split on the nonnegative flag, discharging each arm by the corresponding balanced-of-flag lemma.
Claim. For every signed orbit $z$, either $z$ is flagged nonnegative and $z$ is balanced with the signed orbit built from the absolute value $|z|$, or $z$ is flagged negative and $z$ is balanced with the pointwise negation of that same absolute-value orbit. Balance means $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$ on $\delta$-orbit positions.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of distinction-nat positions (pos, neg) rather than classical $\mathbb{Z}$. Two signed orbits are balanced when their orbit lengths match under the internal relation $a.pos + b.neg = b.pos + a.neg$ (K4.9). Absolute value extracts the unsigned magnitude as absDiff of the two legs; pointwise negation swaps pos and neg.
Sign is recorded by Boolean flags nonnegFlag and negativeFlag. The sibling lemmas balanced_of_nonnegFlag and balanced_of_negativeFlag already show that each flag forces balance against the corresponding canonical representative: the positive orbit of $|z|$, or its negation. The present statement packages those two facts into a single exhaustive disjunction.
The surrounding module builds the internal order surface on these signed orbits (reflexivity, transitivity, antisymmetry up to balance, trichotomy, and flag characterizations of $\le 0$ and $< 0$).
proof idea
Case-split on whether nonnegFlag z = true.
- If yes, left disjunct: pair the hypothesis with
balanced_of_nonnegFlag, which rewrites balance to integer equality and usesabs_toInt_of_nonnegFlag. - If no, derive
negativeFlag z = trueby unfolding the negative flag and exhausting the Boolean cases onnonnegFlag(the true branch contradicts the case hypothesis). Right disjunct: pair that withbalanced_of_negativeFlag, which rewrites vianegate_toIntandofOrbit_toInt.
No further arithmetic is needed; the work sits in the two upstream flag-to-balance lemmas.
why it matters
This is the sign-canonical normal-form step for the internal integer order. Downstream it feeds integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed": the certificate bundles display lemmas for truncated subtraction, $\le$, absolute difference, and the nonnegative characterizations, all of which rely on every signed orbit lining up with a unique signed absolute-value representative.
In the Recognition foundation stack this sits under ledger forcing and the primitive recognition calculus that precedes the forcing chain (T0–T8). Balanced ledgers and balanced signed orbits are the same structural idea at two layers: event lists that cancel, and orbit pairs that cancel. Closing the order surface is a prerequisite for treating integers as derived, not postulated, structure inside the calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.