recipNonzero
plain-language theorem explainer
Defines the reciprocal of a nonzero rational orbit: numerator is the original denominator with sign taken from the structural nonnegative flag, and denominator is the absolute value of the original numerator. Anyone building internal field arithmetic on ratio orbits cites this constructor. The body is a direct structure assembly using abs-nonzero from the non-balance hypothesis.
Claim. Given a ratio orbit $a = (n,d)$ whose numerator $n$ is not balanced with zero, the reciprocal is the ratio orbit whose numerator is $+d$ if $n$ is structurally nonnegative and $-d$ otherwise, and whose denominator is $|n|$ (which is nonzero by the non-balance hypothesis).
background
In the Primitive Recognition Calculus, integers are carried as signed orbits: pairs of distinction-nat positions with intended meaning $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; balance with zero is the internal zero test. Absolute value is the orbit-length difference $\mathrm{absDiff}(\mathrm{pos},\mathrm{neg})$, and the computable nonnegative flag is the structural comparison $\mathrm{neg}\le\mathrm{pos}$.
A ratio orbit is an integer numerator over a nonzero orbit denominator. Reciprocals are only well-defined off the zero class, so the constructor takes an explicit non-balance hypothesis. Upstream, abs_ne_zero_of_not_balanced_zero converts that hypothesis into a nonzero denominator certificate for the reciprocal.
proof idea
Definitional structure assembly, not a tactic proof. The numerator branch is a Boolean case on the structural nonnegative flag: if true, lift the original denominator via ofOrbit; if false, take the pointwise negate of that lift. The denominator field is the absolute value of the original numerator. The den_ne_zero field is discharged by applying abs_ne_zero_of_not_balanced_zero to the supplied non-balance hypothesis.
why it matters
This is K4.12 in the integer-rational layer: the total reciprocal constructor used throughout internal order and field lemmas. Downstream, mul_recipNonzero_crossEq_one and recipNonzero_mul_crossEq_one show that multiplying a nonzero ratio by this reciprocal is cross-equivalent to one; recip_eq_recipNonzero_of_not_balanced_zero identifies the partial reciprocal with this total form off zero; and several display lemmas pin numerator and denominator fields (recipNonzero_den_eq_abs, recipNonzero_num_abs_eq_den). It feeds the step-1 IntegerOrderCertificate bundle. Within Recognition Science this is pure foundation scaffolding for ledger arithmetic, not yet a physics forcing step (T5–T8), but it is required before rational displays can support cost and ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.