sub_zero_balanced
plain-language theorem explainer
Subtracting the zero signed orbit leaves a representative balanced with the original: a − 0 ∼ a under the internal PRC integer relation. Order and comparison lemmas cite it to erase trivial subtractions of zero. The proof rewrites balance to integer equality, applies the toInt laws for sub and zero, and finishes by omega.
Claim. For every signed orbit $a$, the difference $a - 0$ is balanced with $a$: writing $a = (p,n)$ for positive and negative orbit lengths, $(a-0).\mathrm{pos} + a.\mathrm{neg} = a.\mathrm{pos} + (a-0).\mathrm{neg}$. Equivalently, $(a-0)^{\mathbb{Z}} = a^{\mathbb{Z}}$ under the verifier integer display.
background
In the Primitive Recognition Calculus, integers are not postulated as a primitive type. A SignedOrbit is a pair of distinction-natural lengths (pos, neg) with intended meaning pos − neg. Two signed orbits are related by the internal balance predicate when a.pos + b.neg = b.pos + a.neg (K4.9): this is the PRC integer equivalence, defined entirely on δ-orbit positions.
The bridge to ordinary integers is the verifier display toInt. Upstream, balanced_iff_toInt_eq states that balance holds exactly when the two displays agree as elements of ℤ. Subtraction and zero are likewise tied to ℤ by sub_toInt ((a−b).toInt = a.toInt − b.toInt) and zero_toInt (0.toInt = 0).
This module builds the order surface on those signed orbits. Balance is the congruence used to transport inequalities and comparisons, so identities such as a − 0 ∼ a are the elementary rewrites that keep the order API free of spurious zero subtractions.
proof idea
Term-mode proof by rewriting, then linear arithmetic. First apply balanced_iff_toInt_eq to turn the goal into equality of integer displays. Then rewrite with sub_toInt and zero_toInt, reducing to a.toInt − 0 = a.toInt. Close with omega. No case splits and no classical choice.
why it matters
This is the zero-subtraction unit law for the signed-orbit balance relation. Downstream it feeds the left/right congruence forms le_sub_zero_left_iff, le_sub_zero_right_iff, lt_sub_zero_left_iff, lt_sub_zero_right_iff, and the comparison identities cmp_sub_zero_left / cmp_sub_zero_right, each of which erases − 0 inside the order or cmp API.
Those lemmas sit under integer_order_certificate, whose doc-comment records that "the internal signed-orbit order surface is closed." Closing that surface is part of the foundation layer that later supports ledger forcing and the Recognition Composition Law chain; without a proved a − 0 ∼ a, order transport across trivial differences would remain scaffolding.
No open hypothesis is discharged here: the claim is fully proved and purely algebraic on the PRC integer model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.