sqrtFive_eq
plain-language theorem explainer
In the golden integers ℤ[φ], the exact carrier of √5 equals 2φ − 1. Anyone calibrating the discrete d'Alembert sequence for T5 cost uniqueness on the φ-ladder needs this identity. The proof is a one-line kernel decision on ring-element equality, with no appeal to Real.sqrt.
Claim. In the ring $\mathbb{Z}[\varphi]$, the designated element $\sqrt{5}$ equals $2\varphi-1$.
background
The module re-derives T5 cost uniqueness on the discrete φ-ladder carrier forced by T6, rather than over ℝ. The ambient ring is GoldenInt = ℤ[φ], so negative powers of φ are exact ring elements (φ⁻¹ = φ − 1) and no field division is required.
The Recognition Composition Law folds, after the usual exponential substitution, into d'Alembert's functional equation. On ℤ the solution is pinned by two initial values: h(0) = 2 and h(1) = √5. The definition sqrtFive packages that second seed as the GoldenInt pair ⟨−1, 2⟩, which the module doc identifies with 2φ − 1.
This lemma simply equates that packaged carrier to the algebraic expression 2·φ − 1 inside GoldenInt, so later uniqueness and RCL statements can cite either form.
proof idea
One-line term proof: by decide. Both sides are concrete GoldenInt values (the left via the pair definition ⟨−1, 2⟩, the right via the ring operations on φ), so the decision procedure discharges equality by kernel computation. No Real.sqrt, no analytic lemmas.
why it matters
T5 in the forcing chain asserts that any reciprocal-symmetric, normalized, calibrated cost satisfying the Recognition Composition Law equals J(x) = (x + x⁻¹)/2 − 1. On ℝ that uniqueness needs continuity and Classical.choice; on the φ-ladder it is pure two-step induction once the seeds are fixed.
The seed h(1) = √5 must match 2φ − 1 so that the discrete double-cost G(n) = traceZ n − 2 calibrates to 2·J(φ) at n = 1. This equality is the algebraic bridge between the packaged √5 carrier and that calibration constant. It sits inside the sigma0 (choice-free) re-derivation of cost uniqueness on GoldenInt, closing the continuum loophole flagged in the module trichotomy read.
No downstream uses are recorded yet; the lemma is infrastructure for the uniqueness and discrete-RCL theorems in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.