zeroSpikeDoubledTrace_hypotheses
plain-language theorem explainer
The zero-spike doubled trace on ratio orbits satisfies the full PRC doubled-trace hypothesis package: reciprocal symmetry, normalization invariance, d'Alembert, unit trace T(1)≃2, and the two-trace calibration. Native-cost uniqueness arguments cite it as a concrete witness. The proof is a five-goal structure refine: zero/nonzero case splits on ratios, then rational transport and field/ring algebra.
Claim. Let $T_0$ be the zero-spike doubled-trace map on ratio orbits. Then $T_0$ satisfies the doubled-trace hypotheses: $T_0(q)\simeq T_0(q^{-1})$ and $T_0(q)\simeq T_0(\mathrm{normalize}(q))$ under cross-equality of orbits; the doubled-trace d'Alembert identity on nonzero orbits; $T_0(1)\simeq 2$; and the two-trace calibration field of the hypothesis package.
background
In the Primitive Recognition Calculus, costs live on ratio orbits (integer-rational displays of positive scale ratios). Cross-equality of orbits is the verifier relation equivalent to equality of rational displays: crossEq a b ↔ a.toRat = b.toRat. The reciprocal sends an orbit to its inverse ratio; normalization is the DistinctionNat reduction of a ratio display.
A doubled trace $T$ of a native PRC cost is a map on ratio orbits asked to obey five structural axioms packed as PRCDoubledTraceHypotheses: reciprocal symmetry, invariance under normalization, a doubled-trace d'Alembert law, unit calibration $T(1)\simeq 2$, and a two-trace calibration. The zero-spike doubled trace agrees with the native doubled-trace value off the zero ratio and takes a special spike value on the zero display.
Upstream rational transport (add_toRat, mul_toRat, crossEq_iff_toRat_eq, crossEq_refl) lets every orbit identity be checked as an equality of rationals. Reciprocal symmetry of the underlying character supplies the nonzero reciprocal case.
proof idea
Refine the five structure fields of PRCDoubledTraceHypotheses.
Reciprocal and normalized-invariant: case on q.toRat = 0. If zero, both sides of the claimed cross-equality hit the spike branch (reciprocal/normalize preserve vanishing), so reduce by crossEq_iff_toRat_eq. If nonzero, open the nonzero formula and apply doubledTraceValue_congr to reciprocal symmetry (resp. normalization invariance) of the underlying value.
D'Alembert: for nonzero $x,y$, products and quotients stay nonzero; rewrite all four $T$-applications to the native doubled-trace formula, pass to rationals via crossEq_iff_toRat_eq and the *_toRat lemmas, then field_simp and ring.
Unit trace: nonzero branch at $1$, expand native doubled trace / doubled-trace value, norm_num to get $2$.
Two-trace: nonzero branch at $2$, then crossEq_refl.
why it matters
This lemma is the hypothesis witness that lets the zero-spike doubled trace serve as a counter-model inside native cost uniqueness. Its sole downstream consumer is PRCDoubledTraceCoherentRootTarget_refuted, which assumes a coherent root target, instantiates it at the zero-spike map plus these hypotheses, and derives a contradiction from zeroSpikeDoubledTrace_no_ratio_character_trace.
In Recognition terms this is local scaffolding for J-uniqueness (forcing chain T5) inside the Primitive Recognition Calculus: the doubled trace is the orbit-level shadow of the cost whose d'Alembert form encodes the Recognition Composition Law. By exhibiting a map that meets every doubled-trace axiom yet admits no matching ratio-character trace, the development rules out an overly loose "coherent root" existence claim and forces cost reconstruction to stay on the genuine native character path rather than an arbitrary d'Alembert solution.
It does not itself name T5 or the closed-form $J(x)=(x+x^{-1})/2-1$; it supplies the concrete spiked witness those uniqueness arguments need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.