isZero_zero
plain-language theorem explainer
The zero primitive-recognition rational lies in the structural zero class: its numerator balances the zero signed orbit. Cited when proving the PRC rationals are nontrivial (zero distinct from one) and when discharging zero-class side conditions. Proof is a one-line wrapper of balance reflexivity at the zero signed orbit.
Claim. The zero class of the primitive recognition calculus rationals satisfies the choice-free zero test: the numerator of the zero rational balances the zero signed orbit (the pair with equal positive and negative distinction-natural components).
background
In the primitive recognition calculus, integers are signed orbits: pairs (pos, neg) of distinction naturals with intended meaning pos - neg. Two signed orbits are balanced when their cross-sums of distinction lengths agree; that is the choice-free stand-in for integer equality. The reflexivity lemma states every signed orbit balances itself.
PRC rationals are a quotient of ratio orbits. The structural zero predicate lifts the test "numerator balances the zero signed orbit" through the quotient. Its doc (K4.8) records that well-definedness routes through the integer cross-multiplication hub and depends only on propext and Quot.sound, with no classical ℚ display.
This module builds that integer/rational layer on top of orbit arithmetic, keeping the foundation choice-free.
proof idea
One-line wrapper. The zero test on the zero class reduces, by definition of the lifted predicate, to balance of the zero signed orbit against itself. Apply the reflexivity theorem for balance at that zero signed orbit; its own proof only unfolds balance and rewrites by commutativity of addition on distinction naturals.
why it matters
Base fact for the K4.8 zero discriminator. The immediate parent is structural nontriviality: zero and one are distinct classes, proved by rewriting along a hypothetical equality and feeding this fact into the companion not_isZero_one. Without the zero class actually passing the zero test, that discriminator cannot fire.
The lemma lives in the IntegerRational layer of PrimitiveRecognitionCalculus, the arithmetic substrate under later foundation constructions. It does not itself touch the forcing chain (T5 J-uniqueness, T6 phi, T7 eight-tick, T8 D=3) or the RCL; those sit higher. It simply locks the zero end of the choice-free rational tests so downstream nontriviality and arithmetic lemmas have a clean base case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.