Jdouble_symm
plain-language theorem explainer
Reciprocal symmetry of the doubled J-cost on the φ-ladder: Jdouble(−n) equals Jdouble(n) for every integer n, i.e. 2·J(φ⁻ⁿ)=2·J(φⁿ). Anyone citing the discrete T5 uniqueness package needs this as the derived (not assumed) symmetry half. The proof is a one-line unfold of Jdouble followed by the trace symmetry lemma.
Claim. For every integer $n$, the doubled J-cost on the $\varphi$-ladder satisfies $J_{\mathrm{double}}(-n)=J_{\mathrm{double}}(n)$, equivalently $2\,J(\varphi^{-n})=2\,J(\varphi^{n})$ where $J(x)=(x+x^{-1})/2-1$.
background
The module CostUniqueness re-derives the T5 cost-uniqueness node on the discrete carrier forced by T6: the φ-ladder ${\varphi^n:n\in\mathbb{Z}}$ inside GoldenInt = $\mathbb{Z}[\varphi]$. Continuum T5 proves that any reciprocal-symmetric, normalized, calibrated continuous $F$ obeying the Recognition Composition Law equals $J(x)=(x+x^{-1})/2-1$, but that argument uses Classical.choice. On the ladder the d'Alembert form is a two-step recurrence, so two initial values pin the solution by induction with no continuity or choice.
The doubled cost is defined by $J_{\mathrm{double}}(n)=\mathrm{traceZ}(n)-2$, where $\mathrm{traceZ}(n)=\varphi^n+\varphi^{-n}$ is the exact $\mathbb{Z}[\varphi]$ carrier of $2\cosh(n\log\varphi)$. Thus $J_{\mathrm{double}}(n)=2,J(\varphi^n)$. Upstream, $\mathrm{traceZ_neg}$ already records reciprocal symmetry of the trace: $\mathrm{traceZ}(-n)=\mathrm{traceZ}(n)$, proved by unfolding and an omega-derived double-negation identity (choice-free).
proof idea
One-line term-mode argument. Unfold the definition $J_{\mathrm{double}}(n)=\mathrm{traceZ}(n)-2$; the claim reduces to $\mathrm{traceZ}(-n)-2=\mathrm{traceZ}(n)-2$. Rewrite with the upstream lemma $\mathrm{traceZ_neg}$, which supplies $\mathrm{traceZ}(-n)=\mathrm{traceZ}(n)$. No induction or ring arithmetic beyond that rewrite.
why it matters
Feeds directly into $\mathrm{t5_delta_forced}$, the sigma0 (choice-free) T5 package on the φ-ladder. That theorem lists five properties of $J_{\mathrm{double}}$: normalization, calibration, reciprocal symmetry, discrete RCL, and uniqueness given only the first two. The third conjunct is exactly $\forall n,,J_{\mathrm{double}}(-n)=J_{\mathrm{double}}(n)$, and the doc stresses that symmetry is derived from the law, not assumed.
In the forcing chain this is the discrete T5 node: J-uniqueness on the carrier forced by T6 (φ as self-similar fixed point). Continuum T5 needed an a-priori reciprocal-symmetry hypothesis; here the same identity is inherited from the algebraic construction of the trace, closing the choice-free re-derivation of cost uniqueness on the recognition ledger's actual domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.