recipNonzero_num_eq_of_negativeFlag
plain-language theorem explainer
When a ratio orbit has strictly negative numerator (and is nonzero), the numerator of its reciprocal equals the pointwise negation of the denominator orbit. Order and reciprocal lemmas in the primitive recognition calculus cite this case split. The proof reduces the negative flag to a false nonnegative flag and unfolds the reciprocal definition.
Claim. Let $a$ be a ratio orbit whose numerator is not balanced with zero. If the numerator is strictly negative (negative flag true), then the numerator of the nonzero reciprocal of $a$ equals the pointwise negation of the nonnegative signed orbit built from the denominator of $a$.
background
In the primitive recognition calculus, integers are signed orbits: pairs of $\delta$-orbit positions with a structural balance relation $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. Nonnegativity is the computable flag comparing the two sides; strict negativity is its Boolean negation. Pointwise negation swaps the two sides. A nonnegative signed orbit is built from a bare orbit by pairing it with zero.
Ratio orbits package a signed numerator with a positive denominator orbit. The nonzero reciprocal is defined by cases on the numerator sign flag: the nonnegative branch places the denominator in the numerator slot; the negative branch places its negation there. This lemma records the negative branch exactly.
The local module develops the internal order on these signed orbits and the interaction of that order with reciprocal and absolute value, feeding a closed integer-order certificate.
proof idea
From the hypothesis that the negative flag is true, unfold that flag as the Boolean negation of the nonnegative flag and case on the nonnegative flag. The true branch contradicts the hypothesis by simplification; the false branch is the needed equality. With the nonnegative flag false in hand, a single simp on the reciprocal definition and that fact yields the claimed numerator equality.
why it matters
This is the negative-numerator case of the reciprocal numerator formula. Downstream it is used by the absolute-value identity for reciprocal numerators, the sign-preservation of the reciprocal numerator, the balanced-with-negated-denominator characterization of the negative flag, the product-balance identity linking numerator times reciprocal numerator to denominator times absolute numerator, and the residual reciprocal-numerator equality under a negative flag. Those lemmas assemble into the integer-order certificate that closes the internal signed-orbit order surface.
In the Recognition foundation this sits inside the pre-physics integer and rational layer of the primitive recognition calculus: signed orbits and ratio orbits before the forcing chain (T5 J-cost, T6 $\varphi$, T7 eight-tick, T8 $D=3$). It does not itself force a physical constant; it keeps reciprocal and order coherent on the discrete ledger integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.