negativeOneRatio_ne_one
plain-language theorem explainer
The ratio-orbit display of −1 is distinct from the unit ratio orbit. Anyone calibrating absolute-value native cost on signed units cites this separation. The proof transports an assumed equality through the rational display map and reduces to −1 = 1, which fails by norm_num.
Claim. The ratio orbit representing $-1$ is not equal to the multiplicative unit ratio orbit (the orbit whose rational display is $1$).
background
In the primitive recognition calculus, rationals are carried as RatioOrbit values: a signed-orbit numerator over a nonzero distinction-nat denominator. The verifier map toRat sends such an orbit to an ordinary rational by integer division; equality of orbits is often checked after this transport (cross-multiplication is the internal characterization).
negativeOneRatio is the concrete ratio-orbit display of $-1$, built via ratioOrbitOfRat (-1). Its simp lemma records negativeOneRatio.toRat = -1. The unit orbit RatioOrbit.one similarly satisfies one.toRat = 1. The surrounding module develops native-cost uniqueness and character calibration; signed-unit calibration is exactly the place where $-1$ must be distinguished from $1$, because prime-direction data alone does not force that orientation.
proof idea
Assume negativeOneRatio = RatioOrbit.one. Apply congrArg RatioOrbit.toRat to obtain equality of rational displays. Rewrite with the simp facts negativeOneRatio_toRat and RatioOrbit.one_toRat, yielding $-1 = 1$ in $\mathbb{Q}$. Discharge by norm_num. Five-line contradiction; no deeper lemmas.
why it matters
Downstream, absValueGeneratedNativeCost_negative_one_zero uses this inequality in the if_neg branch of the absolute-value generated native cost: because the input is not the unit orbit, the cost falls through to the character evaluation, which at $-1$ is zero (cross-equal to the zero orbit). That step is part of native-cost uniqueness for absolute-value characters in the PRC stack, closing the signed-unit calibration gap that prime-to-global orientation propagation cannot force alone. It sits under the foundation forcing chain that later pins J-cost uniqueness (T5) and the Recognition Composition Law, by ensuring the cost functional sees the correct signed unit before global identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.