zeroSpikeDoubledTrace
plain-language theorem explainer
Defines a doubled d'Alembert trace that equals the native J-cost doubled trace on every nonzero rational orbit, but sends the zero orbit to the unit orbit. Used as a counterexample carrier against uniqueness and coherent-root claims that omit zero calibration. The body is a one-line conditional on the rational display of the orbit.
Claim. For a rational orbit $q$, define the zero-spiked doubled trace by $T_\bullet(q) := 1$ if the rational display of $q$ is $0$, and $T_\bullet(q) := 2\bigl(J(q)+1\bigr)$ otherwise, where $J(q)=\frac{q+q^{-1}}{2}-1$ is the native ratio-orbit cost.
background
In the primitive recognition calculus, costs and traces live on RatioOrbit: an integer-numerator / nonzero-denominator display of a rational. The verifier map toRat recovers the ordinary rational. The native cost on these orbits is the J-cost $J(q)=((q+q^{-1})/2)-1$, written as a ratio-orbit object rather than a real function.
The doubled d'Alembert trace of a cost $F$ is $T_F(q)=2(F(q)+1)$. For a character-generated cost this equals $\chi(q)+\chi(q)^{-1}$. The module studies which algebraic hypotheses on such a $T$ force it to arise from the native J-cost, and which extra calibrations (especially at zero) are needed.
The d'Alembert law in the doubled-trace hypothesis package is stated only for nonzero inputs, so a modification supported only at the zero orbit is invisible to those axioms.
proof idea
Definition by cases on the rational display: if q.toRat = 0, return the unit orbit; otherwise apply nativeCostDoubledTrace to the native J-cost onRatioOrbit at $q$. No lemmas are invoked; the body is a single conditional.
why it matters
This is the standard counterexample object for native-cost uniqueness without zero calibration. Downstream, zeroSpikeDoubledTrace_hypotheses shows it still satisfies the nonzero d'Alembert package; zeroSpikeDoubledTrace_no_ratio_character_trace shows it is not a character sum $\chi+\chi^{-1}$; zeroSpikeDoubledTrace_not_zero_calibrated records the deliberate failure at zero; and PRCDoubledTraceCoherentRootTarget_refuted uses it to kill the coherent-root uniqueness target.
It also feeds the continuum-price residue wall: the base ledger admits twists (here, a zero spike) that ContinuousOn plus one-point calibration would have ruled out on the reals. In the forcing chain this sits under T5 J-uniqueness: algebraic d'Alembert alone on nonzero rationals does not pin $J$ until zero (or continuum) data is restored.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.