zeroSpikeDoubledTrace_no_ratio_character_trace
plain-language theorem explainer
No ratio-orbit character can reproduce the zero-spike doubled trace as χ(q)+χ(q)⁻¹ under cross-equivalence. Used when closing the coherent-root branch of PRC native-cost uniqueness. The proof specializes at the zero orbit: reciprocity forces a=a⁻¹ while the trace forces a+a⁻¹=1, impossible in ℚ.
Claim. There is no map $\chi$ from ratio orbits to ratio orbits that is a PRC ratio character (unit at $1$, multiplicative, and reciprocal, all up to cross-equivalence) such that for every ratio orbit $q$, $\chi(q)+\chi(q)^{-1}$ is cross-equivalent to the zero-spike doubled trace of $q$.
background
In the Primitive Recognition Calculus, costs live on ratio orbits: quotient-native rational data with a verifier display toRat. Cross-equivalence is the internal equality relation: two orbits match when cross-multiplication balances as signed orbits, and it agrees with rational equality of the displays (crossEq_iff_toRat_eq).
A PRC ratio character is a candidate d'Alembert root at orbit level: it sends the unit orbit to itself, multiplies under orbit multiplication, and intertwines reciprocal, all up to cross-equivalence rather than definitional equality. The doubled-trace reconstruction of a cost is then the orbit sum $\chi(q)+\chi(q)^{-1}$.
The zero-spike doubled trace is a concrete target functional on orbits. At the zero orbit its display is $1$ (zeroSpikeDoubledTrace_zero with one_toRat). This module studies whether any native PRC cost can arise from such a character factorization.
proof idea
Assume a character $\chi$ matches the zero-spike doubled trace everywhere. Specialize to the zero orbit and set $a:=(\chi(0)).\mathrm{toRat}$.
The character reciprocal law at zero, rewritten via crossEq_iff_toRat_eq, recip_zero_eq, and recip_toRat, yields $a=a^{-1}$.
The trace-matching hypothesis at zero, rewritten via add_toRat, recip_toRat, zeroSpikeDoubledTrace_zero, and one_toRat, yields $a+a^{-1}=1$.
Linear arithmetic forces $a=1/2$. Substituting into $a=a^{-1}$ and norm_num gives the contradiction.
why it matters
This lemma is the concrete obstruction used by PRCDoubledTraceCoherentRootTarget_refuted: any coherent-root package for the zero-spike doubled trace would supply exactly the forbidden character-plus-trace data, so the coherent-root target is empty.
In the broader PRC native-cost uniqueness program, one must rule out alternate d'Alembert factorizations before the native cost can be identified with the unique J-cost from the forcing chain (T5: $J(x)=(x+x^{-1})/2-1$). Zero-spike is the simplest nontrivial doubled-trace probe; killing a ratio character for it closes one coherent-root escape hatch.
Downstream uniqueness arguments therefore inherit a hard negative: no quotient-native multiplicative reciprocal root reproduces this spike as a character trace.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.