jdouble_eq_jcost
plain-language theorem explainer
Evaluating the sigma0 doubled cost at integer rung n yields twice the classical recognition cost of φ^n. Anyone citing the T5 display bridge or the continuum realization of the discrete RCL needs this identity. The proof unfolds definitions (trace embedding, Jcost) and closes by ring arithmetic.
Claim. For every integer $n$, the real evaluation of the discrete doubled cost $J_{\mathrm{double}}(n)=\varphi^n+\varphi^{-n}-2$ equals $2\,J(\varphi^n)$, where $J(x)=(x+x^{-1})/2-1$ is the classical recognition cost and $\varphi$ is the golden ratio.
background
The module GoldenIntReal is the sigma1 display bridge: it evaluates the ring $\mathbb{Z}[\varphi]$ into $\mathbb{R}$ once, so that sigma0 structure (derived inside GoldenInt with only propext and Quot.sound) maps onto the classical PhiForcing presentation. The map toReal sends $a+b\varphi$ to $a+b\varphi_{\mathbb{R}}$ and is a ring embedding.
Upstream, CostUniqueness defines the discrete ladder inside GoldenInt. The trace sequence is $\mathrm{traceZ}(n)=\varphi^n+\varphi^{-n}$, the exact $\mathbb{Z}[\varphi]$ carrier of $2\cosh(n\log\varphi)$. The doubled cost is then $J_{\mathrm{double}}(n)=\mathrm{traceZ}(n)-2$, documented as equal to $2\cdot J(\varphi^n)$ with $J(x)=(x+x^{-1})/2-1$. The continuum cost is the same formula: $J_{\mathrm{cost}}(x)=(x+x^{-1})/2-1$.
The discrete Recognition Composition Law and uniqueness of this cost were already proved at sigma0; this module only pays the continuum tax (Real.sqrt, classical choice) at the display boundary.
proof idea
Unfold $J_{\mathrm{double}}(n)$ as $\mathrm{traceZ}(n)-2$. After recording $\varphi\neq 0$ from positivity, rewrite the goal with the embedding lemmas: toReal of a difference, of the trace, and of the constant 2, together with the definition of $J_{\mathrm{cost}}$ and the negative-power rule for real zpow. The resulting algebraic identity is discharged by ring.
why it matters
This identity is one half of the T5 display bridge (t5_bridge), the module capstone: under evaluation, the sigma0-forced cost ladder is exactly the classical J-cost on the $\varphi$-ladder (and, via the companion traceZ_cosh, its cosh form). Everything with mathematical content (existence, uniqueness, the composition law) was already proved at sigma0 in CostUniqueness; the bridge is pure translation.
In the forcing chain this realizes T5 (J-uniqueness: $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$) on the continuum side, while the discrete RCL that forces $J$ lives in Cost.FunctionalEquation. Downstream work that quotes classical $J(\varphi^n)$ against the integer ladder cites this equality rather than re-deriving the embedding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.