recipNonzero_den_eq_abs
plain-language theorem explainer
For any nonzero ratio orbit, the denominator of its reciprocal equals the absolute value of its numerator. Algebraists working the PRC integer/rational layer cite this when simplifying reciprocal products back to the unit. The proof is pure definitional equality (rfl): recipNonzero is constructed with that denominator by design.
Claim. Let $a$ be a ratio orbit (signed-orbit numerator over a nonzero orbit denominator). If the numerator is not balanced with zero, then the denominator of the reciprocal of $a$ equals the absolute value of that numerator: $\mathrm{den}(a^{-1}) = |a_{\mathrm{num}}|$.
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair of distinction-nat positions $(p,n)$ read as $p-n$. Two signed orbits are balanced when $a.p+b.n=b.p+a.n$; balance with zero is the internal nonzero test. Absolute value of a signed orbit is the orbit-position absolute difference of its positive and negative legs.
A ratio orbit packages a signed-orbit numerator over a nonzero distinction-nat denominator. Its nonzero reciprocal is defined so that the new numerator carries the old denominator with sign chosen by the structural nonneg flag, and the new denominator is exactly the absolute value of the old numerator. The present statement records that last clause as an equality usable in later rewrites.
The local module builds the order and arithmetic surface on these native integer and rational displays, without external $\mathbb{Z}$ or $\mathbb{Q}$ until transport theorems.
proof idea
One-line definitional proof: rfl. Unfolding the reciprocal constructor shows its denominator field is set to a.num.abs, so the claimed equality holds by construction. No lemmas are applied.
why it matters
This is a small but load-bearing identity in the PRC rational arithmetic stack. Downstream it discharges the denominator step in the two-sided reciprocal product laws (mul_recipNonzero_crossEq_one and recipNonzero_mul_crossEq_one), which assert that $a\cdot a^{-1}$ and $a^{-1}\cdot a$ are cross-equal to the unit ratio. It is also the rewrite target for the unrestricted reciprocal form recip_den_eq_abs_of_not_balanced_zero.
Those identities feed the closed integer-order certificate (integer_order_certificate), which packages display lemmas for truncated subtraction, order flags, absolute difference, and signed nonnegativity. In the broader Recognition forcing picture this sits under the foundation ledger/PRC layer that precedes the T5–T8 uniqueness chain; it does not itself force $J$, $\varphi$, or dimension, but keeps the native rational display coherent enough for later cost and mass ladder work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.