recip_mul_crossEq_one_of_not_balanced_zero
plain-language theorem explainer
When a ratio orbit has nonzero numerator (not balanced against the zero signed orbit), multiplying it by its reciprocal yields a ratio orbit cross-equivalent to one. Anyone assembling multiplicative inverse laws for the PRC rational display cites this. The proof rewrites the total reciprocal onto the nonzero branch and applies the specialized inverse identity already proved for that branch.
Claim. Let $a$ be a ratio orbit. If the numerator of $a$ is not balanced with the zero signed orbit, then the product of the reciprocal of $a$ with $a$ is cross-equivalent to the unit ratio orbit: $\mathrm{crossEq}(\mathrm{recip}(a)\cdot a,\,1)$.
background
In the Primitive Recognition Calculus integer-rational layer, a ratio orbit is an integer numerator (a signed orbit) over a nonzero distinction-nat denominator. Two ratio orbits are identified by cross-equivalence: $a$ and $b$ satisfy $\mathrm{crossEq}$ when the scaled signed orbits $a.num\cdot b.den$ and $b.num\cdot a.den$ balance, i.e. their positive and negative orbit lengths match under the K4.9 relation $a.pos+b.neg=b.pos+a.neg$.
Balance against the zero signed orbit is the internal nonzero test on a numerator. The total reciprocal on ratio orbits is defined by cases; on the nonzero branch it coincides with a specialized reciprocal that carries the nonzero hypothesis in its type. The local module builds the order and arithmetic surface for these displays, feeding the integer-order certificate.
Upstream, recip_eq_recipNonzero_of_not_balanced_zero equates the total reciprocal to the nonzero reciprocal under the same hypothesis, and recipNonzero_mul_crossEq_one already proves that the nonzero reciprocal multiplies back to one under cross-equivalence.
proof idea
Term-mode, two steps. First rewrite the total reciprocal via recip_eq_recipNonzero_of_not_balanced_zero using the nonzero-numerator hypothesis, so the goal becomes the specialized product identity. Then discharge by exact on recipNonzero_mul_crossEq_one at the same $a$ and hypothesis. No new arithmetic is performed here; the lemma is a bridge from the total reciprocal API to the already-proved nonzero branch.
why it matters
Multiplicative inverses for ratio orbits are part of closing the internal rational arithmetic surface of PRC. Downstream, recip_mul_crossEq_one_of_not_crossEq_zero reduces the crossEq-to-zero form of the nonzero test to this numerator-balance form and reuses the present result. The broader parent is integer_order_certificate, whose doc states that the internal signed-orbit order surface is closed; inverse laws sit under that certificate as arithmetic support for the order and display layer.
In the Recognition forcing chain this is foundation scaffolding rather than a T5–T8 landmark: it keeps the rational display coherent so later cost and ladder constructions can treat division as an internal operation on δ-orbit data, not an external field axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.