recipNonzero_toRat
plain-language theorem explainer
For a ratio orbit with nonzero numerator, the rational display of its nonzero reciprocal equals the field inverse of its own rational display. Anyone proving reciprocal identities on orbit rationals (double reciprocal, cross-equality) cites this bridge. The proof unfolds the displays, rules out a zero numerator via the balanced hypothesis, then case-splits on the sign flag and reduces absolute values.
Claim. Let $a$ be a ratio orbit (signed-orbit numerator over a nonzero distinction-nat denominator). If the numerator is not balanced against zero, then the rational display of the nonzero reciprocal of $a$ equals $(a^{\mathrm{rat}})^{-1}$ in $\mathbb{Q}$.
background
This module builds integers and rationals from primitive recognition orbits. A signed orbit is a difference of two distinction-nats (intended meaning pos minus neg); its verifier map toInt recovers an ordinary integer. Balance against zero means that integer is zero. A ratio orbit packages a signed-orbit numerator with a nonzero distinction-nat denominator, and toRat sends it to the corresponding rational.
The nonzero reciprocal swaps roles of absolute numerator and denominator (with sign bookkeeping) and is only defined when the numerator is unbalanced against zero. Upstream, abs_toNat identifies the internal absolute value with Int.natAbs of the verifier integer, and the nonneg-flag lemmas classify the sign of toInt.
Local setting is K4 of the primitive recognition calculus: constructing a rational display closed under the operations that later feed ledger and cost algebra.
proof idea
Unfold the nonzero reciprocal and the rational display. The denominator casts to a nonzero rational by the ratio-orbit invariant. The numerator's integer is nonzero: if it were zero, balance against zero would hold by balanced_iff_toInt_eq and zero_toInt, contradicting the hypothesis; cast that to $\mathbb{Q}$.
Case on the numerator's nonneg flag. If true, the integer is nonnegative, hence positive by the nonzero fact; simplify with ofOrbit_toInt and abs_toNat, replace absolute value by the positive cast, and the identity is immediate. If false, the integer is negative; simplify with ofOrbit_toInt, negate_toInt, and abs_toNat, replace absolute value by the negated cast, then field_simp finishes the inverse identity.
why it matters
This is the nonzero half of the rational-display law for reciprocal on ratio orbits (K4.12). The total reciprocal theorem recip_toRat case-splits on balance and invokes this lemma on the nonzero branch, sending zero to zero as in $\mathbb{Q}$. Downstream, recip_recipNonzero_crossEq_self rewrites double reciprocal cross-equality through recip_toRat and this identity, confirming that nonzero reciprocal is an involution up to cross-equality of ratio orbits.
In the Recognition foundation, ratio orbits are the discrete carrier on which ledger ratios and the cost automorphism live. Faithful transport of inversion to $\mathbb{Q}$ is required before the Recognition Composition Law and J-cost identities can be read off verifier displays. The result is fully proved; it closes the nonzero case of the K4 reciprocal package rather than leaving a scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.