t5_bridge
plain-language theorem explainer
Under real evaluation, the sigma0 doubled cost ladder on ℤ[φ] is exactly twice the classical recognition cost J on the real φ-ladder, and the integer trace is twice cosh of n log φ. Cite this for the continuum reading of T5 (J-uniqueness and its cosh form). The proof is a pure term pairing of two already-proved evaluation lemmas.
Claim. For every $n\in\mathbb{Z}$, the real image of the doubled ladder cost at rung $n$ equals $2\,J(\varphi^n)$, and the real image of the integer trace at rung $n$ equals $2\cosh(n\log\varphi)$, where $J(x)=(x+x^{-1})/2-1$ and $\varphi$ is the classical golden ratio.
background
This module is the sigma1 display boundary for the DeltaSpine development. All forcing content for the cost ladder lives in ℤ[φ] (sigma0); here one pays the continuum tax once via the ring embedding toReal : a + b·φ ↦ a + b·φ_ℝ, which is injective by irrationality descent and sends the sigma0 unit φ to the classical PhiForcing.φ.
The classical recognition cost is $J(x)=(x+x^{-1})/2-1$ on positive reals (equivalently $\cosh(\log x)-1$). In CostUniqueness the doubled ladder cost is the GoldenInt element $J_{\mathrm{double}}(n)=\mathrm{trace}_Z(n)-2$, intended as $\varphi^n+\varphi^{-n}-2=2J(\varphi^n)$, with $\mathrm{trace}_Z(n)$ the integer lift of $\varphi^n+\varphi^{-n}$. T5 in the forcing chain is precisely uniqueness of this $J$.
Existence, uniqueness, and the Recognition Composition Law for the cost were already proved at sigma0 in CostUniqueness. This declaration only translates those objects across the evaluation map.
proof idea
One-line term proof: the conjunction is the pair of the two prior evaluation lemmas jdouble_eq_jcost and traceZ_cosh. The first identifies toReal(Jdouble n) with $2,J(\varphi^n)$; the second identifies toReal(traceZ n) with $2\cosh(n\log\varphi)$. No new algebra is done here.
why it matters
Capstone T5 display bridge for the DeltaSpine path. The forcing-chain landmark T5 fixes $J(x)=(x+x^{-1})/2-1=\cosh(\log x)-1$; CostUniqueness already forced the ladder form and composition law inside ℤ[φ]. This theorem is the honest continuum reading: after toReal, the sigma0 ladder is exactly classical $J$ on the φ-powers together with the cosh closed form.
It sits with the module's other bridges (t6_bridge, positivity via isPos_iff_toReal_pos) that make sigma0 uniqueness and trichotomy statements about the real order rather than a private surrogate. No downstream consumers are wired yet in the graph; the role is presentational closure of T5 at the ℝ boundary, not a new derivation step. Derivation remains delta-forced; only display uses classical choice (Real.sqrt, real arithmetic).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.