traceRootCandidate_multiplicative_of_trace_respect
plain-language theorem explainer
Under doubled-trace hypotheses and cross-equivalence respect, the trace-root candidate is multiplicative on ratio orbits (up to cross-multiplication equivalence). Cited when closing native PRC cost uniqueness via a calibrated linear root. Proof cases on vanishing rational displays, then runs d'Alembert on (x,y) and (2x,2y) with the fixed value T(2)=5/2 to force the root product identity.
Claim. Let $T$ map ratio orbits to ratio orbits, satisfy the doubled-trace package (reciprocal symmetry, normalization invariance, d'Alembert, $T(1)\equiv 2$, and the native two-trace calibration), and send cross-equivalent inputs to cross-equivalent outputs. Then for all ratio orbits $x,y$, the trace-root candidate obeys $\mathrm{root}_T(xy)\equiv \mathrm{root}_T(x)\cdot\mathrm{root}_T(y)$ under cross-multiplication equivalence.
background
Ratio orbits are the PRC internal displays of rational ratios, built from signed $\delta$-orbit numerators and denominators. Cross-equivalence (crossEq) is the internal cross-multiplication relation; by K4.10 it agrees with equality of the rational verifier displays toRat.
A doubled trace $T$ is meant to behave like $q\mapsto q+q^{-1}$ on those displays: the structure PRCDoubledTraceHypotheses packages reciprocal symmetry, invariance under canonical normalization, the d'Alembert identity $T(x)T(y)\equiv T(xy)+T(x/y)$, unit calibration $T(1)\equiv 2$, and the two-trace matching the native doubled cost. Quotient-respect (PRCDoubledTraceRespectsCrossEq) says equivalent inputs yield equivalent $T$-values.
The trace-root candidate extracts, from such a $T$, a putative multiplicative linear root (the object whose sum with its reciprocal recovers $T$). Multiplicativity of that root is the algebraic step needed before uniqueness of the native cost character.
proof idea
Fix $x,y$ and case on whether toRat vanishes.
If $x=0$ or $y=0$ as rationals, the product orbit is zero; both sides of the claimed cross-equivalence reduce via crossEq_iff_toRat_eq, mul_toRat, and the zero clauses in the root-candidate definition.
In the nonzero branch, first read $T(2)=5/2$ off two_trace and the native doubled-trace formula. Apply d'Alembert to $(x,y)$ and to $(2x,2y)$, after checking the relevant products and quotients stay nonzero. Use quotient-respect on the elementary cross-equivalences $(2x)(2y)\equiv 2\cdot 2\cdot(xy)$ and $(2x)/(2y)\equiv x/y$ to align $T$-values. Algebraic rearrangement of the two d'Alembert identities, together with the calibrated $T(2)$, forces the root-candidate product identity back through crossEq_iff_toRat_eq.
why it matters
This is a load-bearing multiplicativity lemma inside native PRC cost uniqueness. The sole recorded consumer is PRCDoubledTraceZeroCalibratedLinearRootTarget_proved, which assembles quotient-respect, this multiplicativity fact, and a quadratic-root target into the zero-calibrated linear-root statement for doubled traces.
Framework-wise it sits under the J-uniqueness / Recognition Composition Law strand (forcing chain T5 and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$): the doubled trace is the $q+q^{-1}$ avatar of that cost, and a multiplicative linear root is exactly the character that recovers the unique native $J$. Closing this step removes a free functional degree of freedom before the cost is pinned to the RS-native form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.