GoldenInt
plain-language theorem explainer
The golden ring ℤ[φ] is the carrier of pairs of integers (a,b) standing for a + b·φ, with the relation φ² = φ + 1 built into multiplication. Anyone working the choice-free T6 re-derivation or the discrete d'Alembert uniqueness spine cites this type. It is a plain structure definition with Zero and One instances, not a proved theorem.
Claim. The golden integers are the set of formal pairs $(a,b)\in\mathbb{Z}\times\mathbb{Z}$ representing $a+b\varphi$, where multiplication is reduced by the identity $\varphi^2=\varphi+1$. The zero element is $(0,0)$ and the unit is $(1,0)$.
background
Recognition Science forces the golden ratio at T6 as the unique positive solution of $x^2=x+1$. The classical spine node does this over $\mathbb{R}$ with $\sqrt{5}$, paying a Classical.choice tax. This module rebuilds the same content on an elementary integer carrier so the axiom closure stays inside ${\mathrm{propext},\mathrm{Quot.sound}}$ (sigma0, DELTA_FORCED).
Elements are pairs $(a,b)$ read as $a+b\varphi$. The ring laws are ordinary integer arithmetic once $\varphi^2=\varphi+1$ is folded into the product. Positivity is a decidable predicate on $(2a+b,b)$ (the sign trichotomy of $s+b\sqrt{5}$), so no real numbers appear in the derivation. The continuum bridge (toReal) is deferred to a separate sigma1 display module.
Downstream cost uniqueness works entirely inside this ring: sequences $\mathbb{Z}\to\mathbb{Z}[\varphi]$ satisfy a discrete d'Alembert law whose unique solution is the doubled J-cost on the $\varphi$-ladder.
proof idea
Definition only: an @[ext] structure with two integer fields (the constant term and the $\varphi$-coefficient), deriving DecidableEq and Repr. Zero is the pair $(0,0)$; One is $(1,0)$. No proof obligations beyond the instance constructors.
why it matters
This is the sigma0 carrier for the T6 golden-ratio forcing node in the Delta Forcing Spectrum program. Every uniqueness theorem in CostUniqueness is typed over maps into this ring: d'Alembert step and symmetry, d'Alembert uniqueness (the discrete replacement for continuous cosh ODE uniqueness), discrete RCL uniqueness, and the doubled J-cost $J_{\mathrm{double}}(n)=\varphi^n+\varphi^{-n}-2=2J(\varphi^n)$. Exact inverses such as $\varphi^{-1}=\varphi-1=\langle-1,1\rangle$ live here with no division. The continuum tax is paid once at the display boundary, not inside the forcing derivation. Landmark link: T6 ($\varphi$ forced) and the Recognition Composition Law, now on a choice-free integer spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.