traceRootCandidate_trace_of_quadratic
plain-language theorem explainer
Under doubled-trace hypotheses, cross-equivalence respect, zero calibration, and the linear-root quadratic target, the candidate root r of T at any ratio orbit q satisfies r + r^{-1} ~ T(q). Used when identifying native PRC costs with character traces. Proof cases on the zero orbit, then reduces the nonzero case via reciprocal identities and ring arithmetic on rational displays.
Claim. Let $T$ map ratio orbits to ratio orbits, satisfy the doubled-trace hypotheses (reciprocity, normalization invariance, d'Alembert, unit/two traces), respect cross-equivalence, be zero-calibrated ($T(0)\sim 0$), and obey the linear-root quadratic target. Then for every ratio orbit $q$, writing $r$ for the trace-root candidate of $T$ at $q$, one has $r+r^{-1}\sim T(q)$ under cross-multiplication equivalence.
background
In the Primitive Recognition Calculus, ratio orbits are internal rational displays built from signed $\delta$-orbits. Cross-equivalence (crossEq) is the PRC cross-multiplication relation; by K4.10 it agrees with equality of the verifier rationals toRat.
A doubled trace $T$ is the orbit-level object that should match $x+x^{-1}$ for a multiplicative character $x$. The structure PRCDoubledTraceHypotheses packages reciprocity $T(q)\sim T(q^{-1})$, normalization invariance, the d'Alembert law, and fixed values at the unit and two orbits. Zero calibration separately forces $T(0)\sim 0$, which the nonzero d'Alembert identity cannot pin. Quotient respect says equivalent inputs yield equivalent traces.
The linear-root quadratic target asserts that the candidate root $r$ solves $r\cdot(T(q)-r)\sim 1$ off zero. Algebraically that is the monic quadratic whose roots sum to $T(q)$ and multiply to $1$, so the intended identity is $T(q)\sim r+r^{-1}$. This lemma discharges that identity under the listed hypotheses.
proof idea
Introduce $q$ and case on whether $q.\mathrm{toRat}=0$.
Zero case: unfold the candidate (it returns zero), rewrite cross-equivalence as rational equality, and use add/recip/toRat lemmas. Zero calibration gives $(T(0)).\mathrm{toRat}=0$. Cross-equivalence of $q$ with zero plus quotient respect force $(T q).\mathrm{toRat}=(T 0).\mathrm{toRat}$, so both sides are $0$.
Nonzero case: apply traceRootCandidate_recip_toRat_of_nonzero for the sum identity on rational displays, and traceRootCandidate_reciprocal_of_quadratic for $r(q^{-1})\sim r(q)^{-1}$. Transport the reciprocal via crossEq_symm and crossEq_iff_toRat_eq, rewrite the target sum through add_toRat, and finish by ring.
why it matters
Native cost uniqueness in PRC aims to force the cost functional to be the unique J-cost coming from the Recognition Composition Law and the T5 forcing step $J(x)=\cosh(\log x)-1$. Doubled traces are the bridge: if $T$ is a doubled character trace, recovering $T\sim r+r^{-1}$ identifies $T$ with the standard generator of that cost.
This lemma is the algebraic core used by PRCDoubledTraceZeroCalibratedLinearRootTarget_proved, which packages zero calibration with the linear-root target into a single proved interface. Downstream uniqueness arguments cite that package rather than re-proving the root-sum identity. Without the present reduction, the quadratic target would remain an unlinked side condition instead of a genuine reconstruction of the doubled trace from its candidate root.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.