zeroSpikeDoubledTrace_nonzero
plain-language theorem explainer
When a rational orbit is nonzero, the zero-spiked doubled trace equals the native doubled d'Alembert trace of the J-cost on that orbit. Downstream proofs that install doubled-trace hypotheses on the spiked object cite this equality to reduce to the unspiked native cost. The argument is a one-line rewrite discharging the zero branch by the nonzero hypothesis.
Claim. Let $q$ be a rational orbit with rational value $q \neq 0$. Then the zero-spiked doubled trace of $q$ equals the native doubled d'Alembert trace $T_J(q) = 2\bigl(J(q)+1\bigr)$ of the PRC J-cost $J(q) = \frac{q+q^{-1}}{2}-1$ on ratio orbits.
background
A ratio orbit is an integer-numerator / nonzero-denominator display of a rational (K4.7). Its verifier map toRat recovers the ordinary rational by transport; the internal equality is cross-multiplication.
PRC's rational J-cost on a ratio orbit is $J(q)=((q+q^{-1})/2)-1$. The native doubled d'Alembert trace of a cost $F$ is $T_F(q)=2(F(q)+1)$; for a generated cost this is exactly $\chi(q)+\chi(q)^{-1}$.
The zero-spiked doubled trace is canonical away from zero but deliberately sends the zero orbit to trace $1$. The surrounding doubled-trace hypotheses never see that spike, because their d'Alembert law is restricted to nonzero inputs.
proof idea
One-line wrapper. Unfold the definition of the zero-spiked doubled trace and apply if_neg with the hypothesis that the rational value is nonzero, so the else branch is exactly the native doubled trace of the J-cost on ratio orbits.
why it matters
Feeds zeroSpikeDoubledTrace_hypotheses, which packages reciprocal, normalized-invariant, and d'Alembert structure for the spiked object. That package is the bridge from the deliberately spiked display back to the native cost uniqueness story in this module: away from zero the spike is invisible, so uniqueness and d'Alembert inheritance reduce to the unspiked J-cost.
In the broader Recognition chain this sits under T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. The spike is a technical device so that zero does not break the hypothesis interface; this lemma is the exact point where the device is discharged for nonzero orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.