sub_a
plain-language theorem explainer
Componentwise subtraction on the integer part of the golden ring ℤ[φ]: the a-coordinate of x − y equals a(x) − a(y). Algebraists working the choice-free T6 re-derivation cite it as a simp lemma when expanding differences. The proof rewrites subtraction as addition of the additive inverse, then closes by the component simp set and ring on ℤ.
Claim. For all $x, y$ in the golden ring $\mathbb{Z}[\varphi]$ (pairs of integers representing $a + b\varphi$), the integer part of the difference satisfies $(x - y)_a = x_a - y_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)$ standing for $a + b\varphi$, with multiplication reduced by the relation $\varphi^2 = \varphi + 1$. The goal is a sigma0 (choice-free) derivation: only elementary integer arithmetic, with axiom closure inside ${propext, Quot.sound}$.
Subtraction on this structure is defined via the additive group law as $x - y := x + (-y)$. The two projections $a$ and $b$ are the structure fields. Component lemmas such as this one make ring identities on $\mathbb{Z}[\varphi]$ reduce to ordinary ring goals on $\mathbb{Z}$.
Upstream, the carrier is the extensional structure GoldenInt with fields $a,b : \mathbb{Z}$. No continuum or square-root carrier appears in this layer; the display bridge to real $\varphi$ lives in a separate sigma1 module.
proof idea
Term/tactic hybrid, four lines. First rewrite the goal by unfolding subtraction: show $(x + (-y)).a = x.a - y.a$. Then golden_simp expands the $a$-component of addition and negation to the corresponding integer operations. The residual equality on $\mathbb{Z}$ is closed by ring. Marked @[simp] so downstream component expansions fire automatically.
why it matters
Feeds golden_factorization, which states that $(x - \varphi)(x - \psi) = x^2 - x - 1$ inside $\mathbb{Z}[\varphi]$. That factorization is the algebraic heart of the choice-free T6 node: the golden polynomial has exactly the two roots $\varphi$ and $\psi$ in this ring, proved without Classical.choice or real square roots.
In the Recognition forcing chain, T6 forces $\varphi$ as the self-similar fixed point. The DeltaSpine program re-derives that node at sigma0 so the continuum tax is paid only at the display boundary. Component simp lemmas like this one keep the factorization proof a pure ext; simp only [...]; ring script, matching the module's tactic-hygiene constraints.
No open scaffold: the theorem is fully proved and sits in the elementary ring layer beneath the positivity and uniqueness arguments for $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.