PRCDoubledTraceZeroCalibratedCoherentRootTarget
plain-language theorem explainer
Packages the repaired coherent-root existence claim: every zero-calibrated doubled trace T on ratio orbits that obeys the native doubled-trace hypotheses is the doubled character trace χ+χ⁻¹ of some ratio character χ. Native-cost uniqueness proofs cite this Prop as the post-zero-spike target. It is a pure definition of a proposition, later discharged by linear-root extraction.
Claim. For every map $T$ from ratio orbits to ratio orbits, if $T$ satisfies the doubled-trace hypotheses (reciprocal symmetry $T(q)\sim T(q^{-1})$, normalization invariance, and the d'Alembert identity) and is zero-calibrated ($T(0)\sim 0$), then there exists a ratio character $\chi$ such that $\chi(q)+\chi(q)^{-1}$ is cross-equivalent to $T(q)$ for every ratio orbit $q$.
background
In the Primitive Recognition Calculus, costs and characters live on RatioOrbit: rational displays built from a signed-orbit numerator and a nonzero distinction-nat denominator. Equality of displays is internal cross-multiplication balance (crossEq), not external real equality. Reciprocals send zero to zero as in $\mathbb{Q}$.
A doubled trace $T$ of a native cost is required to obey PRCDoubledTraceHypotheses: reciprocal symmetry, invariance under ratio normalization, and a d'Alembert functional equation. The nonzero d'Alembert law does not constrain $T(0)$; PRCDoubledTraceZeroCalibrated supplies the missing compatibility $T(0)\sim 0$, matching character traces that send the zero orbit to zero.
The module targets uniqueness of the native PRC cost (the J-cost side of the forcing chain). After a zero-spike no-go blocked an earlier root target, this Prop is the repaired coherent-root statement: recover a ratio character whose doubled trace reproduces $T$.
proof idea
Definitional packaging only: the body is the universal-existential Prop above. No tactics or lemmas are applied at this declaration. Downstream, PRCDoubledTraceZeroCalibratedCoherentRootTarget_of_linear_root discharges it by reducing to a linear-root target and instantiating $\chi$ as the explicit candidate traceRootCandidate T (the linear extraction with denominator 3). The closed form ..._proved then chains that reduction to a proved linear-root theorem.
why it matters
This is the post-repair existence interface in the native-cost uniqueness pipeline. Parent theorems PRCDoubledTraceZeroCalibratedCoherentRootTarget_of_linear_root and ..._proved turn the Prop into a theorem, so uniqueness arguments can assume a coherent root character rather than re-prove root extraction. In framework terms it supports T5-style J-uniqueness: native doubled traces that satisfy RCL-type d'Alembert data plus zero calibration must arise as $\chi+\chi^{-1}$ for a ratio character, the discrete precursor of $J(x)=(x+x^{-1})/2-1$. The doc flags it as the repaired target after the zero-spike no-go; the remaining upstream blocker noted downstream is exact zero-orbit compatibility already encoded here as the calibration hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.