mul_toInt
plain-language theorem explainer
Multiplication of signed orbits is compatible with the integer recovery map: the integer of a product equals the product of the integers. Anyone building divisibility, ordering, or ring structure on signed orbits cites this. The proof expands both sides via the (pos,neg) difference representation, rewrites with the Nat recovery lemmas for add and mul, then finishes by ring.
Claim. For signed orbits $a,b$ (each a pair of distinction-naturals read as $\mathrm{pos}-\mathrm{neg}$), if $\mathrm{mul}$ is the signed-orbit product and $\mathrm{toInt}$ is the recovery map to $\mathbb{Z}$, then $\mathrm{toInt}(\mathrm{mul}(a,b)) = \mathrm{toInt}(a)\cdot\mathrm{toInt}(b)$.
background
Signed orbits are the K4.6 difference representation of integers in the Primitive Recognition Calculus: a pair (pos, neg) of distinction-naturals, intended as $\mathrm{pos}-\mathrm{neg}$. The recovery map toInt sends such a pair to an ordinary integer by reading off iteration counts and subtracting.
Upstream, distinction-naturals (and the underlying logic-naturals) already recover ordinary $\mathbb{N}$ arithmetic: toNat_add and toNat_mul state that the logic-level sum and product agree with Nat addition and multiplication under toNat. Integers-from-logic supplies the parallel recovery story for signed pairs, including negation as swap of components.
This module sits in the foundation layer that builds integer and rational structure from recognition orbits before any continuum or cost calculus is imposed. The local goal is a faithful embedding of signed-orbit arithmetic into $\mathbb{Z}$.
proof idea
Unfold both sides in the difference representation. The left-hand side is the integer of the product orbit, written as
$((a_+ b_+ + a_- b_-) - (a_+ b_- + a_- b_+))$ after toNat; the right-hand side is $(a_+-a_-)(b_+-b_-)$.
Rewrite the four products and two sums with DistinctionNat.toNat_mul and DistinctionNat.toNat_add (the recovery theorems that logic-level mul/add match Nat). push_cast lifts the resulting natural equalities into $\mathbb{Z}$, and ring closes the polynomial identity.
why it matters
This is the multiplicative half of the integer-recovery homomorphism for signed orbits. Downstream, the entire integer-divisibility package depends on it: dvdZ_refl, dvdZ_trans, dvdZ_add, one_dvdZ, and dvdZ_zero all reduce balanced-product witnesses through mul_toInt (often with one_toInt or zero_toInt) before an omega finish. Ratio-orbit order lemmas such as leQ_neg_neg_iff and the antisymmetry/transitivity suite likewise rewrite through it when comparing signed cross-multiples.
In the Recognition foundation chain this is pure arithmetic scaffolding: it does not yet touch J-cost, the forcing chain T5–T8, or the phi-ladder, but it is required before any integer or rational statement about orbits can be stated in $\mathbb{Z}$. Without it, divisibility and ordered-field structure on recognition integers stay unlinked to classical arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.