not_isZero_one
plain-language theorem explainer
The unit class in the primitive recognition calculus rationals fails the choice-free zero test. Anyone building the PRC rational field (or citing K4.8 structural nontriviality) needs this discriminator fact. The proof reduces the balanced-numerator claim to the integer display and obtains 1 = 0, which omega rejects.
Claim. The multiplicative unit of the primitive recognition calculus rationals is not a zero-class element: $\neg\,\mathrm{isZero}(1)$. Equivalently, the numerator of a representative of $1$ does not balance the zero signed orbit under the internal balanced relation.
background
In the IntegerRational layer of Primitive Recognition Calculus, rationals are quotients of ratio-orbits whose numerators and denominators are signed orbit differences. A SignedOrbit is a pair of distinction-nats interpreted as $\mathrm{pos}-\mathrm{neg}$. The map toInt sends such a pair to an ordinary integer verifier display.
The predicate isZero is the choice-free structural zero test on PRCRat: a class is zero iff a representative numerator balances the zero signed orbit. Well-definedness routes through the integer cross-multiplication hub, so the definition depends only on propext and Quot.sound, with no classical ℚ display.
The bridge lemma balanced_iff_toInt_eq (K4.9) equates the internal balanced relation on signed orbits with equality of their integer displays. The simp facts one_toInt and zero_toInt fix those displays at $1$ and $0$ respectively.
proof idea
Assume toward contradiction that isZero one holds. By definition that means the numerator of the unit balances the zero signed orbit. Apply balanced_iff_toInt_eq (forward direction) to convert the balanced hypothesis into equality of integer displays. Rewrite with one_toInt and zero_toInt to obtain $1=0$, then close by omega. Term-mode proof with a single intro, one bridge application, two rewrites, and a linear-arithmetic finish.
why it matters
This is the discriminator half of K4.8 structural nontriviality: zero and one must be distinct as PRC rational classes, proved without ever opening a classical rational display. The immediate parent is zero_ne_one, whose doc-comment states it is "Proved by the choice-free isZero discriminator (no ℚ display)". That nontriviality is the minimal field axiom needed before addition, multiplication, and inversion lemmas on PRCRat can be trusted as a genuine number system rather than a collapsed quotient.
In the broader Recognition foundation this sits under the primitive recognition calculus that feeds the forcing chain: a collapsed $0=1$ would make the later J-cost, phi fixed point, and eight-tick constructions vacuous. The result is fully proved (no sorry), so it closes rather than opens scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.