add_neg
plain-language theorem explainer
Negation distributes over addition on signed orbit differences: the negative of a sum equals the sum of the negatives. Anyone building integer or mediant arithmetic on distinction orbits cites this as a simp rule. The equality is definitional, discharged by reflexivity.
Claim. For signed orbits $a,b$ (each a pair of distinction naturals meaning $\mathrm{pos}-\mathrm{neg}$), $-(a+b)=(-a)+(-b)$.
background
In the primitive recognition calculus, a signed orbit is a pair of distinction naturals (pos, neg) with intended meaning $\mathrm{pos}-\mathrm{neg}$. It is the local stand-in for an integer before quotienting by the usual equivalence of differences.
Addition of signed orbits is componentwise on the positive and negative parts (inherited from the orbit arithmetic layer). Negation swaps the two components, matching the pattern used for logic integers (-(a,b)=(b,a)), intervals (-[a,b]=[-b,-a]), and logic rationals.
The module sits under Foundation and imports orbit and orbit-arithmetic primitives so that integer-like and rational-like constructions can be grown from recognition distinctions rather than assumed as primitives.
proof idea
One-line wrapper: the goal is definitionally true from the componentwise definitions of add and neg on signed orbits, so rfl closes it. No lemmas are applied.
why it matters
This simp lemma keeps signed-orbit arithmetic coherent when signs flip under sums. Downstream it is used in the mediant density argument ltQ_mediant (ratio-orbit growth), where simp unfolds add_neg while comparing mediants in the signed-orbit order. It also supports the integer coefficients of PhiInt in the $\mathbb{Z}[\varphi]$ ring (pairs $a+b\varphi$), which is the algebraic home of the golden-ratio ladder forced at T6. Without distributivity of negation over addition, the signed difference calculus cannot feed cleanly into $\varphi$-ring arithmetic or mediant comparisons on the recognition ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.