recipNonzero_num_eq_of_nonnegFlag
plain-language theorem explainer
When a nonzero ratio orbit has nonnegative numerator, the reciprocal's numerator is exactly the nonnegative signed orbit built from the original denominator. Integer-order and reciprocal-identity lemmas cite this case split. The proof is a one-line simp that unfolds the reciprocal constructor against the nonnegative flag.
Claim. Let $a$ be a ratio orbit whose numerator is not balanced with zero. If that numerator is flagged nonnegative, then the numerator of the reciprocal of $a$ equals the nonnegative signed orbit constructed from the denominator of $a$.
background
In the primitive recognition calculus, a ratio orbit is an integer numerator (a signed orbit) over a nonzero orbit denominator. Signed orbits carry two $\delta$-orbit lengths; they are balanced when $a.pos + b.neg = b.pos + a.neg$, the internal PRC integer relation. The computable nonnegative flag is structural comparison of those sides via $\mathrm{leq}$ on distinction naturals.
The reciprocal of a nonzero ratio orbit selects its numerator sign from that flag: if the flag is true, the new numerator is the nonnegative embedding of the old denominator; otherwise it is the negation of that embedding. The nonnegative embedding of an orbit position is the signed orbit with that position on the positive side and zero on the negative side.
This module builds the internal signed-orbit order surface used later by the integer-order certificate. The present lemma is the nonnegative branch of the reciprocal-numerator identity.
proof idea
One-line wrapper: simp unfolds the reciprocal definition and rewrites with the hypothesis that the nonnegative flag is true, so the if branch yields exactly the nonnegative embedding of the denominator.
why it matters
Closes the nonnegative case of the reciprocal numerator, which several sibling identities depend on: absolute-value of the reciprocal numerator equals the old denominator; balance of reciprocal numerator against the embedded denominator is equivalent to the nonnegative flag; sign-flag transport under reciprocal; and the product identity linking numerator times reciprocal-numerator to denominator times absolute value.
Those lemmas feed the integer-order certificate, which asserts that the internal signed-orbit order surface is closed (truncated subtraction, $\mathrm{leq}$, absolute difference, and nonnegative displays all match). In the Recognition foundation this is bookkeeping on the PRC integer/rational layer beneath the forcing chain, not a T5–T8 step itself, but required scaffolding for order and inversion on the native integer display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.