zero_not_crossEq_one
plain-language theorem explainer
Zero and one are inequivalent as ratio orbits under cross-multiplication: the signed-orbit products that would witness 0 ~ 1 never balance. Anyone building the internal order or rational display on δ-orbits cites this separation. The proof is a one-line symmetry flip of the already-proved one-not-zero fact.
Claim. As ratio orbits, $0$ and $1$ are not related by cross-multiplication: $\neg\,\mathrm{crossEq}(0,1)$, i.e. the signed products that would equate them as rationals do not balance.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator (a signed orbit) over a nonzero distinction-nat denominator. Two such displays are related by crossEq when the cross-multiplied numerators balance as signed orbits: $a_{\mathrm{num}}\cdot b_{\mathrm{den}}$ balances $b_{\mathrm{num}}\cdot a_{\mathrm{den}}$. That relation is the internal PRC stand-in for rational equality, defined entirely on δ-orbit positions (K4.10).
The sibling fact one_not_crossEq_zero already shows that the unit orbit is not cross-equivalent to the zero orbit, by reducing cross-equality to ordinary rational equality of the verifier displays and applying norm_num. Symmetry of cross-equality is immediate from symmetry of signed-orbit balance.
This module develops the integer order surface on those same orbit displays: nonnegativity flags, truncated subtraction, and the order certificate that packages the display lemmas.
proof idea
Assume crossEq zero one. Symmetry of cross-equality (crossEq_symm) yields crossEq one zero. That directly contradicts the sibling theorem one_not_crossEq_zero, which already rules out the swapped pair by reducing to toRat equality and a numeric check. The whole argument is therefore a one-line symmetry flip; no new arithmetic is done here.
why it matters
Separating the zero and unit ratio orbits is a basic integrity check for the internal rational and order layers. Without it, the signed-orbit order could collapse 0 and 1 under the same cross-multiplication relation used for rational equality.
The sole recorded consumer is integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate bundles display lemmas (truncated subtraction, leq, absolute difference, nonnegativity flags) into a single closed package. This inequivalence is one of the elementary non-degeneracy facts that keep that package coherent.
In the broader Recognition forcing chain this sits in the foundation layer beneath cost uniqueness and the J-functional; it does not itself force φ, the eight-tick octave, or D = 3, but it keeps the rational orbit language non-degenerate so those later steps can talk about distinct rungs and costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.