add_lt_add_left
plain-language theorem explainer
Left addition by a fixed signed orbit preserves strict order: if a < b then c+a < c+b. Ordered-arithmetic developments on the primitive recognition integer layer cite this monotonicity. The proof is a one-line reverse application of the left-addition order equivalence.
Claim. Let $a,b,c$ be signed orbits (pairs of distinction naturals read as differences). If $a < b$ in the internal strict order (nonnegative unbalanced difference), then $c+a < c+b$.
background
Signed orbits are the integer layer of the primitive recognition calculus: a structure with nonnegative distinction-natural components pos and neg, intended as the difference pos − neg. Strict order on them is defined internally as the weak order together with unbalancedness (nonnegative difference that is not zero).
This module builds the ordered arithmetic surface on that type. The key upstream fact is the biconditional that left addition by any fixed $c$ preserves and reflects strict order; its proof rewrites both sides through the integer embedding of signed orbits and finishes with omega on $\mathbb{Z}$. Related strict orders on LogicNat (existence of a successor gap) and on PRC rationals (positive gap of the difference) sit in the same foundation stack but are not used in the body here.
proof idea
One-line wrapper. Invoke the reverse direction of the already-proved equivalence that $c+a < c+b$ if and only if $a < b$, and feed in the hypothesis $a < b$. No new arithmetic is performed.
why it matters
Contributes a standard ordered-group monotonicity law to the integer-order certificate that declares the signed-orbit order surface closed. Downstream consumers include the binary-reflected Gray-code one-bit step (discrete path inequalities along the cycle) and the neutrino-sector lemmas placing fractional $\Delta m^2_{21}$ and $\Delta m^2_{31}$ predictions inside NuFIT bands, which need ordered comparisons on mass-ladder quantities. In the broader Recognition stack this is hygiene on the integer substrate beneath the phi-ladder mass formula; it does not itself force J-uniqueness, phi, the eight-tick octave, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.