positive_normalize
plain-language theorem explainer
Normalization of a ratio orbit preserves PRC-native positivity: if q is positive, so is its GCD-reduced form. Anyone building the ordered field structure on ratio orbits cites this when reducing fractions. The proof is a two-step rewrite through the bridge to ordinary rational positivity and the fact that normalization leaves the displayed rational unchanged.
Claim. Let $q$ be a ratio orbit (signed numerator over a nonzero distinction-orbit denominator). If $q$ is positive in the PRC-native sense, then the GCD-normalized ratio orbit of $q$ is likewise positive.
background
In the Primitive Recognition Calculus, rationals are not taken as a primitive type. A RatioOrbit packages a signed orbit numerator with a nonzero DistinctionNat denominator (the base-neutral finite orbit of repeated distinction). Display to ordinary rationals is via toRat.
PRC-native positivity means the signed numerator is nonnegative and not balanced with zero, i.e. strictly positive as an orbit. The companion lemma equates this with ordinary positivity of the displayed rational: positive q if and only if $0 < q.\mathrm{toRat}$.
Normalization divides numerator magnitude and denominator by their native orbit GCD, restoring sign via the nonneg flag. The key upstream fact is that this operation does not change the displayed rational: $(\mathrm{normalizeRatio}, q).\mathrm{toRat} = q.\mathrm{toRat}$.
proof idea
Two rewrites, then the hypothesis. First replace the goal positive (normalizeRatio q) by 0 < (normalizeRatio q).toRat via the positivity bridge. Second replace that displayed value by q.toRat using normalizeRatio_toRat. The resulting inequality 0 < q.toRat is exactly the forward direction of the bridge applied to the assumption positive q.
why it matters
The RationalField module equips ratio orbits with field operations and an order compatible with the PRC cost calculus. Positivity must be stable under the Euclidean reduction that puts fractions in lowest terms; without that, ordered-field lemmas would have to track unreduced representatives.
No downstream consumers are wired yet (used_by is empty), so this is infrastructure for the ordered-field layer rather than a step already named in the T0–T8 forcing chain. It sits under the foundation that later feeds J-cost uniqueness and the Recognition Composition Law, by ensuring the native positive cone is well-defined on orbit rationals independent of representative choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.