recipNonzero_num_zero_le_iff
plain-language theorem explainer
For a ratio orbit with nonzero numerator, the numerator of its reciprocal is nonnegative in the signed-orbit order iff the original numerator is. Cited by anyone transporting sign under inversion on the PRC integer/rational surface. Proof is a three-rewrite chain: both sides reduce to nonnegativity flags, then flag equality under reciprocal.
Claim. Let $a$ be a ratio orbit whose numerator is not balanced with the zero signed orbit. Then $0\le N(\mathrm{recip}^*(a))$ if and only if $0\le N(a)$, where $N$ extracts the numerator signed orbit, $\mathrm{recip}^*$ is reciprocal under the nonzero-numerator hypothesis, $\le$ is the internal order ($b-a$ nonnegative), and balance is the PRC integer equivalence $x_{\mathrm{pos}}+y_{\mathrm{neg}}=y_{\mathrm{pos}}+x_{\mathrm{neg}}$.
background
In Primitive Recognition Calculus, integers are signed orbits: pairs of $\delta$-orbit positions equipped with a nonnegativity flag. Two signed orbits are balanced (the internal integer equality) when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. The order $a\le b$ means the difference $b-a$ is nonnegative.
Ratio orbits package a rational as numerator and denominator signed orbits. Reciprocal under a nonzero-numerator hypothesis is a specialized constructor that keeps the nonzero witness in the type. The module builds the full order surface on these representations before any external $\mathbb{Z}$ or $\mathbb{Q}$ embedding.
Upstream, zero is at most a signed orbit exactly when its nonnegativity flag is true. A companion lemma states that reciprocal preserves that flag on the numerator whenever the numerator is not balanced with zero.
proof idea
Pure rewrite proof, three steps. Rewrite both sides of the biconditional with the characterization that $0\le z$ iff the nonnegativity flag of $z$ is true. The goal collapses to equality of those flags on the reciprocal numerator and the original numerator, which is exactly the upstream flag-preservation lemma for reciprocal under the nonzero hypothesis. No case split remains at this layer.
why it matters
Supplies the sign-transport step used by the sibling that upgrades the statement from the specialized reciprocal constructor to ordinary reciprocal (via their equality when the numerator is nonzero). Both sit under the integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed.
At framework scale this is foundation arithmetic, not yet T5–T8 physics: it ensures the order and the rational structure agree on inversion before mass ladders, $J$-cost, or the eight-tick octave are built on top. Without sign coherence under reciprocal, later comparison lemmas on ratio orbits would not be trustworthy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.