PRCDoubledTraceRespectsCrossEq_of_normalizeRatio_canonical
plain-language theorem explainer
Under the doubled-trace hypotheses for a map T on ratio orbits, plus uniqueness of GCD-normalized representatives for cross-equivalent displays, T respects cross-equivalence: equivalent raw ratios map to equivalent traces. Cited when showing native PRC costs descend to the ratio quotient. Proof chains normalized invariance through the canonical normalizer via refl, symm, and trans of cross-equivalence.
Claim. Let $T$ be a map on ratio orbits satisfying the doubled-trace hypotheses (reciprocal symmetry, invariance under GCD normalization, d'Alembert identity, and fixed unit/two traces). If every pair of cross-equivalent ratio orbits shares the same GCD-normalized representative, then $T$ respects cross-equivalence: $q \sim r$ implies $T(q) \sim T(r)$.
background
Ratio orbits are rational displays: a signed-orbit numerator over a nonzero distinction-nat denominator. Cross-equivalence is the balanced integer relation identifying displays of the same rational (choice-free via an integer bridge; refl/symm/trans are available). DistinctionNat is the base-neutral finite orbit of repeated distinction. The map normalizeRatio divides numerator magnitude and denominator by their native GCD and restores sign via the nonneg flag.
Doubled-trace hypotheses package the structural properties expected of the doubled trace of a native PRC cost: reciprocal symmetry, pointwise invariance under normalization, a d'Alembert equation, and fixed values on the unit and two. The canonical-normalization target asserts that cross-equivalent raw displays yield identical normalizeRatio outputs. As its doc states, this is "the exact quotient-normalization uniqueness statement needed to turn normalized_invariant into general quotient respect."
The local setting is native-cost uniqueness in the Primitive Recognition Calculus: cost data built from characters and doubled traces must be well-defined on ratio classes, not raw representatives.
proof idea
Term proof. Introduce raw displays $q,r$ and a cross-equivalence hypothesis. Chain three crossEq steps with crossEq_trans.
Left leg: normalized_invariant at $q$ gives $T(q)\sim T(\mathrm{normalize},q)$. Middle leg: rewrite by the canonical target so $\mathrm{normalize},q=\mathrm{normalize},r$, then close by crossEq_refl on $T(\mathrm{normalize},r)$. Right leg: crossEq_symm of normalized_invariant at $r$ gives $T(\mathrm{normalize},r)\sim T(r)$. The composite is $T(q)\sim T(r)$.
Only the normalized_invariant field of the hypotheses is used; reciprocal, d'Alembert, and unit/two traces are idle here.
why it matters
Immediate parent is PRCDoubledTraceRespectsCrossEq_proved, which instantiates the canonical-normalization hypothesis by PRCNormalizeRatioCanonicalTarget_proved and obtains unconditional quotient respect for any doubled trace satisfying the native hypotheses. That respect is required so native cost values (doubled traces of ratio characters) are functions of equivalence classes rather than raw displays, a necessary step in the uniqueness argument for the PRC native cost.
In the Recognition Science forcing chain this supports the J-cost uniqueness path (T5 / RCL): costs must depend on the ratio class. The lemma closes the gap between pointwise normalized_invariant and full crossEq-respect without classical choice, matching the choice-free integer-bridge design of crossEq_trans upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.