negate_neg
plain-language theorem explainer
After pointwise negation of a signed orbit (swap of its positive and negative distinction counts), the negative field of the result equals the original positive field. Anyone simplifying signed-orbit arithmetic or discharging field projections after negate will cite this simp lemma. The proof is pure definitional reflexivity from the swap.
Claim. Let $a$ be a signed orbit, a pair $(p,n)$ of distinction naturals with intended meaning $p-n$. Define pointwise negation by swapping components: $\mathrm{negate}(a)=(n,p)$. Then the negative component of $\mathrm{negate}(a)$ equals the original positive component $p$.
background
In the primitive recognition calculus, integers are assembled before classical $\mathbb{Z}$ is available. A SignedOrbit (K4.6) is a pair of distinction naturals (pos, neg) whose intended meaning is the difference $\mathrm{pos}-\mathrm{neg}$. Display as an ordinary integer is handled separately by a verifier map toInt.
Pointwise negation is the structure-level swap negate a = ⟨a.neg, a.pos⟩, deliberately named negate rather than neg so it does not collide with the structure field neg. The same swap pattern appears upstream in logic integers (-(a,b)=(b,a)) and in protocol negation on delta-reals; here it is the native signed-orbit version used by the integer/rational layer of PRC.
This module sits on orbit arithmetic and builds the signed difference type that later feeds rational constructions from logic.
proof idea
One-line definitional proof: rfl. Unfolding negate replaces (negate a).neg by a.pos, so the equality is judgmental and needs no lemmas or case splits. The @[simp] attribute exposes that reduction to the simplifier.
why it matters
The lemma is a field-projection companion to the definition of signed-orbit negation in the K4.6 integer layer of Primitive Recognition Calculus. It keeps simp-normal forms tidy when proofs manipulate pos/neg after a swap, parallel to how logic-integer negation swaps pair components.
No downstream theorems currently depend on it in the mirror graph; it is local scaffolding hygiene for the IntegerRational development rather than a forcing-chain landmark (T5–T8, RCL, phi). Its place is bookkeeping: once toInt and arithmetic lemmas are stacked on SignedOrbit, this identity prevents manual field rewrites after every negate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.