PRCDoubledTraceLinearRootCandidateWorks
plain-language theorem explainer
Packages the repaired doubled-trace root problem as an exact linear-root predicate on a map T of ratio orbits: the forced candidate must be a ratio character, and its value plus reciprocal must recover T under cross-equivalence. Downstream uniqueness targets cite this Prop as the success condition. Pure definitional packaging; no proof obligations.
Claim. For a map $T$ on ratio orbits, write $\chi_T$ for the linear root candidate forced by the split-trace formula at axis $2$. The predicate asserts that $\chi_T$ is a ratio character (unit at $1$, multiplicative up to cross-equivalence) and that $\chi_T(q)+\chi_T(q)^{-1}$ is cross-equivalent to $T(q)$ for every ratio orbit $q$.
background
In the Primitive Recognition Calculus, costs live on ratio orbits: pairs of a signed numerator orbit and a nonzero distinction-orbit denominator. Equality is the internal cross-multiplication relation (balanced scaled numerators), not definitional identity, so statements stay quotient-native.
A ratio character is a map on ratio orbits that sends $1$ to $1$ and is multiplicative up to cross-equivalence. The d'Alembert factorization of a PRC cost asks for a character $\chi$ with $T(q)=\chi(q)+\chi(q)^{-1}$. The linear root candidate is the closed-form inversion of that split at the distinguished axis $2$: when $\chi(2)=2$, one has $\chi(q)=(2,T(2q)-T(q))/3$, with the zero orbit handled by the repaired zero-calibration field.
This module packages native-cost uniqueness for the doubled-trace presentation of that factorization.
proof idea
Definitional only: the body is the conjunction of two Props. First, the linear root candidate of $T$ satisfies the ratio-character axioms (unit and multiplicativity under cross-equivalence). Second, for every ratio orbit $q$, the sum of the candidate at $q$ and its total reciprocal is cross-equivalent to $T(q)$. No tactics, no lemmas discharged here.
why it matters
This is the exact success condition for the repaired doubled-trace root problem. The immediate parent is the zero-calibrated linear-root target: every $T$ obeying the doubled-trace hypotheses and zero-calibration must satisfy this predicate. That target is the bridge from native doubled-trace data to a genuine ratio character, which is the d'Alembert factor needed for PRC cost uniqueness.
In the broader Recognition chain this sits under J-uniqueness (T5): the cost $J(x)=(x+x^{-1})/2-1$ is the unique continuous solution of the Recognition Composition Law, and the character-plus-reciprocal factorization is the algebraic skeleton of that uniqueness at the ratio-orbit level. Closing the linear-root target discharges the constructive half of recovering $\chi$ from $T$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.