recip_eq_recipNonzero_of_not_balanced_zero
plain-language theorem explainer
When a ratio orbit has nonzero numerator (not balanced against zero), its total reciprocal coincides with the nonzero reciprocal constructor. Order and field-law lemmas for PRC rationals cite this to rewrite away the zero branch. The proof is a two-line unfold-and-simp on the definitional if-then-else.
Claim. Let $a$ be a ratio orbit (signed-orbit numerator over a nonzero distinction-nat denominator). If the numerator of $a$ is not balanced with the zero signed orbit, then the total reciprocal of $a$ equals the nonzero reciprocal of $a$ under that hypothesis.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of distinction-nats (pos, neg) with intended meaning pos - neg. Two signed orbits are balanced when a.pos + b.neg = b.pos + a.neg; balancing against zero is the internal nonzero test.
A ratio orbit packages a signed-orbit numerator with a nonzero distinction-nat denominator. The total reciprocal mirrors ordinary rationals: it returns zero when the numerator balances zero, and otherwise calls the nonzero reciprocal, which swaps absolute value into the denominator and rebuilds the numerator sign from nonnegFlag.
This lemma lives in the IntegerOrder module, which closes the internal order surface on those displays and feeds the integer-order certificate.
proof idea
One-line definitional reduction. Unfold the total reciprocal: it is if h : balanced(num, zero) then zero else recipNonzero a h. The hypothesis is exactly the negation of the if-guard, so simp [h] selects the else branch and yields definitional equality with recipNonzero a h.
why it matters
Bridge between the total and partial reciprocal APIs. Downstream lemmas that prove a * recip(a) ~ 1, recip(a) * a ~ 1, denominator equals absolute numerator, and numerator absolute value equals the old denominator all rewrite through this equality before invoking the nonzero-case facts.
Those facts accumulate into integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (truncated subtraction, leq, absolute difference, and nonnegativity displays). In the Recognition foundation this is bookkeeping for the rational layer built from δ-orbits, not a forcing-chain step (T5–T8), but it is required scaffolding before cost uniqueness and ledger arithmetic can treat inverses cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.