PRCSignedRatioDecompositionTarget
plain-language theorem explainer
Every nonzero ratio orbit is cross-equivalent either to a positive ratio built from distinction-orbit directions, or to that form times the signed unit display of -1. Native-cost uniqueness and character-trace arguments cite this as the exact signed decomposition target after pass 279. The declaration only packages that statement as a Prop; the proof lives in the companion theorem.
Claim. For every ratio orbit $q$ whose verifier display is a nonzero rational, either there exist nonzero distinction naturals $n,d$ such that $q$ is cross-equivalent (via balanced scaled signed orbits) to the product of the orbit direction of $n$ with the reciprocal of the orbit direction of $d$, or the same holds after left-multiplying by the ratio-orbit display of $-1$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator (signed orbit) over a nonzero distinction-natural denominator. Distinction naturals are the base-neutral finite orbit of repeated distinction. The verifier map toRat sends a ratio orbit to an ordinary rational; the internal equality relation is cross-equivalence: two ratio orbits match when the cross-multiplied signed orbits balance (K4.10).
Reciprocal on ratio orbits is total and sends zero to zero, matching $\mathbb{Q}$. Orbit direction lifts a nonzero distinction natural to a positive ratio-orbit generator. The signed unit is the ratio-orbit display of $-1$, introduced to expose missing signed-unit calibration in prime-to-global orientation propagation.
This module packages native-cost uniqueness targets. The present definition isolates the signed-ratio decomposition needed after pass 279: every nonzero raw ratio is a positive orbit fraction, or that fraction times the signed unit.
proof idea
Definitional packaging only: the body is the universal Prop over ratio orbits with nonzero verifier display, split as a disjunction of two existential blocks (positive $n/d$ form versus signed-unit times that form), each witnessed by nonzero distinction naturals and cross-equivalence. No tactics or lemmas are applied here; discharge is deferred to the companion proved theorem.
why it matters
This target is the exact signed-ratio decomposition required after pass 279 for native-cost uniqueness in PRC. The companion theorem PRCSignedRatioDecompositionTarget_proved discharges it, so downstream cost-from-character and doubled-trace matching can treat every nonzero ratio as oriented positive fraction or signed-unit times positive fraction.
That orientation step closes a gap in prime-to-global sign propagation: without the $-1$ case, cross-equivalence alone would miss negative verifier displays. In the broader Recognition forcing chain this sits under foundation work that feeds J-cost uniqueness (T5) and the Recognition Composition Law, by ensuring rational orbit displays used in cost characters are fully classified up to sign before uniqueness arguments run.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.