mul_strictpos_cf
plain-language theorem explainer
If two signed orbits are strictly positive (negative part strictly smaller than positive part under the toNat count), their product is strictly positive. Cited when closing positivity of rational orbit multiplication under the choice-free order. Proof expands the product components via toNat recovery, substitutes the strict inequalities as additive witnesses, then finishes by ring normalization and omega.
Claim. Let $a,b$ be signed orbits. If $a_{\mathrm{neg}} < a_{\mathrm{pos}}$ and $b_{\mathrm{neg}} < b_{\mathrm{pos}}$ as natural numbers (via the iteration-count map), then $(ab)_{\mathrm{neg}} < (ab)_{\mathrm{pos}}$.
background
In the primitive recognition calculus, integers and rationals are rebuilt from distinction orbits rather than assumed as primitives. A signed orbit packages a positive and a negative distinction count; the map toNat reads each count as an ordinary natural number (the iteration depth of the logic-natural). Strict positivity of a signed orbit is the inequality of those counts: negative part strictly less than positive part.
Multiplication of signed orbits is the bilinear rule familiar from integer pairs: the positive part of $ab$ is $a_{+}b_{+} + a_{-}b_{-}$ and the negative part is $a_{+}b_{-} + a_{-}b_{+}$. The recovery theorems toNat_add and toNat_mul guarantee that these orbit operations agree with ordinary Nat arithmetic after reading off counts, so positivity questions reduce to elementary Nat inequalities.
The local module sits in the Grow layer that equips ratio orbits with a choice-free order and multiplicative structure, feeding later comparison and positivity lemmas for rational orbits.
proof idea
Unfold the product: the positive count of $ab$ equals $a_{+}b_{+} + a_{-}b_{-}$ and the negative count equals $a_{+}b_{-} + a_{-}b_{+}$, each justified by rewriting with toNat_add and toNat_mul. Rewrite the goal with those identities. From the two strict inequalities, obtain additive witnesses $s,t$ via Nat.exists_eq_add_of_lt, substitute, normalize with ring_nf, and discharge the resulting Nat inequality by omega.
why it matters
This is the signed-orbit engine behind positivity of rational multiplication. Downstream, ltQ_mul_pos reduces zero-less-than product of ratio orbits to zero-less-than on numerators and invokes this theorem directly: after rewriting through zero_ltQ_iff_num and the definition of ratio multiplication, the claim is exactly mul_strictpos_cf on the numerators.
In the Recognition foundation stack, choice-free ordered arithmetic underpins the later forcing chain (T0–T8) and the cost calculus that forces $J$ and $\varphi$. Without closed positivity of products, the ordered field structure on ratio orbits would remain scaffolding. The result is fully proved (no sorry), so it hardens that layer rather than leaving an interface hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.