traceRootCandidate_one_of_trace_respect
plain-language theorem explainer
Under doubled-trace hypotheses and cross-equivalence respect, the root candidate extracted from a doubled trace at the unit ratio orbit is itself the unit orbit. Used when calibrating the linear root of a native PRC cost against the zero-calibration target. The proof evaluates the candidate on rational displays via unit and two-trace normalizations and finishes by arithmetic.
Claim. Let $T$ send ratio orbits to ratio orbits. Assume $T$ satisfies the doubled-trace hypotheses (reciprocal symmetry, normalization invariance, d'Alembert identity, unit trace $T(1)\sim 2$, and two-trace matching the native doubled cost at $2$) and that cross-equivalent inputs yield cross-equivalent $T$-values. Then the trace root candidate of $T$ at the unit orbit is cross-equivalent to the unit orbit.
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 K4.10 it agrees with equality of the verifier rationals toRat.
A doubled trace $T$ is a map on ratio orbits meant to carry the doubled native cost (the quantity that for the classical $J$-cost behaves like $x+x^{-1}$). The structure PRCDoubledTraceHypotheses packages the structural laws: reciprocal symmetry, invariance under GCD normalization, the d'Alembert functional equation, unit normalization $T(1)\sim 2$, and the two-trace calibration against the native doubled cost.
Quotient-respect (PRCDoubledTraceRespectsCrossEq) demands that cross-equivalent displays carry cross-equivalent traces. The root candidate is the algebraic extraction of a linear root from that doubled value; at the unit this root is forced to be the unit itself once the calibrations hold.
proof idea
Work entirely through crossEq_iff_toRat_eq and the ring morphisms mul_toRat, add_toRat, one_toRat.
First, $2\cdot 1\sim 2$ by direct rational arithmetic, so quotient-respect gives $T(2\cdot 1)\sim T(2)$. The two-trace hypothesis, unfolded through nativeCostDoubledTrace and doubledTraceValue, forces $(T,2).\mathrm{toRat}=5/2$. The unit-trace hypothesis forces $(T,1).\mathrm{toRat}=2$.
Apply the nonzero evaluation lemma for the root candidate at the unit, substitute the three rational values, and close with norm_num: the candidate's display equals $1$, hence is cross-equivalent to the unit orbit.
why it matters
This is a calibration lemma inside native PRC cost uniqueness: it pins the root candidate of any doubled trace that obeys the structural hypotheses to the unit at the unit input. Downstream, PRCDoubledTraceZeroCalibratedLinearRootTarget_proved invokes it (after proving quotient-respect from the hypotheses) as part of establishing the zero-calibrated linear-root target for doubled traces.
In the broader Recognition chain this supports uniqueness of the native cost that realizes the Recognition Composition Law and the T5 $J$-cost $J(x)=(x+x^{-1})/2-1$. The doubled display is the natural lift $x+x^{-1}$; forcing its unit root to be $1$ is the base point of the linear-root calibration that distinguishes the genuine cost from other d'Alembert solutions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.