recip_num_eq_of_nonnegFlag_of_not_balanced_zero
plain-language theorem explainer
When a ratio orbit has a nonzero nonnegative numerator, the numerator of its reciprocal equals the nonnegative signed orbit built from the original denominator. Reciprocal-arithmetic and integer-order certificate proofs cite this identity. The argument rewrites reciprocal onto the nonzero branch, then applies the corresponding numerator lemma.
Claim. Let $a$ be a ratio orbit. If the numerator of $a$ is not balanced with zero and carries nonnegative flag true, then the numerator of the reciprocal of $a$ equals the nonnegative signed orbit formed from the denominator of $a$.
background
In the Primitive Recognition Calculus, integers are represented as signed orbits: pairs of $\delta$-orbit positions (positive and negative sides). Two signed orbits are balanced when $a.pos + b.neg = b.pos + a.neg$; balance with zero is the internal zero test. The nonnegative flag is the structural comparison leq of the negative side against the positive side. ofOrbit builds a nonnegative signed orbit $\langle n, 0\rangle$ from a bare $\delta$-orbit length.
Ratio orbits package a numerator and denominator signed orbit as an internal rational. Reciprocal is defined by cases: on the nonzero branch it swaps sides (with sign bookkeeping); the zero branch is excluded by the unbalanced-with-zero hypothesis. The sibling lemma recip_eq_recipNonzero_of_not_balanced_zero identifies the total reciprocal with that nonzero branch under the same hypothesis. A parallel lemma already computes the numerator of the nonzero reciprocal when the original numerator is flagged nonnegative.
proof idea
Term-mode, two steps. First rewrite the total reciprocal to the nonzero reciprocal via recip_eq_recipNonzero_of_not_balanced_zero, using the unbalanced-with-zero hypothesis. Then apply recipNonzero_num_eq_of_nonnegFlag with the same nonzero witness and the nonnegative-flag hypothesis; that lemma simplifies the nonzero reciprocal definition under the flag and yields equality of the numerator with ofOrbit of the original denominator.
why it matters
This is a small but necessary reciprocal-numerator identity on the internal rational surface. It feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed; the certificate packages display lemmas for truncated subtraction, order, absolute difference, and nonnegative flags. Without a clean numerator formula for reciprocals of nonnegative nonzero ratio orbits, order and comparison facts on rationals built from signed orbits cannot be discharged inside the PRC stack. The result sits in the Foundation layer that underwrites later forcing-chain arithmetic (T5 J-cost uniqueness and the phi ladder rely on a coherent ordered field of internal integers and rationals).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.