psi_a
plain-language theorem explainer
In the golden ring ℤ[φ] ≅ ℤ×ℤ, the conjugate root ψ = 1−φ has first coordinate equal to 1. Anyone simplifying componentwise arithmetic on GoldenInt cites this simp fact. The proof is pure definitional reflexivity from the constructor ψ := ⟨1, −1⟩.
Claim. Writing elements of $\mathbb{Z}[\varphi]$ as pairs $(a,b)$ for $a+b\varphi$, the conjugate root $\psi=1-\varphi$ satisfies $a(\psi)=1$.
background
This module rebuilds the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi]\cong\mathbb{Z}\times\mathbb{Z}$, with pairs $(a,b)$ standing for $a+b\varphi$ and multiplication folded through $\varphi^2=\varphi+1$. The goal is a choice-free (sigma0) re-derivation: only elementary integer arithmetic, no continuum carrier.
The conjugate root is the ring element $\psi:=\langle 1,-1\rangle$, i.e. $1-\varphi$. Its real counterpart in the continuum spine is $(1-\sqrt{5})/2$. Component projections .a and .b are the two integer coordinates; a family of @[simp] reflexivity lemmas exposes them so later proofs can rewrite with simp only rather than full simp (banned here for choice contamination).
proof idea
One-line definitional proof: psi is defined as the pair $\langle 1,-1\rangle$, so the first projection equals $1$ by rfl. No lemmas are applied.
why it matters
Part of the component-lemma simp set that keeps the whole GoldenInt development inside {propext, Quot.sound}. Downstream, golden_factorization uses psi_a (with psi_b, phi_a, phi_b, and the mul/sub component lemmas) to prove $(x-\varphi)(x-\psi)=x^2-x-1$ by ext; simp only [...]; ring. That factorization is the algebraic heart of the sigma0 T6 node: the golden polynomial has exactly the two roots $\varphi$ and $\psi$ inside $\mathbb{Z}[\varphi]$, without invoking $\mathbb{R}$ or Classical.choice. Landmark: T6 phi-forcing, delta-forced over the integer golden ring.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.