phi_a
plain-language theorem explainer
In the golden integer ring ℤ[φ] ≅ ℤ×ℤ, the first coordinate of φ is zero (φ = 0 + 1·φ). Anyone building the choice-free T6 re-derivation cites this as part of the component simp set. The proof is pure definitional equality (rfl).
Claim. Writing elements of $\mathbb{Z}[\varphi]$ as pairs $(a,b)$ for $a+b\varphi$, the golden unit $\varphi$ has first coordinate $a(\varphi)=0$.
background
The module rebuilds the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi]\cong\mathbb{Z}\times\mathbb{Z}$, with carrier pairs $(a,b)$ standing for $a+b\varphi$ and multiplication folded through $\varphi^2=\varphi+1$. The goal is a sigma0 (choice-free) derivation: only ${propext, Quot.sound}$, no continuum and no Classical.choice.
Under that encoding $\varphi$ itself is the pair with $a=0$ and $b=1$. Component projections are exposed as a family of @[simp] lemmas (phi_a, phi_b, one_a, mul_a, sub_a, …) so later algebraic identities can be reduced by simp only plus ring on $\mathbb{Z}$, avoiding the choice-tainted default simp set.
proof idea
One-line definitional proof: rfl. The constant phi is constructed with first component 0, so the equality is judgmental.
why it matters
This lemma is a brick in the component simp set that keeps the whole GoldenInt development inside the sigma0 DELTA_FORCED envelope of the Delta Forcing Spectrum program. Downstream, golden_factorization rewrites (x-φ)(x-ψ)=x²-x-1 by simp only over exactly these component lemmas (including phi_a) and then ring. That factorization is the algebraic heart of the choice-free T6 node: the golden polynomial has precisely the two roots φ and ψ inside ℤ[φ], with no appeal to ℝ or √5 as a real. The continuum bridge is deferred to GoldenIntReal and paid once at the display boundary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.