Jdouble
plain-language theorem explainer
The doubled J-cost on the integer φ-ladder is G(n)=φⁿ+φ⁻ⁿ−2 in the golden ring ℤ[φ], equal to twice the classical cost J at φⁿ. It is the discrete carrier for T5 cost uniqueness without continuum analysis or choice. Downstream existence, symmetry, calibration, and uniqueness theorems cite it as the canonical normalized solution of the discrete Recognition Composition Law. The body is a one-line shift of the trace sequence by −2.
Claim. For each integer $n$, define $G(n)=\varphi^n+\varphi^{-n}-2$ as an element of the golden ring $\mathbb{Z}[\varphi]$. Equivalently $G(n)=2\,J(\varphi^n)$ where $J(x)=(x+x^{-1})/2-1$.
background
This module re-derives the T5 cost-uniqueness node on the forced discrete carrier of Recognition Science: the φ-ladder {φⁿ : n∈ℤ} inside the golden ring ℤ[φ] (pairs a+bφ with φ²=φ+1). The continuum T5 proof over ℝ needs continuity and Classical.choice to kill pathological solutions of the Recognition Composition Law (RCL). On the ladder those pathologies cannot appear: the law collapses to a two-step recurrence fixed by two initial values.
The upstream trace sequence is t(n)=φⁿ+φ⁻ⁿ, the exact ℤ[φ] stand-in for 2 cosh(n log φ). It satisfies d'Alembert's identity t(m+n)+t(m−n)=t(m)·t(n) purely algebraically. Normalization of a cost functional (Axiom 1) requires vanishing at unity: F(1)=0, which for the doubled object becomes G(0)=0.
The classical J-cost is J(x)=(x+x⁻¹)/2−1. Doubling clears the factor of 1/2 so that everything stays inside the ring: G(n)=t(n)−2=2J(φⁿ).
proof idea
One-line definition: subtract the constant 2 from the already-constructed trace sequence. No tactics, no lemmas beyond the dependency on the trace and the golden-integer carrier. Subsequent lemmas unfold this definition and rewrite with the corresponding trace identities (zero, one, negation, d'Alembert).
why it matters
This is the explicit solution object for the choice-free T5 node on the delta spine. The module doc states the program: existence of a discrete RCL solution with normalization G(0)=0 and calibration G(1)=√5−2, plus uniqueness of that solution. Both rest on this definition.
Downstream, the existence theorem rearranges the trace d'Alembert identity into the discrete RCL for G; the zero and one lemmas discharge normalization and calibration; symmetry is inherited from the evenness of the trace; and the uniqueness theorem shifts any competing sequence by +2 into the d'Alembert frame and invokes trace uniqueness. The real-embedding comparison later identifies this ring element with the classical real J-cost.
In the forcing chain this closes T5 (J-uniqueness) on the T6 carrier without leaving sigma0, matching the Recognition Composition Law skeleton while avoiding the continuum ODE argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.