crossEq_zero_iff_num_balanced_zero
plain-language theorem explainer
Cross-equality of a ratio orbit to zero is equivalent to its numerator balancing the zero signed orbit. Order and reciprocal lemmas in the primitive recognition calculus cite this bridge. The proof unfolds cross-equality and zero, rewrites through the toInt characterization and scale-by-nat identities, then simplifies.
Claim. For every ratio orbit $a$ (signed-orbit numerator over a nonzero distinction-nat denominator), $a$ is cross-equal to the zero ratio orbit if and only if the numerator of $a$ is balanced with the zero signed orbit.
background
In the primitive recognition calculus, integers are carried by signed orbits: pairs of distinction-nat lengths with an internal balance relation $a.pos + b.neg = b.pos + a.neg$. That relation is equivalent to equality of the conservative integer displays (toInt).
Rationals are ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator. Two ratio orbits are cross-equal when the scaled products of numerator and opposite denominator balance as signed orbits. This is the internal PRC stand-in for rational equality, defined only on $\delta$-orbit positions (K4.10).
The zero ratio orbit has zero numerator. The present lemma specializes cross-equality against that zero to a pure numerator condition, using the bridge balanced_iff_toInt_eq and the scaling law (z.scaleByNat d).toInt = z.toInt \cdot d.toNat.
proof idea
Unfold the definitions of cross-equality and of the zero ratio orbit. Rewrite both sides with balanced_iff_toInt_eq, apply scaleByNat_toInt on each scaled factor, and insert zero_toInt. A final simp closes the resulting integer arithmetic identity. The argument is a short rewrite chain; no case split is required.
why it matters
This is the zero-test for internal rationals: $a \sim_{\times} 0$ reduces to numerator balance with zero. Downstream it feeds the symmetric form zero_crossEq_iff_num_balanced_zero, the reciprocal zero tests recip_crossEq_zero_iff_num_balanced_zero and recip_crossEq_zero_iff_crossEq_zero, and the nonzero hypotheses in the reciprocal product laws that recover cross-equality to one.
Those facts sit on the path to integer_order_certificate, which closes the internal signed-orbit order surface (nonnegativity flags, truncated subtraction, absolute difference displays). Within Recognition Science this is foundation scaffolding for the rational layer that later supports the forcing chain and the J-cost calculus, not a physics claim itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.