phi
plain-language theorem explainer
The golden ratio sits in the golden ring as the pure coefficient element 0 + 1·φ. Anyone citing the choice-free T6 re-derivation over ℤ[φ] uses this constant as the distinguished generator. The body is the structure constructor on the integer pair (0, 1).
Claim. Let $\mathbb{Z}[\varphi]$ be the golden ring of pairs $(a,b)$ standing for $a + b\cdot\varphi$. Define $\varphi := (0,1)\in\mathbb{Z}[\varphi]$, i.e. the pure $\varphi$-coefficient unit $0 + 1\cdot\varphi$.
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, read as $a + b\cdot\varphi$, with multiplication folded through the relation $\varphi^2 = \varphi + 1$. The point is sigma0 (choice-free) arithmetic: ring laws reduce to ring on $\mathbb{Z}$, and positivity is a decidable integer predicate, so no continuum or classical choice enters the derivation.
GoldenInt is exactly that carrier: a structure with integer part $a$ and $\varphi$-coefficient $b$. The present definition names the generator itself inside the ring. The conjugate root $\psi = 1 - \varphi$ is introduced immediately afterward in the same style. The continuum bridge (toReal, matching the classical $\varphi$) is deferred to a separate sigma1 display module.
proof idea
Pure definitional construction. The value is the structure literal $\langle 0, 1\rangle$, so the integer part is $0$ and the $\varphi$-coefficient is $1$. No lemmas or tactics are involved.
why it matters
T6 in the forcing chain forces $\varphi$ as the unique positive self-similar fixed point of the cost calculus. The classical spine node does this over $\mathbb{R}$ and pays a Classical.choice tax. This constant is the ring-level avatar of that same $\varphi$ inside the delta-forced golden ring, so every subsequent choice-free identity (norm, positivity, uniqueness of the positive root, integral-domain facts) can mention $\varphi$ without leaving $\mathbb{Z}\times\mathbb{Z}$.
It anchors the sigma0 re-derivation program: the axiom closure target is ${propext, Quot.sound}$ only. Downstream display lemmas that recover the real embedding pay the continuum tax once, at the boundary, rather than inside the forcing argument. No used-by edges are recorded yet; the constant is infrastructure for the rest of the GoldenInt development (conjugates, component arithmetic, T6 delta-forced statement).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.