sqrtFive_sq
plain-language theorem explainer
Exact identity (√5)² = 5 inside the golden integers ℤ[φ], where √5 is the ring element −1 + 2φ rather than a real square root. Anyone building the discrete T5 cost uniqueness on the φ-ladder cites this kernel fact. The proof is a one-tactic decide on the concrete GoldenInt multiplication.
Claim. In the golden integers $\mathbb{Z}[\varphi]$, the element $\sqrt{5} := -1 + 2\varphi$ satisfies $(\sqrt{5})^2 = 5$.
background
CostUniqueness re-derives the T5 J-cost uniqueness node on the discrete φ-ladder carrier forced by T6, avoiding continuum choice. The ambient ring is GoldenInt = ℤ[φ], pairs ⟨a,b⟩ for a + bφ, with φ the golden ratio unit.
The module introduces sqrtFive as the exact ring element ⟨−1, 2⟩, i.e. −1 + 2φ. Because φ = (1+√5)/2 one has 2φ − 1 = √5 in ℝ, but here √5 never leaves ℤ[φ]: no Real.sqrt, no field inversion. Downstream the same element calibrates the trace sequence t(n) = φⁿ + φ⁻ⁿ (the ℤ[φ] stand-in for 2 cosh(n log φ)) via the initial value h(1) = √5.
That calibration is the discrete replacement for the continuum cosh uniqueness argument in the classical RCL → Jcost forcing chain.
proof idea
One-line tactic proof: by decide. Lean reduces the concrete product ⟨−1, 2⟩ * ⟨−1, 2⟩ in the GoldenInt ring structure and checks equality with the integer 5 (embedded as ⟨5, 0⟩). No lemmas are invoked beyond the decidable equality and arithmetic of the pair representation.
why it matters
T5 in the forcing chain identifies J(x) = (x + x⁻¹)/2 − 1 as the unique reciprocal-symmetric normalized cost obeying the Recognition Composition Law. On ℝ that uniqueness needs continuity and Classical.choice; on the φ-ladder it collapses to a two-step recurrence for the trace t(n).
The recurrence is pinned by t(0) = 2 and t(1) = √5. This theorem guarantees that the ring element used for that initial value really squares to 5, so the discrete calibration G(1) = √5 − 2 = 2·J(φ) is algebraically consistent. It is pure kernel arithmetic supporting the sigma0 (choice-free) re-derivation of cost uniqueness on GoldenInt.
No downstream dependents are recorded yet; the immediate consumers are the uniqueness and RCL-satisfaction theorems for traceZ / Jdouble in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.