zeroSpikeDoubledTrace_not_zero_calibrated
plain-language theorem explainer
The zero-spike doubled trace fails zero-orbit calibration: it sends the zero ratio orbit to the unit orbit, not to zero. Anyone arguing uniqueness of native cost from doubled-trace axioms cites this as the explicit counterexample forcing a zero-calibration side condition. The proof rewrites cross-equality to rational equality and obtains the contradiction 1 = 0.
Claim. Let $T$ be the doubled-trace map that agrees with the native cost doubled trace on every nonzero ratio orbit and sends the zero orbit to the unit orbit. Then $T$ is not zero-calibrated: $T(0)$ is not cross-equal to the zero orbit (equivalently, the rational display of $T(0)$ is not $0$).
background
Ratio orbits are rational displays: an integer numerator over a nonzero orbit denominator, with a verifier map toRat into $\mathbb{Q}$. Cross-equality of two orbits is equivalent to equality of those rational displays (K4.10).
A doubled trace is a map $T$ on ratio orbits meant to encode the doubled character trace of a native cost. The nonzero d'Alembert law constrains $T$ only off zero, so it cannot force $T(0)$. Zero calibration is the missing side condition: cross-equality of $T(0)$ with the zero orbit. Character traces with the intended zero image have doubled trace $0$ at the zero orbit.
The zero-spike map is canonical away from zero but deliberately sets the zero orbit to the unit orbit. Its d'Alembert hypotheses never see the spike, because they are restricted to nonzero inputs.
proof idea
Assume zero calibration of the zero-spike map. Unfold the calibration predicate to cross-equality of $T(0)$ with the zero orbit. Replace cross-equality by rational equality via crossEq_iff_toRat_eq. Evaluate the spike at zero (it is the unit orbit) and apply the simplifications one.toRat = 1 and zero.toRat = 0. The hypothesis collapses to $1 = 0$, which norm_num refutes.
why it matters
Native-cost uniqueness cannot rest on nonzero d'Alembert data alone: this lemma exhibits a concrete doubled trace that satisfies the unrestricted nonzero law yet fails the intended zero image. Downstream, continuumPriceResidueWall_holds packages several such no-gos into the continuum price residue wall (base, strengthened, and prime-signed uniqueness targets all refuted). The result is a forcing step inside Primitive Recognition Calculus: any selection theorem that pins the native $J$-cost must add zero-orbit calibration (or an equivalent character-trace match) rather than hope the doubled-trace axioms close the gap by themselves. It sits upstream of the T5 $J$-uniqueness story by clearing a false uniqueness route before the genuine cost is selected.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.