balanced_negate_ofOrbit_abs_iff_balanced_zero_of_nonnegFlag
plain-language theorem explainer
For a non-negative signed orbit z, balance of z against the negation of the absolute-value orbit is equivalent to balance of z against zero. Order-certificate and integer-order work cite this to collapse the signed absolute-value case under the nonneg flag. The proof rewrites to the unrestricted disjunction lemma, then kills the negative-flag branch by sign exclusivity.
Claim. Let $z$ be a signed orbit with non-negative flag true. Then $z$ is balanced against the negation of the orbit built from $|z|$ if and only if $z$ is balanced against zero.
background
In the primitive recognition calculus, integers are represented as signed orbits: a pair of distinction counts (positive and negative legs) together with boolean sign flags. The absolute value of a signed orbit is the distinction-nat absolute difference of those legs; ofOrbit lifts that back to a signed orbit, and negation flips the signed presentation.
Balance is the ledger-style equality relation on signed orbits (events cancel). An unrestricted sibling already states that balance of $z$ against $\mathrm{negate}(\mathrm{ofOrbit}(|z|))$ holds exactly when either the negative flag is true or $z$ is balanced against zero. Sign flags are exclusive: non-negative and negative cannot both be true.
This module builds the internal order surface on those signed orbits (reflexivity, totality, trichotomy, flag characterizations of $\le 0$ and $<0$). The present lemma specializes the absolute-value balance identity to the non-negative cone.
proof idea
Term-mode proof. Rewrite the goal by the unrestricted sibling balanced_negate_ofOrbit_abs_iff_negativeFlag_or_balanced_zero, obtaining an iff with the disjunction "negative flag or balanced against zero".
Left-to-right: case-split the disjunction. The negative-flag case is exfalso via signFlags_exclusive against the hypothesis that the non-negative flag is true. The remaining case is exactly balance against zero.
Right-to-left: inject balance-against-zero into the right disjunct (Or.inr).
why it matters
Feeds integer_order_certificate, which packages the closed internal signed-orbit order surface (truncated subtraction, $\le$ display, abs-diff display, and nonneg flag characterizations). Without collapsing negate-of-abs balance to zero-balance on the nonneg cone, the certificate cannot treat absolute value and order as a single coherent integer interface.
In the Recognition foundation stack this sits under ledger forcing and the primitive calculus that later supports the forcing chain (T0–T8). It is pure discrete order algebra: no continuum, no J-cost, no physical constants. It closes one flag-conditioned identity needed so the signed-orbit model behaves like classical $\mathbb{Z}$ under absolute value and sign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.