isZero_mk
plain-language theorem explainer
On a primitive-recognition rational built from a ratio-orbit representative, membership in the zero class is definitionally the same as the numerator balancing the zero signed orbit. Anyone simplifying zero tests in PRC rational arithmetic cites this simp lemma. The proof is pure definitional reflexivity of ↔ from the quotient-lift definition of the zero predicate.
Claim. For every ratio orbit $q$ (signed-orbit numerator over a nonzero distinction-nat denominator), the PRC rational class of $q$ is zero if and only if the numerator of $q$ is balanced against the zero signed orbit: $q_{\mathrm{num}}.\mathrm{pos}+0=0+q_{\mathrm{num}}.\mathrm{neg}$ in orbit lengths.
background
In Primitive Recognition Calculus, integers are signed orbits: pairs of distinction-nats read as $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; that is the internal integer equality, stated entirely on $\delta$-orbit positions (K4.9).
Rationals are ratio orbits: a signed numerator over a nonzero distinction-nat denominator (K4.7), then quotiented to PRC rationals. The zero test is choice-free: a PRC rational lies in the zero class exactly when a representative numerator balances the zero signed orbit. Well-definedness of that lift uses only the integer cross-multiplication hub, depending on ${\mathrm{propext},\mathrm{Quot.sound}}$ and never a classical $\mathbb{Q}$ display (K4.8).
This module sits under Foundation, importing orbit arithmetic so ledger-style bookkeeping can stay native to orbit lengths.
proof idea
One-line wrapper: Iff.rfl. The zero predicate is defined as the quotient lift of exactly SignedOrbit.balanced q.num SignedOrbit.zero, so applying it to mk q is definitionally that balance statement; no further lemma is needed.
why it matters
Gives the canonical simp reduction for zero-class membership on PRC rationals: unfold the class constructor and land on orbit balance. That keeps later arithmetic and cost arguments inside the choice-free K4.8 interface rather than classical rationals.
No recorded downstream users yet; the lemma is infrastructure for any proof that must discharge or rewrite isZero after building a rational from a ratio orbit. In the broader Recognition stack it supports foundation work that treats integers and rationals as orbit data before J-cost, RCL, and the T5–T8 forcing chain are applied. It does not itself touch mass ladders or coupling constants; it only locks the zero test to the balanced-orbit relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.