recipNonzero_num_nonnegFlag_eq

In the primitive recognition calculus, integers are carried as signed orbits: a distinction-nat magnitude plus a Boolean nonnegativity flag (with a derived negative flag). A ratio orbit is a pair of signed orbits (numerator and denominator) representing a rational in lowest form under the ledger balance relation. Balance with zero means the signed orbit is the zero element, so the hypothesis here is that the numerator is nonzero.

The nonzero reciprocal swaps numerator and denominator with sign bookkeeping: if the original numerator is nonnegative, the reciprocal numerator is the positive orbit of the old denominator; if negative, it is the negation of that orbit. Upstream lemmas record exactly those two equalities (recipNonzero_num_eq_of_nonnegFlag, recipNonzero_num_eq_of_negativeFlag), together with the facts that ofOrbit is always nonnegative and that negation of a nonzero positive orbit is negative.

This module builds the internal order surface on signed orbits and ratio orbits (reflexivity, totality, trichotomy, flag characterizations of $\le$ and $<$). The present statement is the flag-level bridge that lets order comparisons with zero pass through inversion.

Case-split on whether the numerator nonnegativity flag is true.

Positive branch: rewrite the reciprocal numerator via recipNonzero_num_eq_of_nonnegFlag to ofOrbit of the denominator, then apply nonnegFlag_ofOrbit to recover true, matching the hypothesis flag.

Negative branch: first force the flag to false by exhaustion, then convert to negativeFlag = true by negativeFlag_eq_true_iff_nonnegFlag_eq_false. Rewrite the reciprocal numerator via recipNonzero_num_eq_of_negativeFlag to the negation of ofOrbit of the denominator, and apply nonnegFlag_negate_ofOrbit_of_ne_zero (using denominator nonzero) to obtain false, again matching the original flag.

This is the flag-preservation step that closes reciprocal order transfer for nonzero ratio orbits. Downstream, recipNonzero_num_zero_le_iff and recipNonzero_num_zero_lt_iff reduce zero-comparisons of the reciprocal numerator to the same comparisons on the original numerator by rewriting through this equality and the flag characterizations of $\le$ and $<$. The unrestricted reciprocal wrapper recip_num_nonnegFlag_eq_of_not_balanced_zero is a one-line reduction to the same fact.

Those lemmas feed the integer-order certificate (integer_order_certificate), whose doc-comment states that "the internal signed-orbit order surface is closed." In the Recognition foundation stack this sits under the ledger-forcing and primitive calculus layer that supports the forcing chain (T0–T8), not as a physics identity itself: it is bookkeeping that keeps sign and order coherent when ratios invert, which later mass-ladder and coupling constructions rely on for well-defined positive scales.