PRCDoubledTraceRespectsCrossEq_proved
plain-language theorem explainer
Any doubled-trace map on ratio orbits that satisfies the native PRC doubled-trace hypotheses respects cross-equivalence: equivalent displays get equivalent traces. Cost-uniqueness arguments cite this to treat the doubled trace as well-defined on the quotient. The proof is a one-line application of the canonical-normalization bridge plus the already-proved normalization uniqueness target.
Claim. Let $T$ map ratio orbits to ratio orbits and satisfy the native doubled-trace hypotheses (reciprocal symmetry, invariance under GCD normalization, d'Alembert identity, and the unit/two calibration conditions). Then $T$ respects cross-equivalence: whenever two ratio orbits $q$ and $r$ are cross-equivalent, $T(q)$ and $T(r)$ are cross-equivalent.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer-numerator / nonzero-denominator display of a rational scale factor. Cross-equivalence identifies displays that represent the same rational after sign and cancellation, so cost and trace data must be stated on the quotient.
The doubled trace $T$ is the orbit-level object extracted from a native PRC cost. The structure of doubled-trace hypotheses packages the algebraic constraints inherited from that cost: reciprocal symmetry $T(q)\sim T(q^{-1})$, invariance under native GCD normalization, a d'Alembert functional equation, and fixed calibrations at the unit and at two.
Quotient-respect is the missing glue: without it, $T$ is only a function of raw displays. The module isolates a canonical-normalization target stating that cross-equivalent raw displays normalize to the same representative; that target turns the built-in normalized-invariance hypothesis into full cross-equivalence respect.
proof idea
One-line term wrapper. Apply the bridge lemma that derives quotient-respect from the doubled-trace hypotheses plus the canonical-normalization target, supplying the already-proved instance of that target (itself obtained from uniqueness of reduced sign-canonical ratio representatives).
No extra case analysis appears at this layer: the bridge lemma does the work of routing an arbitrary cross-equivalence through normalization and invoking normalized invariance of $T$.
why it matters
This closes the quotient-well-definedness step for doubled traces inside native cost uniqueness. Downstream, the zero-calibrated linear-root target proof invokes it immediately: once $T$ respects cross-equivalence, one can pass to quadratic/root identities on the quotient and force the calibrated linear root that pins the native cost.
In the broader Recognition forcing chain this is infrastructure for J-uniqueness (T5): the native cost is the discrete precursor of $J(x)=(x+x^{-1})/2-1$, and doubled-trace quotient respect is required before uniqueness and calibration arguments can speak about rationals rather than raw displays. It does not itself name $J$ or $\phi$; it clears the display-vs-quotient obstruction those later steps need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.