RatioNormalizationTarget
plain-language theorem explainer
Every rational orbit admits a cross-equivalent representative whose absolute numerator is coprime to the denominator. This packages the lowest-terms normalization goal for Euclidean reduction on δ-orbit ratios. Foundation workers cite it when reducing RatioOrbit displays before cost or uniqueness arguments. It is a Prop definition, not a proved theorem; the companion theorem discharges it via normalizeRatio.
Claim. For every rational orbit $q$ (signed numerator over a nonzero orbit denominator), there exists a rational orbit $q'$ such that $q$ and $q'$ are equivalent under cross-multiplication balance and the absolute value of the numerator of $q'$ is coprime to its denominator.
background
In the Primitive Recognition Calculus, a rational orbit is a signed numerator over a nonzero distinction-nat denominator. Two such displays are identified by cross-multiplication: $a$ and $b$ are equivalent when $a.num$ scaled by $b.den$ balances $b.num$ scaled by $a.den$ as signed orbits (the internal PRC rational relation, K4.10).
Object-level coprimality on distinction-nats means the orbit GCD is a unit. Absolute value of a signed orbit is the distinction-nat absolute difference of its positive and negative legs. The local module builds a Euclidean surface (div/mod, GCD fuel) on these orbit positions so ratios can be reduced without leaving the δ-orbit language.
This definition states the normalization target that the Euclidean pass is meant to hit: after signed division by the orbit GCD, a balanced equivalent representative in lowest terms always exists.
proof idea
Definitional packaging only. The body is the universal Prop: for every rational orbit $q$, assert existence of $q'$ with cross-equivalence to $q$ and coprimality of $|q'.num|$ with $q'.den$. No tactics or lemmas run here. The companion theorem ratio_normalization_target later witnesses the Prop by supplying normalizeRatio q and the two lemmas that it preserves cross-equivalence and yields coprime absolute numerator and denominator.
why it matters
This Prop is the named target closed by the Euclidean orbit surface in this module. The theorem ratio_normalization_target proves it, and OrbitEuclideanCertificate bundles the surrounding div/mod display facts for the same pass. Without a lowest-terms representative internal to δ-orbits, later PRC cost uniqueness and rational display arguments would have to carry arbitrary common factors. The declaration sits in the foundation layer that prepares integer and rational orbit arithmetic before the forcing chain (T5 J-uniqueness and RCL) consumes clean ratio data. It does not itself touch J-cost or the phi ladder; it only guarantees reduced rational displays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.