recip_num_balanced_zero_iff
plain-language theorem explainer
Reciprocal preserves zero-ness of a ratio orbit's numerator: the numerator of recip(a) is balanced with signed zero exactly when a's numerator is. Order and cross-equality lemmas for RatioOrbit cite this when relating recip(a) to zero. The proof is a case split on whether the numerator is already zero, using the nonzero-reciprocal branch and its non-vanishing lemma.
Claim. For every ratio orbit $a$, the numerator of its reciprocal is balanced with signed-orbit zero if and only if the numerator of $a$ is balanced with signed-orbit zero. Here balance of signed orbits $x,y$ means $x_{\mathrm{pos}}+y_{\mathrm{neg}}=y_{\mathrm{pos}}+x_{\mathrm{neg}}$.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative $\delta$-orbit lengths with a balance relation $a.pos + b.neg = b.pos + a.neg$ (K4.9). That relation is the internal equality used throughout IntegerOrder; in particular, "balanced with zero" is the PRC stand-in for a vanishing numerator.
Ratio orbits package a signed numerator (and denominator data) so that rational comparison and reciprocal can be defined without leaving the orbit language. The reciprocal RatioOrbit.recip is defined by cases: if the numerator is already balanced with zero, the reciprocal collapses to the zero ratio orbit; otherwise it routes through a nonzero reciprocal constructor recipNonzero that is known never to produce a zero numerator (recipNonzero_num_not_balanced_zero).
The local module builds the signed-orbit order surface (reflexivity, totality, trichotomy, sign flags) that later feeds the integer-order certificate.
proof idea
Case on whether a.num is balanced with signed zero.
- Zero case: unfold
RatioOrbit.recip; simplification with the zero hypothesis,RatioOrbit.zero, and reflexivity of balance closes both directions. - Nonzero case: rewrite
recip atorecipNonzero a hviarecip_eq_recipNonzero_of_not_balanced_zero. Each implication is then anexfalso: the forward direction appliesrecipNonzero_num_not_balanced_zero(nonzero reciprocal never has zero numerator); the reverse direction is just the case hypothesis.
why it matters
Zero-preservation under reciprocal is the bridge from numerator balance to cross-equality with the zero ratio. Immediate consumers are recip_crossEq_zero_iff_num_balanced_zero and zero_crossEq_recip_iff_num_balanced_zero (each a short trans with the ordinary crossEq-zero characterization), plus the negated form recip_num_not_balanced_zero_iff.
Those facts sit on the path to integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags). In the Recognition stack this is foundation plumbing for the PRC integer/rational layer beneath ledger forcing and the later T0–T8 chain, not a physics identity itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.