negate_pos
plain-language theorem explainer
Negating a signed orbit swaps its two legs: the positive component of the result is exactly the original negative component. Anyone simplifying signed-orbit arithmetic in the primitive recognition calculus will hit this simp rule. The proof is pure definitional equality from the swap construction.
Claim. For every signed orbit $a = (p, n)$ (intended value $p - n$), if $\mathrm{negate}(a) = (n, p)$, then the positive leg of $\mathrm{negate}(a)$ equals $n$.
background
In the primitive recognition calculus, integers are built before classical $\mathbb{Z}$ by pairing two distinction-counts. A signed orbit is the structure with fields pos and neg (both DistinctionNat), with intended meaning $\mathrm{pos} - \mathrm{neg}$ (K4.6).
Pointwise negation is the swap map: $\mathrm{negate}(a)$ has positive leg $a.\mathrm{neg}$ and negative leg $a.\mathrm{pos}$. The name negate (not neg) avoids clashing with the structure field. The same swap pattern appears upstream in logic integers, where $-(a,b)=(b,a)$, and in protocol negation on nested real intervals.
This module sits in the foundation layer that reconstructs integer and rational arithmetic from recognition orbits, feeding later cost and ledger constructions.
proof idea
One-line definitional proof. Unfolding negate gives a structure whose pos field is definitionally a.neg, so rfl closes the goal. Marked @[simp] so the rewrite fires automatically in signed-orbit calculations.
why it matters
Tiny but load-bearing simp fact for the signed-orbit API. Without it, every proof that manipulates $\mathrm{negate}$ must manually unfold the structure. It locks the swap convention to the same pattern used for logic-integer negation and protocol negation, keeping the integer reconstruction coherent.
No downstream users are recorded yet in the graph; the lemma is infrastructure for later orbit arithmetic and comparison lemmas in this module (absolute difference, order, toInt). It does not itself touch T0–T8 or the J-cost equation; it only stabilizes the integer layer those later steps sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.