iff
plain-language theorem explainer
Defines the zero-test for a logic-rational via its integer representative: the class is zero exactly when a numerator balances the zero signed orbit. Well-definedness is routed only through integer cross-multiplication and quotient soundness, never a displayed ℚ. Anyone building arithmetic on signed orbits or discharging zero goals in the primitive recognition calculus would cite it. The body is a definitional class/abbrev, not a tactic proof.
Claim. A logic-rational $q$ is the zero class if and only if, for a representative pair $(a,b)$ with $b\neq 0$, the numerator $a$ balances the zero signed orbit (equivalently $a$ is the zero logic-integer). Equality of representatives is the integer cross-multiplication relation $a\cdot d=c\cdot b$; the predicate is well-defined on the quotient and depends only on propositional extensionality and quotient soundness.
background
The module sits in the primitive recognition calculus layer that rebuilds integers and rationals from logical/orbit data rather than from a classical ℤ/ℚ display. Sibling material introduces signed orbits, the map sending a signed orbit to a logic-integer, and the zero signed orbit with its image under that map.
Upstream, integers-from-logic soundness says that if $a+d=c+b$ on logic-naturals then the corresponding integer quotient classes coincide. Rationals-from-logic soundness lifts the same idea: if $a\cdot d=c\cdot b$ with nonzero denominators then the rational classes coincide. Both are thin wrappers around Quotient.sound.
The local convention is to keep every well-definedness argument on the integer cross-multiplication hub, so no Hilbert or ℚ display is required for this zero characterization.
proof idea
There is no tactic proof body: the declaration is a class or definitional abbreviation. It packages the biconditional "rational class is zero ↔ representative numerator balances the zero signed orbit" and records that well-definedness factors through the integer cross-multiplication relation. Discharge of representative independence is intended to invoke the rationals-from-logic and integers-from-logic soundness lemmas (both Quotient.sound wrappers), together with propext where the Prop-level biconditional must be transported across quotient equality.
why it matters
In Recognition Science the forcing chain and cost calculus need a clean arithmetic substrate built from recognition/orbit data. This zero characterization keeps that substrate free of classical rational display: zero is detected entirely by signed-orbit balance and integer cross-multiplication. That matches the foundation program of deriving structure from logical constructors before any continuum or Hilbert display is introduced.
No downstream uses are recorded yet in the mirror graph, so the declaration currently closes a local definitional gap inside IntegerRational rather than feeding a named parent theorem. It is scaffolding for later orbit-arithmetic lemmas that must decide vanishing of logic-rationals without leaving the {propext, Quot.sound} fragment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.