mul_b
plain-language theorem explainer
The φ-coefficient of a product in ℤ[φ] expands as a_x b_y + b_x a_y + b_x b_y. Anyone proving ring identities, the multiplicative norm, or the golden factorization on the golden integers cites this component lemma. The proof is pure definitional equality from the multiplication law folded through φ² = φ + 1.
Claim. For golden integers $x = a_x + b_x\varphi$ and $y = a_y + b_y\varphi$ in $\mathbb{Z}[\varphi]$, the $\varphi$-coefficient of the product equals $a_x b_y + b_x a_y + b_x b_y$.
background
GoldenInt is the ring $\mathbb{Z}[\varphi]$ realized as pairs $(a,b)$ of integers, standing for $a + b\cdot\varphi$, with multiplication folded through the minimal equation $\varphi^2 = \varphi + 1$. Expanding $(a_x + b_x\varphi)(a_y + b_y\varphi)$ and reducing the $\varphi^2$ term yields integer part $a_x a_y + b_x b_y$ and $\varphi$-coefficient $a_x b_y + b_x a_y + b_x b_y$.
This module is the sigma0 (choice-free) re-derivation of the T6 golden-ratio forcing node: everything is elementary integer arithmetic, with ring laws discharged by ring over $\mathbb{Z}$. Full simp is banned; only a closed set of component rfl-lemmas (including this one) is allowed, via the local golden_simp macro.
proof idea
One-line definitional proof: rfl. The statement is exactly the second projection of the structure-level multiplication on GoldenInt, so both sides are definitionally equal. No lemmas are applied; the equality is by construction of the product law.
why it matters
This is one of the two component projections of multiplication (paired with the integer-part lemma). It sits in the golden_simp set that discharges every CommRing law on GoldenInt by ext; golden_simp; ring.
Downstream it is used by: (1) multiplicativity of the norm $N(a+b\varphi)=a^2+ab-b^2$, which is pure ring after unfolding both components; (2) the golden factorization $(x-\varphi)(x-\psi)=x^2-x-1$ inside $\mathbb{Z}[\varphi]$; (3) the display bridge toReal_mul, which shows the integer product law matches real multiplication because $\varphi^2=\varphi+1$. Together these close the choice-free T6 spine: $\varphi$ is forced as the unique positive root of $x^2=x+1$ without continuum carriers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.