traceRootCandidate_quadratic_of_trace_respect
plain-language theorem explainer
Under doubled-trace hypotheses plus quotient respect, the trace-root candidate for any nonzero ratio orbit q multiplies with its T(q)-complement to the unit orbit (cross-equivalence). Cited by anyone closing native PRC cost uniqueness via linear-root calibration of the doubled trace. Proof evaluates d'Alembert on (2,2), (q,q), and (2q,2/q), then reduces all identities through rational displays.
Claim. Let $T$ map ratio orbits to ratio orbits, satisfy the doubled-trace package (reciprocity, normalization invariance, d'Alembert identity, $T(1)\sim 2$, and the fixed two-trace calibration), and respect cross-multiplication equivalence. Then for every ratio orbit $q$ with $q\neq 0$ as a rational display, $\mathrm{root}(T,q)\cdot\bigl(T(q)-\mathrm{root}(T,q)\bigr)\sim 1$, where $\sim$ is cross-equivalence of ratio orbits.
background
Ratio orbits are the PRC internal display of rationals: a signed-orbit numerator over a nonzero distinction-nat denominator. Cross-equivalence is the internal cross-multiplication relation; by the IntegerRational bridge it agrees exactly with equality of the rational verifier displays toRat.
The doubled trace $T$ is the character-side object attached to a native PRC cost. Its hypothesis package demands reciprocity $T(q)\sim T(1/q)$, invariance under GCD normalization, the multiplicative d'Alembert identity, unit calibration $T(1)\sim 2$, and a fixed two-trace value. Quotient respect says equivalent displays carry equivalent traces.
The linear-root quadratic target asserts that the designated root candidate and its complement under $T(q)$ multiply to the unit orbit. Algebraically this is the statement that the candidate solves $X\cdot(T(q)-X)=1$, i.e. the monic quadratic $X^2-T(q)X+1=0$ whose roots are the classical $x+1/x$ pair for the doubled character.
proof idea
Tactic proof by direct evaluation on rational displays. First read off $T(2)=5/2$ and $T(1)=2$ from the two-trace and unit-trace hypotheses via crossEq_iff_toRat_eq and the toRat homomorphism lemmas (add_toRat, mul_toRat, one_toRat).
Apply d'Alembert at $(2,2)$: since $2/2\sim 1$ and respect identifies $T(2/2)$ with $T(1)$, obtain $T(4)=17/4$. The same identity at $(q,q)$ with $q/q\sim 1$ yields the Chebyshev relation $T(q^2)=T(q)^2-2$.
Form the pair $(2q,,2/q)$. Cross-equivalence identities (again via toRat and field simplification) give $(2q)\cdot(2/q)\sim 4$ and $(2q)/(2/q)\sim q^2$. Respect transfers these to $T$-values. Feed the pair into d'Alembert, substitute the known values, and rearrange: the product of the root candidate with $T(q)$ minus that candidate is cross-equivalent to $1$, which is the target.
why it matters
This lemma is the algebraic heart of the linear-root calibration step inside native PRC cost uniqueness. Downstream it is invoked by PRCDoubledTraceZeroCalibratedLinearRootTarget_proved, which packages the zero-calibrated form of the same quadratic target used to pin the doubled trace to the unique native character.
In the Recognition forcing chain this sits under T5 (J-uniqueness): the doubled trace is the $x+x^{-1}$ (equivalently $2\cosh\log$) avatar of the cost, and the quadratic $X^2-T(q)X+1=0$ is exactly the characteristic equation forcing that avatar. Establishing the root product identity under only the d'Alembert package plus quotient respect closes the gap between abstract functional hypotheses and the concrete native cost on ratio orbits.
Without this step, zero-calibration and uniqueness of the native cost character remain conditional on an unproved root identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.