recipNonzero_num_cmp_zero
plain-language theorem explainer
Reciprocating a nonzero ratio orbit preserves the three-way comparison of its numerator against zero. Order and ratio-arithmetic developments cite this when moving sign facts across inversion. The proof cases on cmp of the numerator versus zero, routes the strict cases through reciprocal-numerator order equivalences, and discharges equality by the nonzero hypothesis.
Claim. Let $a$ be a ratio orbit whose numerator is not balanced with zero. Then $\mathrm{cmp}\bigl((\mathrm{recip}_{\neq 0}(a)).\mathrm{num},\,0\bigr)=\mathrm{cmp}(a.\mathrm{num},\,0)$. Equivalently, the nonzero reciprocal preserves the sign of the numerator relative to zero under the internal signed-orbit comparison.
background
This lives in the primitive recognition calculus integer-order layer, where integers are carried as signed orbits and comparison is internal rather than display-level. SignedOrbit.cmp is the three-way selector: it returns equality when the two orbits are balanced, otherwise inspects the nonnegativity flag of their difference. The companion characterizations cmp_eq_lt_iff, cmp_eq_eq_iff, and cmp_eq_gt_iff (with the directed constructors cmp_eq_lt_of_lt and cmp_eq_gt_of_gt) convert freely between Ordering values and the underlying strict order or balance relation.
A RatioOrbit packages a signed numerator (and denominator) as a ratio. The partial operation recipNonzero inverts a ratio under the hypothesis that the numerator is not balanced with zero, i.e. the ratio is nonzero. Balance here is the ledger-style equality test on signed orbits, not a floating display check. The local goal is to show that this inversion does not flip the numerator's comparison against zero.
proof idea
Term-mode proof by cases on hcmp : cmp a.num zero.
lt: convert viacmp_eq_lt_ifftoa.num < 0, push across the reciprocal withrecipNonzero_num_lt_zero_iff, then rebuildcmp = ltbycmp_eq_lt_of_lt.eq: convert viacmp_eq_eq_iffto balance ofa.numwith zero, contradicting the nonzero hypothesish; finish withFalse.elim.gt: convert viacmp_eq_gt_iffto0 < a.num, push withrecipNonzero_num_zero_lt_iff, rebuildcmp = gtbycmp_eq_gt_of_gt.
No arithmetic expansion of reciprocal is needed; the work is pure order-transport through the existing iff lemmas.
why it matters
Closes a sign-stability fact for ratio inversion inside the signed-orbit order surface. Downstream, recip_num_cmp_zero_of_not_balanced_zero reduces the total reciprocal's numerator comparison to this statement by rewriting recip to recipNonzero under the same nonzero hypothesis. That fact, together with sibling order lemmas, feeds integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed."
In the Recognition foundation stack this is bookkeeping for the arithmetic layer beneath the forcing chain: integers and ratios must carry a coherent internal order before J-cost, the Recognition Composition Law, and the T5–T8 uniqueness steps can sit on top. It does not itself force phi or dimension; it keeps numerator sign coherent under inversion so later certificates can treat ratio order as closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.