psi_b
plain-language theorem explainer
The φ-coefficient of the conjugate root ψ in ℤ[φ] is definitionally −1. Anyone rewriting componentwise over the golden integers cites this as a simp lemma. The proof is pure rfl from the constructor of ψ.
Claim. If $\psi = 1 - \varphi$ is represented in $\mathbb{Z}[\varphi] \cong \mathbb{Z}\times\mathbb{Z}$ by the pair $(a,b)$ with value $a + b\varphi$, then $b = -1$.
background
This module rebuilds the T6 golden-ratio 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 $\varphi^2 = \varphi + 1$. The goal is a choice-free (sigma0) re-derivation: ring laws by integer arithmetic, no continuum carrier.
The conjugate root is defined as the pair $\psi := \langle 1, -1\rangle$, i.e. $1 - \varphi$. (The parallel real definition $(,1 - \sqrt{5},)/2$ lives only in the display bridge, not here.) Component projections .a and .b are the two integer coordinates; this lemma pins the second coordinate.
Component rfl lemmas form the only allowed simp set in the module. Full simp is banned because the default Mathlib simp set pulls Classical.choice.
proof idea
One-line definitional proof: rfl. Unfolding psi gives $\langle 1, -1\rangle$, so the .b field is definitionally $-1$. No lemmas are applied beyond the constructor.
why it matters
Feeds the componentwise simp set used by golden_factorization, which proves $(x - \varphi)(x - \psi) = x^2 - x - 1$ in $\mathbb{Z}[\varphi]$ by expanding coordinates and ringing over $\mathbb{Z}$. That factorization is the algebraic heart of the choice-free T6 node: the golden polynomial has exactly the two roots $\varphi$ and $\psi$ inside the golden integers.
In the broader Recognition forcing chain, T6 forces $\varphi$ as the self-similar fixed point. This lemma is scaffolding for the sigma0 DELTA_FORCED audit target of the module: every rewrite stays inside {propext, Quot.sound}, with continuum tax deferred to GoldenIntReal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.