recip_den_eq_abs_of_not_balanced_zero
plain-language theorem explainer
For a rational orbit whose numerator is not balanced with zero, the denominator of its reciprocal equals the absolute value of that numerator. Order and arithmetic lemmas on the internal signed-orbit rationals cite this identity when simplifying recip displays. The proof rewrites recip to the nonzero branch and applies the definitional equality for that branch's denominator.
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 (i.e. $a$ is nonzero as a rational), then the denominator of the reciprocal of $a$ equals the absolute value of the numerator of $a$.
background
In the Primitive Recognition Calculus, integers are signed orbits: pairs of distinction-nat positions with an internal balance relation. Two signed orbits $a,b$ are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; this is the PRC integer equality, defined only on $\delta$-orbit positions. Absolute value of a signed orbit is the distinction-nat $\lvert\mathrm{pos}-\mathrm{neg}\rvert$.
A ratio orbit packages a signed-orbit numerator with a nonzero distinction-nat denominator. Reciprocal is defined by cases: on the nonzero branch (numerator not balanced with zero) it swaps roles via a dedicated nonzero constructor; otherwise it falls back to a default. The local module builds the ordered field surface on these displays so that later certificates can treat integer and rational order as closed internal structure rather than imported $\mathbb{Z}$/$\mathbb{Q}$.
Upstream, recip_eq_recipNonzero_of_not_balanced_zero identifies the total reciprocal with the nonzero branch under the nonzero hypothesis, and recipNonzero_den_eq_abs states that the nonzero branch's denominator is definitionally the numerator's absolute value.
proof idea
Two-step term proof. First rewrite the total reciprocal along the nonzero-branch identification: under $\neg\mathrm{balanced}(a.\mathrm{num},0)$, $\mathrm{recip},a=\mathrm{recipNonzero},a,h$. Then apply the definitional lemma that $(\mathrm{recipNonzero},a,h).\mathrm{den}=a.\mathrm{num}.\mathrm{abs}$, which is rfl on the structure field. No further arithmetic is needed.
why it matters
Feeds integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (truncated subtraction, $\le$ display, abs-diff, and nonneg flag lemmas all line up). Without a clean identity for the reciprocal's denominator on nonzero rationals, order and comparison proofs on ratio orbits would have to case-split on the recip definition at every use site.
In the broader Recognition stack this sits in Foundation under Primitive Recognition Calculus: the integer/rational layer that must be self-contained before ledger forcing and the T0–T8 chain can treat discrete order as derived rather than axiomatic. It is bookkeeping, not a forcing step, but it closes a display equality the certificate package consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.