le_add_left_iff
plain-language theorem explainer
Left translation by a fixed signed orbit preserves the internal order: c+a ≤ c+b if and only if a ≤ b. Anyone building ordered arithmetic on signed orbits cites this for cancellation and interval arithmetic. The proof reduces both sides to integer comparison via toInt, then finishes by omega on ℤ.
Claim. For signed orbits $a,b,c$ (each a pair of distinction naturals interpreted as $\mathrm{pos}-\mathrm{neg}$), one has $c+a \le c+b$ if and only if $a \le b$, where $\le$ means the difference is nonnegative.
background
SignedOrbit is the K4.6 carrier for integer-like differences: a pair (pos, neg) of distinction naturals with intended meaning pos − neg. Addition is componentwise on the two legs; add_toInt records that this matches ordinary integer addition after the toInt embedding.
The internal order le is defined by nonnegativity of the difference: a ≤ b means nonneg (b − a). The bridge lemma le_iff_toInt_le equates this with the standard order on the embedded integers a.toInt ≤ b.toInt. Upstream, ArithmeticFromLogic.le is the corresponding existential order on bare logic naturals (∃ k, n+k = m), which feeds the nonnegative flag used here.
This module assembles the ordered-ring surface for signed orbits inside Primitive Recognition Calculus, so translation invariance is a basic structural fact before certificates close the API.
proof idea
Rewrite both occurrences of SignedOrbit.le with le_iff_toInt_le, turning the biconditional into a comparison of integers. Rewrite both sums with add_toInt, so the claim becomes c.toInt + a.toInt ≤ c.toInt + b.toInt ↔ a.toInt ≤ b.toInt. Close with omega on ℤ.
why it matters
Feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas (truncated subtraction, leq flags, absdiff, signed nonnegativity) so downstream foundation code can treat signed-orbit order as a finished API rather than an open construction.
In the Recognition stack this sits under Foundation arithmetic rebuilt from logic, before mass ladders and forcing-chain physics. It is ordinary ordered-group hygiene, not a T0–T8 landmark, but without left-invariance the certificate cannot honestly claim a closed order surface. Sibling facts (reflexivity, transitivity, totality, trichotomy, sign-flag exclusivity) complete the same package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.