sub_b
plain-language theorem explainer
Componentwise subtraction on the φ-coefficient of the golden ring ℤ[φ]: if x = a_x + b_x φ and y = a_y + b_y φ, then the φ-part of x − y is b_x − b_y. Component lemmas and factorization identities in the delta-forced T6 spine cite this as a simp rule. Proof rewrites subtraction as addition of negation, unfolds projections, and closes by ring on ℤ.
Claim. For all $x,y\in\mathbb{Z}[\varphi]$ written $x=a_x+b_x\varphi$ and $y=a_y+b_y\varphi$, the $\varphi$-coefficient of $x-y$ equals $b_x-b_y$.
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: ring laws reduce to ring on $\mathbb{Z}$, and positivity is a decidable integer predicate, so no continuum or classical choice enters the spine.
Subtraction is defined via addition of additive inverse, so the $b$-projection of a difference is not primitive; it must be proved equal to ordinary integer subtraction of the coefficients. Sibling component lemmas (add_a, sub_a, and the zero/one/$\varphi$/$\psi$ constants) form the simp set that keeps later algebraic identities elementary.
proof idea
Rewrite the goal as the $b$-component of $x+(-y)$. The custom golden_simp unfolds addition, negation, and field projections on GoldenInt to integer arithmetic on the coefficients. The residual equality on $\mathbb{Z}$ is discharged by ring. No external lemmas beyond the local component simp set are required.
why it matters
Feeds golden_factorization, which states that $(x-\varphi)(x-\psi)=x^2-x-1$ in $\mathbb{Z}[\varphi]$ and is proved by ext plus simp over the component lemmas including this one. That identity is the algebraic core of the choice-free T6 node: the golden polynomial splits exactly at the two units $\varphi$ and $\psi$ inside the integer ring, without invoking $\sqrt{5}$ over $\mathbb{R}$.
In the Recognition forcing chain, T6 forces $\varphi$ as the self-similar fixed point. This lemma is scaffolding arithmetic for the delta-forced (sigma0) re-derivation of that node, keeping axiom closure inside {propext, Quot.sound} before the continuum bridge is paid once at the display boundary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.