negativeOneRatio
plain-language theorem explainer
Canonical ratio-orbit representative of the rational −1 inside the PRC native-cost interface. Downstream uniqueness and minimality proofs cite it as the signed-unit test point that absolute-value and other unsigned costs fail. The definition is a one-line section of −1 through the rational-to-orbit embedding.
Claim. Let $\mathrm{RatioOrbit}$ be the display of a signed integer numerator over a nonzero distinction-nat denominator. Define $\mathrm{negativeOneRatio}$ to be the image of the rational $-1$ under the verifier-backed section $\mathbb{Q}\to\mathrm{RatioOrbit}$.
background
In the Primitive Recognition Calculus, costs and characters act on ratio orbits rather than bare rationals. A RatioOrbit packages a signed numerator orbit with a nonzero distinction-nat denominator (K4.7), so that reciprocal and cross-equality identities can be stated without leaving the native ledger.
The helper ratioOrbitOfRat is deliberately not a new PRC primitive: it is a verifier-backed section $\mathbb{Q}\to\mathrm{RatioOrbit}$ used to probe whether the current character interface already admits classical rational countermodels. Feeding it $-1$ yields the signed unit in orbit language.
The surrounding module develops native-cost uniqueness and minimality for PRC characters (J-cost style reciprocal costs on ratio orbits). Signed-unit calibration is the load-bearing field that separates the canonical cost from absolute-value and other unsigned competitors.
proof idea
One-line definitional wrapper: apply ratioOrbitOfRat to the rational literal $-1$. No further proof obligations; the section constructs numerator and denominator distinction-nats from the integer parts of $-1$ and records the nonzero-denominator witness.
why it matters
This constant is the standard probe for signed-unit calibration across the native-cost ledger. Downstream, PRCSlimSansSignUniquenessTarget_refuted applies uniqueness hypotheses to the absolute-value cost at this orbit and obtains a contradiction, proving the sign field cannot be dropped. Structural results such as absValueGeneratedNativeCost_not_signReversing and signReversing_forces_signed_unit evaluate sign-reversal at the pair (one, negativeOneRatio). Calibration theorems (twoAdicGeneratedNativeCost_signed_unit, zero-calibrated strengthened uniqueness, canonical selection) use the same orbit to check that a cost sends $-1$ to the expected signed unit value.
In framework terms this is the discrete witness that orientation (sign) is forced once base, pair, and zero calibration are present: without it, prime-to-global orientation propagation is incomplete and J-uniqueness (T5-style reciprocal cost) fails to pin the signed character.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.