zeroSpikeDoubledTrace_zero
plain-language theorem explainer
The zero-spiked doubled trace sends the zero ratio orbit to the unit orbit. Anyone ruling out zero-calibration or character-trace representations of this spike map cites the identity. The proof is a one-line rewrite: unfold the spike definition and fire the positive branch via zero-to-rational.
Claim. Let $T^\sharp$ be the doubled-trace map that equals the native cost doubled trace off zero and returns the unit ratio orbit on zero. Then $T^\sharp(0) = 1$ in the ratio-orbit monoid.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator, with evaluation toRat into $\mathbb{Q}$. The native cost doubled trace is the orbit-level lift of the usual doubled character trace $q \mapsto \chi(q)+\chi(q)^{-1}$ built from the PRC cost character.
The zero-spike variant keeps that native map on every nonzero orbit but deliberately forces the zero orbit to the unit orbit. Its doc-comment states the motive: current doubled-trace hypotheses never see the spike, because their d'Alembert law is restricted to nonzero inputs. The supporting fact zero.toRat = 0 is the simp lemma that opens the positive branch of the spike definition.
Local setting is native-cost uniqueness: which doubled traces can arise from a ratio character and which calibration axioms they must obey.
proof idea
One-line wrapper. Rewrite by the definition of the zero-spike map, then apply if_pos with the simp fact that the zero orbit evaluates to rational zero. The true branch returns the unit ratio orbit, which is the claimed right-hand side. No further algebraic work.
why it matters
Feeds two negative uniqueness results in the same module. First, zeroSpikeDoubledTrace_no_ratio_character_trace: no ratio character $\chi$ can reproduce the spiked doubled trace via the cross-equation $\chi(q)+\chi(q)^{-1}$. Second, zeroSpikeDoubledTrace_not_zero_calibrated: the spike fails zero-calibration, proved by rewriting the calibration predicate through this identity and comparing 1.toRat against 0.toRat.
In the Recognition framework this is a boundary probe on T5 J-uniqueness and the Recognition Composition Law. The native cost (built from $J(x)=(x+x^{-1})/2-1$) is forced only under the full hypothesis package; a one-point spike at zero is enough to leave the character-trace class while still agreeing with the d'Alembert law on the nonzero locus. The lemma therefore pins the necessity of zero-calibration in the native-cost uniqueness chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.