phi_b
plain-language theorem explainer
In the golden integer ring ℤ[φ] ≅ ℤ×ℤ, the second coordinate of φ is definitionally 1. Anyone rewriting componentwise in the choice-free T6 re-derivation cites this as part of the banned-full-simp component lemma set. The proof is pure rfl from the constructor of φ.
Claim. Writing elements of $\mathbb{Z}[\varphi]$ as pairs $(a,b)$ for $a+b\varphi$, the golden unit satisfies $\varphi.b = 1$ (i.e. $\varphi = 0 + 1\cdot\varphi$).
background
This module rebuilds the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi] = \mathbb{Z}\times\mathbb{Z}$, with pairs $(a,b)$ standing for $a + b\varphi$ and multiplication folded through the relation $\varphi^2 = \varphi + 1$. The point is a sigma0 (choice-free) re-derivation: the classical spine node PhiForcing works over $\mathbb{R}$ and pays a Classical.choice tax; here everything is elementary integer arithmetic.
The element $\varphi$ is the pair with first coordinate $0$ and second coordinate $1$. Component projections .a and .b are the two $\mathbb{Z}$-coordinates. A family of @[simp] lemmas (phi_a, phi_b, one_a, mul_a, mul_b, …) exposes those coordinates so later proofs can rewrite with simp only [...] plus ring on $\mathbb{Z}$, never full simp (which would reintroduce choice-tainted Mathlib lemmas).
proof idea
One-line definitional proof: rfl. The constructor of phi sets the second coordinate to 1, so phi.b = 1 holds by reduction.
why it matters
Part of the component-lemma simp set that keeps the whole GoldenInt development inside axiom closure {propext, Quot.sound} (sigma0 DELTA_FORCED). Downstream, golden_factorization uses it explicitly: the identity $(x-\varphi)(x-\psi)=x^2-x-1$ is proved by ext then simp only over the component lemmas including phi_b, followed by ring. That factorization is the algebraic heart of "the golden equation has exactly the two roots $\varphi$ and $\psi$ in $\mathbb{Z}[\varphi]$", the choice-free stand-in for T6 (phi forced as the self-similar fixed point) in the UnifiedForcingChain.
The continuum bridge (toReal phi = PhiForcing.φ) is deferred to GoldenIntReal and pays the sigma1 tax once at the display boundary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.