PRCSignedRatioDecompositionTarget_proved
plain-language theorem explainer
Every nonzero ratio orbit factors, up to cross-equivalence, as a positive directed numerator times a reciprocal directed denominator, or as that positive ratio times the signed unit -1. This is the signed-ratio decomposition needed after pass 279 in native-cost uniqueness. Cite it when lifting signed coherent prime orientation from local characters to global ratio displays. Proof is a two-branch case split on the numerator sign flag, then rational field simplification.
Claim. For every ratio orbit $q$ with nonzero rational display, either there exist nonzero distinction naturals $n,d$ such that $q$ is cross-equivalent to $\mathrm{dir}(n)\cdot\mathrm{dir}(d)^{-1}$, or there exist nonzero $n,d$ such that $q$ is cross-equivalent to $(-1)\cdot\mathrm{dir}(n)\cdot\mathrm{dir}(d)^{-1}$.
background
In the Primitive Recognition Calculus, ratio orbits are the native display of rational comparisons built from distinction naturals and signed orbits. The display map recovers the ordinary rational value; cross-equivalence identifies displays with the same rational content. Directed orbits embed a nonzero distinction natural as a positive ratio generator, and reciprocal is multiplicative inversion on ratio orbits.
The target proposition records the exact signed-ratio decomposition required after pass 279: every nonzero raw ratio is either a positive orbit numerator times the reciprocal denominator, or the signed unit times such a positive ratio. The signed unit is the ratio display of $-1$. Absolute value on signed orbits erases the sign flag and recovers a distinction natural whose integer image is the absolute value of the numerator.
This sits inside the native-cost uniqueness module, which builds the J-cost character from doubled-trace and d'Alembert structure on ratio displays. Upstream recovery maps connect logic integers and naturals to classical $\mathbb{Z}$ and $\mathbb{N}$, so the case split can quote ordinary integer absolute-value identities.
proof idea
Fix a ratio orbit $q$ with nonzero rational display. First show the numerator integer image is nonzero (else the display is zero), then that its absolute distinction natural is nonzero via the signed-orbit absolute-value lemma.
Case on the numerator nonnegativity flag. If true, take $n$ as absolute numerator and $d$ as denominator, and prove cross-equivalence to $\mathrm{dir}(n)\cdot\mathrm{dir}(d)^{-1}$ by rewriting through the cross-equivalence-to-rational criterion, multiplicative and reciprocal display lemmas, and the directed-orbit display lemma. The key cast equates the absolute numerator natural with the nonnegative integer image; field simplification finishes.
If the flag is false, force it to false, take the same $n,d$, and target $(-1)\cdot\mathrm{dir}(n)\cdot\mathrm{dir}(d)^{-1}$. The false-flag lemma gives a negative integer numerator; cast the absolute natural to the negated integer, then field-simplify and normalize numerals.
why it matters
Native cost uniqueness needs a clean factorization of every nonzero ratio display into positive directed generators plus at most one global sign. Without that split, signed characters cannot be reduced to absolute ratio characters plus a coherent orientation of $-1$.
The sole recorded consumer is the theorem that signed coherent prime orientation propagates to the global target, which lifts a signed coherent prime orientation from local character data to every ratio orbit. That parent introduces a character and needs global signed decompositions of the present shape so orientation hypotheses propagate under multiplication and reciprocal.
In the broader Recognition forcing chain this supports T5 J-uniqueness: the native cost is forced to be the unique J satisfying the Recognition Composition Law once ratio displays reduce to positive generators and a single sign bit. The theorem closes the signed-decomposition obligation introduced after pass 279; it does not itself name J or $\varphi$, but it is on the path that makes the cost character well-defined on all nonzero rational orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.