recipNonzero_num_not_balanced_zero
plain-language theorem explainer
If a rational orbit has nonzero numerator, the numerator of its reciprocal is also nonzero. Order and reciprocal lemmas in the primitive recognition calculus cite this to keep zero out of the reciprocal numerator. The proof rewrites absolute value of the reciprocal numerator to the original denominator and invokes the denominator nonzero certificate.
Claim. Let $a$ be a rational orbit (signed-orbit numerator over a nonzero orbit denominator). If the numerator of $a$ is not balanced with the zero signed orbit, then the numerator of the reciprocal of $a$ (formed under that nonzero hypothesis) is likewise not balanced with zero.
background
In the primitive recognition calculus, integers are carried as 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}$; balance with the zero orbit is the internal notion of being zero. Absolute value of a signed orbit is the distinction-nat absolute difference of its positive and negative positions.
A rational orbit is a signed-orbit numerator over a nonzero distinction-nat denominator (the structure carries den ≠ 0 by construction). Reciprocal on the nonzero locus swaps roles so that the absolute value of the reciprocal numerator equals the original denominator.
The local module builds the internal order surface on these displays: comparison, sign flags, and reciprocal compatibility, without appealing to an external integer verifier.
proof idea
Contradiction. Assume the reciprocal numerator is balanced with zero. The upstream equivalence abs_eq_zero_iff_balanced_zero turns that into: absolute value of the reciprocal numerator equals distinction-nat zero. Rewrite via recipNonzero_num_abs_eq_den, which identifies that absolute value with the original denominator. The resulting equality den = 0 contradicts the rational orbit's built-in denominator-nonzero certificate.
why it matters
Reciprocal must preserve nonzeroness of the numerator so that order comparisons and sign flags remain well-defined after inversion. Downstream, recip_num_not_balanced_zero_of_not_balanced_zero lifts the statement from the nonzero reciprocal constructor to the total reciprocal, and recipNonzero_num_zero_lt_iff uses it to equate strict positivity of a numerator with strict positivity of its reciprocal numerator. The same fact feeds recip_num_balanced_zero_iff and ultimately the closed integer-order certificate that packages display lemmas for the signed-orbit order surface.
In the Recognition foundation this is bookkeeping on the δ-orbit integer layer beneath the forcing chain: clean reciprocal nonzeroness is required before cost functionals and ladder arithmetic can treat rational displays as a field-like structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.