neg_b
plain-language theorem explainer
On the golden ring ℤ[φ], negation acts componentwise on the φ-coefficient: the b-field of −x is −(b of x). Anyone simplifying arithmetic in the choice-free T6 spine cites this as a @[simp] projection lemma. The proof is pure definitional equality (rfl).
Claim. For every $x$ in the golden ring $\mathbb{Z}[\varphi]$ (pairs $(a,b)$ for $a+b\varphi$), the $\varphi$-coefficient of $-x$ equals the negation of the $\varphi$-coefficient of $x$.
background
GoldenInt is the ring $\mathbb{Z}[\varphi]$ realized as pairs $(a,b)\in\mathbb{Z}\times\mathbb{Z}$ for $a+b\varphi$, with multiplication reduced by $\varphi^2=\varphi+1$. The two projections are the integer part $a$ and the $\varphi$-coefficient $b$.
This module rebuilds the T6 golden-ratio forcing node without the continuum or Classical.choice: ring laws are elementary integer arithmetic, positivity is a decidable predicate on $(2a+b,b)$, and the target axiom closure is ${\mathrm{propext},\mathrm{Quot.sound}}$ (sigma0 DELTA_FORCED). Component lemmas such as this one keep simp restricted to local projections so the default Mathlib simp set cannot pull in choice-tainted material.
proof idea
One-line definitional proof: negation on GoldenInt is defined fieldwise, so the $b$-projection of $-x$ is definitionally $-x.b$. Closed by rfl; no lemmas required.
why it matters
Feeds the elementary arithmetic layer of the sigma0 re-derivation of T6 (unique positive root of $x^2=x+1$ inside $\mathbb{Z}[\varphi]$). The parent program is the Delta Forcing Spectrum: keep the forcing chain’s golden fixed point free of Classical.choice, paying the continuum tax only at the display bridge in GoldenIntReal. Small @[simp] projection facts like this keep later ring and positivity arguments inside the allowed tactic set (ring on ℤ, decide, explicit trichotomy, atomic omega).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.