ratio_normalization_target
plain-language theorem explainer
Every ratio orbit admits an equivalent representative whose absolute numerator is coprime to the denominator, obtained by dividing out the native orbit GCD. Anyone assembling the Euclidean orbit surface certificate cites this existence claim. The proof is a one-line packaging of the constructive normalizer with its cross-equality and coprimality lemmas as the existential witness.
Claim. For every ratio orbit $q$ there exists a ratio orbit $q'$ such that $q$ and $q'$ are cross-equal (they represent the same rational) and $\gcd(|q'.\mathrm{num}|, q'.\mathrm{den}) = 1$.
background
In the primitive recognition calculus, a ratio orbit is a signed-numerator / positive-denominator pair carrying a rational value on the discrete orbit surface. Two orbits are cross-equal when their cross-multiplied integer forms agree, equivalently when they map to the same rational.
The Euclidean layer on this surface supplies a native GCD for orbit integers (via fuel-bounded division and remainder). The normalizer divides absolute numerator and denominator by that GCD and restores sign through the nonnegativity flag on the signed quotient, yielding a balanced representative.
The target proposition simply asserts that every orbit has some cross-equal representative whose absolute numerator is coprime to the denominator. Upstream lemmas already prove that the concrete normalizer is cross-equal to its input and that the normalized pair is coprime.
proof idea
Term-style packaging after a single introduction. Fix an arbitrary ratio orbit $q$. Instantiate the existential with the constructive normalizer of $q$. Discharge the two conjuncts by the already-proved facts that the normalizer is cross-equal to $q$ and that the absolute numerator of the normalizer is coprime to its denominator. No further arithmetic is performed at this layer.
why it matters
This is the existence half of signed-rational normalization on the $\delta$-only Euclidean orbit surface. Downstream it is consumed by the orbit Euclidean certificate, whose doc-comment lists "signed-rational normalization by native orbit GCD" among the closed surface properties (alongside divmod display, remainder bound, and quotient-remainder decomposition).
In the broader Recognition stack the certificate sits inside Primitive Recognition Calculus: discrete orbits must reduce to coprime balanced fractions before they feed higher forcing and self-reference layers. The result does not itself invoke J-cost, $\varphi$, or the eight-tick octave; it is pure arithmetic hygiene on the orbit surface those later steps rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.