Jdouble_zero
plain-language theorem explainer
On the φ-ladder the doubled J-cost vanishes at the identity rung: 2·J(φ⁰)=0. Anyone assembling the discrete T5 uniqueness package cites this as the normalization pin. The argument unfolds the definition, rewrites by the zero-trace identity, and finishes with ring arithmetic.
Claim. The doubled cost on the golden-integer ladder satisfies $2\cdot J(\varphi^{0})=0$, i.e. $\varphi^{0}+\varphi^{0}-2=0$ under the identification $2J(x)=x+x^{-1}-2$.
background
This module re-derives T5 cost-uniqueness on the discrete carrier forced by T6: the φ-ladder ${\varphi^{n}:n\in\mathbb{Z}}$ inside GoldenInt = ℤ[φ]. Continuum pathologies never appear; the d'Alembert law becomes a two-step recurrence pinned by two initial values.
The doubled cost is defined by $J_{\mathrm{double}}(n)=\mathrm{trace}{Z}(n)-2=\varphi^{n}+\varphi^{-n}-2=2\cdot J(\varphi^{n})$, where $J(x)=(x+x^{-1})/2-1$ is the unique reciprocal-symmetric cost from the Recognition Composition Law. Here $\mathrm{trace}{Z}$ is the exact $\mathbb{Z}[\varphi]$ carrier of $2\cosh(n\log\varphi)$.
Upstream, $\mathrm{trace}_{Z}(0)=2$ is already proved by unfolding to $\varphi^{0}+\varphi^{0}$ and evaluating the unit powers. Calibration axioms in the continuum CostAxioms bundle motivate the discrete pin $G(0)=0$, but are not invoked here.
proof idea
One short tactic proof. Unfold $J_{\mathrm{double}}$ to $\mathrm{trace}{Z}(0)-2$. Rewrite with the lemma $\mathrm{trace}{Z}(0)=2$, obtaining $2-2$. Close by ring. No induction, no RCL identity, no calibration step.
why it matters
Supplies the normalization conjunct of t5_delta_forced, the sigma0 (choice-free) T5 package on the φ-ladder: $J_{\mathrm{double}}(0)=0$, calibration $J_{\mathrm{double}}(1)=\sqrt{5}-2$, derived reciprocal symmetry, discrete RCL, and uniqueness given only those pins. That theorem is the discrete counterpart of the continuum T5 node (J-uniqueness via RCL), which the module doc classifies as sigma1 because of continuum choice. Closing normalization here is the first of the two initial values that let induction force the whole sequence, aligning with forcing-chain T5 and the T6 self-similar carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.