PRCDoubledTraceRespectsCrossEq
plain-language theorem explainer
A map on ratio-orbit displays respects cross-equivalence when it sends cross-equivalent inputs to cross-equivalent outputs. Anyone proving that a doubled-trace operator descends to the rational quotient cites this predicate. It is a one-line Prop abbreviation, not a proved statement.
Claim. A map $T$ from ratio orbits to ratio orbits respects cross-equivalence when, for all ratio orbits $q,r$, if $q$ and $r$ are cross-equivalent (cross-multiplication balances as signed orbits), then $T(q)$ and $T(r)$ are cross-equivalent.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator: the internal display of a rational. Two such displays are cross-equivalent when scaled numerators balance under cross-multiplication, the PRC stand-in for ordinary rational equality.
Doubled-trace constructions act on these raw displays before any quotient is taken. For a cost or root candidate built from such a map $T$ to be well-defined on rationals, $T$ must send cross-equivalent pairs to cross-equivalent pairs. Upstream, native GCD normalization already preserves the PRC cost via normalized_invariant, which equates a ratio to its normalized representative under cross-equivalence.
This module packages native-cost uniqueness for doubled traces. The present definition is the exact quotient-respect interface those uniqueness arguments quantify over.
proof idea
No proof: this is a Prop-valued definition. The body is the universal statement that cross-equivalence of inputs implies cross-equivalence of $T$-images. Downstream theorems discharge it from doubled-trace hypotheses plus canonical normalization, or assume it as a hypothesis when deriving multiplicative and reciprocal laws for trace-root candidates.
why it matters
Quotient-respect is the gate between raw orbit arithmetic and well-defined rational cost. It feeds the proved discharge PRCDoubledTraceRespectsCrossEq_proved (via canonical normalize-ratio) and the conditional form under native hypotheses. From there it unlocks the trace-root candidate laws: normalization invariance, the unit value at one, multiplicativity, and the quadratic/reciprocal identities used in zero-calibrated linear-root uniqueness.
In the Recognition chain this sits under native J-cost uniqueness (T5 territory: $J(x)=(x+x^{-1})/2-1$). Without cross-equivalence respect, doubled-trace costs would depend on the representative, blocking the identification of the unique d'Alembert cost on the ratio quotient. Parent targets include PRCDoubledTraceZeroCalibratedLinearRootTarget_proved and the family of traceRootCandidate_*_of_trace_respect lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.