recipNonzero_num_abs_eq_den
plain-language theorem explainer
For a nonzero ratio orbit a, the absolute value of the numerator of its reciprocal equals a's denominator. Order and rational-arithmetic developments cite this when relating reciprocal numerators to original denominators under the signed-orbit encoding. The proof case-splits on the numerator sign flag and rewrites via the two recip-numerator lemmas plus absolute-value identities for ofOrbit and its negate.
Claim. Let $a$ be a ratio orbit whose numerator is not balanced with zero. Then $\lvert \mathrm{num}(a^{-1}) \rvert$ equals the denominator of $a$, where $a^{-1}$ is the reciprocal formed under the nonzero-numerator hypothesis.
background
In the primitive recognition calculus, integers are encoded as signed orbits: a distinction-nat magnitude together with nonnegativity and negativity flags. Absolute value on a signed orbit recovers the underlying distinction-nat; ofOrbit embeds a distinction-nat as a nonnegative signed orbit, and negate flips the sign. Balance against zero is the internal zero test.
Ratio orbits package a signed numerator with a positive denominator. Reciprocal for a nonzero numerator swaps roles: the new numerator is built from the old denominator, with sign matching the original numerator. Two companion lemmas pin that construction: if the numerator is nonnegative, the reciprocal numerator is exactly ofOrbit of the denominator; if negative, it is the negate of that embedding.
The local module builds the ordered structure on these encodings (reflexivity, totality, trichotomy, sign-flag exclusivity) toward a closed integer-order certificate.
proof idea
Case on whether a.num.nonnegFlag is true.
Nonnegative branch: rewrite the reciprocal numerator by recipNonzero_num_eq_of_nonnegFlag, then apply abs_ofOrbit so the absolute value collapses to a.den.
Negative branch: first obtain negativeFlag = true from the flag exclusivity lemma negativeFlag_eq_true_iff_nonnegFlag_eq_false (the true case of the flag is discharged by the case hypothesis). Rewrite the reciprocal numerator by recipNonzero_num_eq_of_negativeFlag, then apply abs_negate_ofOrbit to again recover a.den.
why it matters
This identity is the absolute-value half of reciprocal correctness for nonzero ratio orbits. Downstream, recip_num_abs_eq_den_of_not_balanced_zero lifts it to the total reciprocal operation by reducing to the nonzero case, and recipNonzero_num_not_balanced_zero uses the same absolute-value fact to show the reciprocal numerator stays nonzero.
Both feed the broader integer-order surface closed by integer_order_certificate ("The internal signed-orbit order surface is closed"). In the Recognition foundation stack this sits under the primitive calculus that supports ledger forcing and the later forcing chain (T0–T8), where clean rational arithmetic on orbits is prerequisite infrastructure rather than a physics claim itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.