isZero
plain-language theorem explainer
A PRC rational is zero exactly when a ratio-orbit representative has numerator balancing the zero signed orbit. This is the choice-free structural zero test on the cross-multiplication quotient, cited by field-axiom lemmas and by CPT procedure-space soundness. Well-definedness routes through the integer cross-multiplication hub and cancels nonzero denominators, using only propext and Quot.sound.
Claim. Define a predicate on PRC rationals by lifting, along the cross-multiplication quotient, the property that the numerator signed orbit of a representative is balanced against the zero signed orbit. Equivalently, a class is zero iff that numerator has integer display $0$. The lift is independent of representative.
background
PRC rationals are quotient classes of ratio orbits with nonzero denominator, identified when numerators and denominators cross-multiply equally at the orbit level. The constructor sends a ratio orbit to its class; arithmetic is built without a classical $\mathbb{Q}$ display as the primary object.
Signed-orbit balance is the internal integer relation: two signed orbits $a,b$ satisfy $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. The bridge theorem states this holds iff their integer displays agree. The zero signed orbit is the neutral element of that display.
The local setting (K4.8) builds rationals and a structural zero test from $\delta$-orbit data alone. Upstream maps toNat/toInt recover ordinary $\mathbb{N}$/$\mathbb{Z}$ only as conservative verifiers; the zero test itself stays on orbits and balance.
proof idea
The body is a Quot.lift of the representative predicate "numerator balances zero signed orbit". The respect proof takes a cross-equivalence $h$ between ratio orbits $a,b$, rewrites it via the cross-multiplication iff to an integer cross identity, and records that both denominators have nonzero toNat (hence nonzero as integers).
It then applies propext to the two balance statements, rewrites each by balanced_iff_toInt_eq and zero_toInt, and proves the resulting integer equalities by transporting $0$ across the cross identity and canceling the nonzero denominator factor with Int.eq_of_mul_eq_mul_right (using Int.zero_mul on the zero side).
why it matters
This discriminator is the structural zero test for PRC rationals: simp lemmas give the constructor form, reflexivity shows the zero class is zero, and a short omega argument shows the unit class is not. Downstream field work cites it for a choice-free $0\neq 1$ and for distributivity packaging in the rational field layer.
In verification, CPT procedure spaces and soundness are parameterized by zero/nonzero predicates; domination and optimality results (including the $\phi^\star$ procedure-space membership) thread this zero test as the concrete $X\to\mathrm{Prop}$ instance. Within the foundation chain it closes K4.8's need for a quotient-level zero without classical choice or a primary $\mathbb{Q}$ carrier, keeping the arithmetic stack aligned with orbit-first Recognition constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.