PRCDoubledTraceLinearRootQuadraticTarget
plain-language theorem explainer
For a doubled-trace map T on ratio orbits, this Prop demands that at every nonzero q the linear root candidate χ and the residual T(q)−χ multiply to the unit under cross-equivalence. Cost-uniqueness arguments cite it as the algebraic packaging of the reciprocal-root identity for X²−TX+1=0. It is a pure definition of that target predicate, not a proved statement.
Claim. A map $T$ from ratio orbits to ratio orbits satisfies the doubled-trace linear-root quadratic target when, for every ratio orbit $q$ whose rational display is nonzero, the product of the linear root candidate of $T$ at $q$ with $T(q)$ minus that candidate is cross-equivalent to the unit ratio orbit.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero orbit denominator; its verifier display toRat is the ordinary rational, while internal equality is crossEq (cross-multiplication of signed orbits balances). The doubled-trace setting treats a map $T$ meant to act as $T(q)=\chi(q)+\chi(q)^{-1}$ for a multiplicative character $\chi$.
The linear root candidate is the explicit split forced at the distinguished axis 2: when $\chi(2)=2$, one recovers $\chi(q)=(2,T(2q)-T(q))/3$ (zero case handled by zero-calibration). If $T$ really is a doubled trace, the two roots of $X^2-T(q)X+1=0$ are $\chi(q)$ and $\chi(q)^{-1}$, so their product is 1.
This module packages native-cost uniqueness targets on that algebraic skeleton, upstream of the J-cost and d'Alembert chain that forces the Recognition Composition Law.
proof idea
Definition only: the body is the universal Prop that, for every nonzero $q$, crossEq holds between the product of traceRootCandidate T q with T q minus that candidate, and the unit ratio orbit. No tactics or lemmas are applied; downstream theorems discharge or consume the predicate.
why it matters
This target is the quadratic-product half of the linear-root package used to reconstruct the character from a doubled trace. It is proved from doubled-trace hypotheses plus cross-equivalence respect by traceRootCandidate_quadratic_of_trace_respect, and is then fed to nonzeroness, reciprocity, and trace-reconstruction lemmas (traceRootCandidate_nonzero_of_quadratic, traceRootCandidate_reciprocal_of_quadratic, traceRootCandidate_trace_of_quadratic). Those close into PRCDoubledTraceZeroCalibratedLinearRootTarget_proved.
In the broader RS chain this sits under native-cost uniqueness: once the character is recovered as the linear root, the cost is forced to the J-cost $J(x)=(x+x^{-1})/2-1$ (T5), which is the functional seed of the Recognition Composition Law. Without the product-to-one identity the reciprocal root would not be identified and the uniqueness argument would stall.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.