traceRootCandidate_reciprocal_of_quadratic
plain-language theorem explainer
Under doubled-trace hypotheses, quotient respect, and the linear-root quadratic target, the root candidate of a reciprocal ratio equals (cross-equivalence) the reciprocal of the root candidate. Anyone proving that the candidate is a genuine reciprocal root of the doubled-trace quadratic will cite this. The proof splits on zero versus nonzero rational display and finishes by field simplification of the quadratic identity.
Claim. Let $T$ map ratio orbits to ratio orbits. Assume $T$ satisfies the doubled-trace package (reciprocity, normalization invariance, d'Alembert, unit and two traces), respects cross-equivalence, and meets the linear-root quadratic target: for every nonzero $q$, if $r$ is the trace-root candidate at $q$ then $r\cdot(T(q)-r)\sim 1$. Then for every ratio orbit $q$, the root candidate at the reciprocal of $q$ is cross-equivalent to the reciprocal of the root candidate at $q$.
background
In the Primitive Recognition Calculus, ratio orbits are the internal rational displays built from signed $\delta$-orbits. Cross-equivalence (crossEq) is the PRC stand-in for rational equality: two orbits match when cross-multiplication balances, and this is equivalent to equality of their verifier rationals (toRat).
A doubled trace $T$ is a map on ratio orbits meant to encode twice the native cost character. The structure PRCDoubledTraceHypotheses packages reciprocity $T(q)\sim T(1/q)$, invariance under GCD normalization, a d'Alembert functional equation, and fixed values at the unit and at two. Quotient respect requires that cross-equivalent inputs yield cross-equivalent traces.
The linear-root quadratic target says the candidate root $r$ at nonzero $q$ solves $r(T(q)-r)\sim 1$, i.e. $r$ is a root of $x^2-T(q)x+1=0$. That monic reciprocal quadratic is the algebraic signature of a cost whose generating character is of J-type (the T5 uniqueness shape $J(x)=(x+x^{-1})/2-1$).
proof idea
Fix $q$ and case-split on whether $q.\mathrm{toRat}=0$.
Zero case: reciprocity of the display sends the reciprocal orbit to zero as well. Both sides of the claimed cross-equivalence evaluate the root-candidate definition on the zero branch, and the resulting rationals match by direct computation (crossEq_iff_toRat_eq, recip_toRat, zero_toRat).
Nonzero case: invoke the auxiliary identity that the candidate at the reciprocal has rational display equal to the reciprocal of the candidate sum data, together with the quadratic target at $q$. Rewrite everything in toRat via mul_toRat, sub_toRat, one_toRat, and recip_toRat. Non-vanishing of the candidate's rational follows by contradiction from the quadratic (else $0\cdot(T-0)=1$). field_simp then reduces the claim exactly to the quadratic identity.
why it matters
Native PRC cost uniqueness aims to force the doubled trace (and hence the cost) to be the unique J-shaped character on ratio orbits. The root candidate is the algebraic device that extracts the "$x$" factor in $x+1/x$ from the doubled trace $T\sim x+1/x$. Reciprocity of that candidate is mandatory: without it the candidate cannot consistently serve as a multiplicative character root.
Downstream, traceRootCandidate_trace_of_quadratic uses this lemma to relate the candidate back to the trace itself, and PRCDoubledTraceZeroCalibratedLinearRootTarget_proved folds it into the zero-calibrated linear-root package that closes the uniqueness chain. In the broader Recognition forcing ladder this is local algebraic support for T5 (J-uniqueness) inside the PRC native-cost development, not a global physics derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.