PRCDoubledTraceZeroCalibratedLinearRootTarget
plain-language theorem explainer
Packages the claim that every doubled-trace map on rational orbits obeying the native PRC hypotheses and zero-calibration admits a working linear root candidate (a ratio character whose doubled trace recovers the map). Cost-uniqueness arguments in the primitive recognition calculus cite this interface. The body is a pure Prop abbreviation, not a proof; discharge lives in the companion proved theorem.
Claim. For every map $T$ from rational orbits to rational orbits, if $T$ satisfies the doubled-trace hypotheses (reciprocity under orbit inversion, invariance under ratio normalization, and the d'Alembert functional equation) and is zero-calibrated ($T(0)$ is cross-equal to the zero orbit), then the linear root candidate for $T$ works: it is a ratio character, and for every orbit $q$ the doubled-trace reconstruction via that character is cross-equal to $T(q)$.
background
In the primitive recognition calculus, costs are reconstructed from characters on rational orbits. A RatioOrbit is an integer-numerator / nonzero-orbit-denominator display of a rational scale ratio. The doubled trace of a native cost is a map $T$ on those orbits that records the sum of the cost at $q$ and at its reciprocal, up to the cross-equality relation used throughout the module.
PRCDoubledTraceHypotheses packages the structural laws such a $T$ must obey: reciprocity ($T(q)$ matches $T(1/q)$), normalization invariance, and a d'Alembert identity. Separately, zero-calibration requires $T(0)=0$. The nonzero d'Alembert law alone cannot force the value at the zero orbit; character traces with the intended zero image do force it, so the calibration is stated as an extra hypothesis.
The linear-root candidate problem asks whether there exists a ratio character whose doubled trace recovers $T$. The sibling PRCDoubledTraceLinearRootCandidateWorks is the exact statement that the concrete linear root candidate built from $T$ is a ratio character and matches $T$ pointwise under cross-equality.
proof idea
No proof body: this is a def equating a name to a Prop. The proposition is the universal quantification over maps $T$, assuming doubled-trace hypotheses and zero-calibration, and concluding that the linear root candidate works. Downstream theorems either assume this Prop as a hypothesis or prove it by constructing the candidate and checking the character and trace-match conditions.
why it matters
This target is the linear-root gate in the native-cost uniqueness pipeline. The companion theorem PRCDoubledTraceZeroCalibratedLinearRootTarget_proved discharges it; the bridge PRCDoubledTraceZeroCalibratedCoherentRootTarget_of_linear_root lifts a proof of this linear-root target to the coherent-root target used later in the uniqueness argument.
In the broader Recognition Science forcing chain, uniqueness of the native cost is the local avatar of T5 J-uniqueness: the cost must be the standard $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced by the Recognition Composition Law. Packaging the linear-root obligation as a named Prop keeps the zero-calibration repair visible and lets the coherent-root and uniqueness theorems cite a single interface rather than inlining the quantifiers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.