neg_a
plain-language theorem explainer
On the golden ring ℤ[φ], negation acts componentwise on the integer part: the a-coefficient of −x is −(a-coefficient of x). Downstream positivity trichotomy, exclusivity of IsPos, and the real embedding all rewrite through this lemma. The proof is pure definitional equality (rfl).
Claim. For every $x=(a,b)\in\mathbb{Z}[\varphi]$ (representing $a+b\varphi$), the integer coefficient of $-x$ equals $-a$.
background
The module rebuilds the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi]$ rather than $\mathbb{R}$. Elements are pairs $(a,b)$ of integers standing for $a+b\varphi$, with multiplication folded through the relation $\varphi^2=\varphi+1$. The goal is a sigma0 (choice-free) derivation: only {propext, Quot.sound}, no Classical.choice.
GoldenInt is the structure with fields a (integer part) and b ($\varphi$-coefficient). Negation, addition, and multiplication are defined on those components; the present lemma is the a-projection of negation. Companion component lemmas (neg_b, add_a, mul_b, …) form the restricted simp set used throughout the module, because full simp is banned as choice-contaminated.
proof idea
One-line definitional proof: rfl. Negation on GoldenInt is defined by negating each integer field, so the a-component equality holds by construction. Marked @[simp] so later rewrites can fire it under the module's restricted simp-only discipline.
why it matters
This is plumbing for the choice-free T6 spine. It is used inside isPos_not_neg (positivity exclusive with negativity) and isPos_trichotomy (exactly one of IsPos x, x=0, IsPos(-x)), both of which rewrite (-x).a when transporting the PosPair predicate across negation. The display bridge toReal_neg in GoldenIntReal also simp-only's this lemma to show the real embedding intertwines negation.
Together with the rest of the component simp set, it keeps every ring identity and positivity argument inside elementary integer arithmetic, so the unique-positive-root statement for $\varphi$ never leaves sigma0. That is the Delta Forcing Spectrum target for the T6 node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.