one_not_crossEq_zero
plain-language theorem explainer
The unit ratio orbit is not cross-equivalent to the zero ratio orbit under the PRC cross-multiplication relation. Anyone assembling the ordered field surface on integer and rational orbits cites this separation of 1 from 0. The proof rewrites cross-equality to equality of verifier rationals and discharges 1 ≠ 0 by norm_num.
Claim. The unit ratio orbit is not cross-equivalent to the zero ratio orbit: $\neg\,\mathrm{crossEq}(1,0)$. Equivalently, their verifier displays disagree as rationals, since $\mathrm{toRat}(1)=1$ and $\mathrm{toRat}(0)=0$.
background
In the Primitive Recognition Calculus, a RatioOrbit is an integer numerator (signed orbit) over a nonzero distinction-nat denominator. It is the internal display of a rational before any external ℚ is assumed. Two such orbits are related by crossEq when the scaled products of numerator and denominator balance as signed orbits: $a.num\cdot b.den$ balances $b.num\cdot a.den$. That is the PRC-native stand-in for rational equality (K4.10).
The bridge lemma crossEq_iff_toRat_eq states that cross-multiplication agrees with equality of the verifier displays toRat. The unit and zero orbits are the canonical displays with one.toRat = 1 and zero.toRat = 0. The local module builds the order surface on these integer and rational orbits; separating 1 from 0 is the first non-degeneracy fact for that order.
proof idea
Term-mode rewrite chain. First apply crossEq_iff_toRat_eq to replace crossEq one zero by one.toRat = zero.toRat. Then simplify with the simp lemmas one_toRat and zero_toRat, obtaining the goal 1 = 0 over ℚ. Close by norm_num. No induction or case split; pure transport to the verifier and a numeric contradiction.
why it matters
Feeds the symmetric fact zero_not_crossEq_one (via crossEq_symm) and sits in the dependency cone of integer_order_certificate, whose doc-comment records that "the internal signed-orbit order surface is closed." Without 1 ≁ 0 the order and field certificates on ratio orbits would collapse. In the broader Recognition stack this is foundation plumbing under the forcing chain: before J-cost uniqueness (T5), φ, or the eight-tick octave can be stated on rational displays, the native rationals must distinguish unit from zero. It is a proved non-degeneracy lemma, not scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.