mul_recipNonzero_crossEq_one
plain-language theorem explainer
For any nonzero ratio orbit a, the product of a with its nonzero reciprocal is cross-equivalent to the unit ratio. Order and field-structure developments on the internal PRC rationals cite this as the multiplicative inverse law. The proof reduces cross-equality to integer balance via toInt, then cancels using the numerator–reciprocal balance lemma and the reciprocal-denominator identity.
Claim. Let $a$ be a ratio orbit whose numerator is not balanced with the zero signed orbit. Then the product of $a$ with its nonzero reciprocal is cross-equivalent to the unit ratio orbit: $a \cdot a^{-1} \sim 1$.
background
In the Primitive Recognition Calculus, integers are signed orbits: pairs of distinction-nat positions with balance $a.pos + b.neg = b.pos + a.neg$ as the internal equality (K4.9). Absolute value is the orbit length $|z| = |pos - neg|$. Ratio orbits package a signed numerator with a positive denominator orbit; two ratios are identified by cross-equality, the balance of the two cross products of numerators and denominators.
Nonzero ratios (numerator not balanced with zero) admit a reciprocal whose denominator is exactly the absolute value of the original numerator. Multiplication of ratio orbits multiplies numerators and denominators in the signed-orbit and distinction-nat senses. The recovery theorem toNat_mul ensures distinction-nat multiplication matches ordinary Nat multiplication under the display map.
The local module builds the ordered field surface on these internal integers and rationals, feeding the integer-order certificate.
proof idea
Start from the sibling lemma that the product of $a$'s numerator with the reciprocal's numerator is balanced against the orbit of $den(a) \cdot |num(a)|$. Convert that balance to a toInt equality. Unfold cross-equality, multiplication, and the unit ratio, then rewrite both sides through balanced_iff_toInt_eq, mul_toInt, ofOrbit_toInt, and toNat_mul. After scaling both sides by the appropriate denominators and inserting recipNonzero_den_eq_abs (denominator of the reciprocal equals $|num(a)|$), the two toInt expressions match and simp closes.
why it matters
This is the internal multiplicative inverse law for nonzero PRC ratio orbits: $a \cdot a^{-1} \sim 1$. It is the direct input to mul_recip_crossEq_one_of_not_balanced_zero, which lifts the statement from the nonzero-reciprocal constructor to the general reciprocal on nonzero ratios. Both feed the closed integer-order certificate (integer_order_certificate), whose doc-comment states that the internal signed-orbit order surface is closed.
In the Recognition foundation stack this sits under ArithmeticFromLogic and LedgerForcing: integers and rationals are forced from distinction orbits before the T0–T8 chain reaches J-uniqueness, $\varphi$, the eight-tick octave, and $D=3$. Without inverse cancellation, the ordered-field surface on the phi-ladder mass formula and constant normalizations would not be internally certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.