mul_a
plain-language theorem explainer
In the golden ring ℤ[φ], the integer part of a product is a₁a₂ + b₁b₂. Componentwise arithmetic on golden integers cites this as the a-projection of multiplication. Proof is reflexivity: the identity is the definition of Mul on pairs (a,b) ↦ a + bφ with φ² = φ + 1 folded in.
Claim. For $x,y\in\mathbb{Z}[\varphi]$ written $x=a_x+b_x\varphi$ and $y=a_y+b_y\varphi$, the integer coefficient of the product satisfies $(xy)_a = a_x a_y + 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 reduced by the relation $\varphi^2=\varphi+1$. Expanding $(a+b\varphi)(c+d\varphi)$ and collecting the constant term yields $ac+bd$; that is exactly the a-component stated here.
The design goal is sigma0 (choice-free) axiom closure: only {propext, Quot.sound}. Full simp is banned because Mathlib's default simp set pulls choice; instead a hand-curated set of rfl component lemmas (this one among them) plus ring over $\mathbb{Z}$ is used everywhere below.
GoldenInt is the structure with fields a (integer part) and b ($\varphi$-coefficient). Multiplication is defined so that this identity holds definitionally.
proof idea
One-line rfl. The Mul instance on GoldenInt is defined so that the a-field of a product is literally x.a * y.a + x.b * y.b; the theorem is that definitional equality, marked @[simp] for the restricted component simp set.
why it matters
This is a base component lemma for all ring arithmetic in the delta-forced golden ring. Downstream it is used by golden_factorization (the identity $(x-\varphi)(x-\psi)=x^2-x-1$), by the companion b-component lemma, by multiplicativity of the norm $N(a+b\varphi)=a^2+ab-b^2$, and by the bridge toReal_mul that shows the $\mathbb{Z}[\varphi]$ product law is ordinary multiplication in $\mathbb{R}$ once $\varphi^2=\varphi+1$ is restored.
In the Recognition Science forcing chain this supports the sigma0 re-derivation of T6 (φ forced as the self-similar fixed point) without continuum or classical choice. The continuum tax is paid only later, at the display boundary in GoldenIntReal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.