traceRootCandidate_normalized_of_trace_respect
plain-language theorem explainer
If a doubled-trace map on ratio orbits respects cross-equivalence, its trace-root candidate is unchanged (up to cross-equivalence) when the input is replaced by its GCD-normalized representative. Cited when discharging normalization invariance for native-cost uniqueness from doubled-trace data. Proof splits on vanishing of the rational display and reduces both branches to equality of verifier rationals via the respect hypothesis and multiplication by two.
Claim. Let $T$ be a map on ratio orbits that sends cross-equivalent inputs to cross-equivalent outputs. Then for every ratio orbit $q$, the trace-root candidate built from $T$ at $q$ is cross-equivalent (by cross-multiplication) to the same candidate at the GCD-normalized representative of $q$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator: an internal display of a rational, with verifier map toRat. Two ratio orbits are cross-equivalent when cross-multiplication balances as signed orbits; that relation is equivalent to equality of the rational displays (K4.10).
GCD normalization produces a canonical raw representative of a ratio orbit. Quotient-respect for a doubled-trace map $T$ means cross-equivalent inputs yield cross-equivalent $T$-values: equivalent displays must carry equivalent traces.
The trace-root candidate is the algebraic root expression built from $T$ at $q$ and at twice $q$ (with a zero branch when the rational display vanishes). This lemma states that candidate is stable under replacing $q$ by its normalized form, once $T$ respects cross-equivalence. The local module develops uniqueness of the native cost from doubled-trace structure.
proof idea
Fix $q$ and case on whether its rational display is zero.
Zero case: normalization preserves vanishing of toRat. Both sides of the candidate hit the zero branch, so cross-equivalence is immediate after rewriting through the toRat characterization of cross-equivalence.
Nonzero case: normalization keeps the display nonzero. Cross-equivalence of $q$ with its normalize (standard normalize lemma) plus respect of $T$ gives equal toRat values of $T$ at those two inputs. The same for twice $q$ versus twice the normalize, using that multiplication by two preserves cross-equivalence on toRat. Rewrite both candidates via the nonzero toRat formula and substitute the two equalities.
All steps are rewrites through crossEq_iff_toRat_eq, mul_toRat, and the normalize/toRat lemmas; no analytic content.
why it matters
Native-cost uniqueness in PRC needs the doubled-trace root target to be well-defined on the quotient of ratio orbits, not merely on raw displays. This lemma supplies the missing normalization invariance of the root candidate once quotient-respect of $T$ is known.
It is consumed by PRCDoubledTraceZeroCalibratedLinearRootTarget_proved, which packages zero-calibration and linear-root structure for doubled traces into the proved target used by the uniqueness chain. That sits inside the foundation layer that forces the native cost functional (the $J$-cost side of the Recognition Composition Law and the T5 uniqueness landmark), before constants and the mass ladder are read off.
Without this step, root extraction could depend on the choice of representative inside a cross-equivalence class, blocking passage from character data to a unique native cost on orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.