toNat_mul
plain-language theorem explainer
Orbit multiplication on distinction naturals is faithful under the verifier map: the displayed magnitude of a product equals the product of the displayed magnitudes. Anyone proving factorization chart transitions, integer multiplication recovery, or magnitude uniqueness cites this. The proof is induction on the second factor, reducing via the recursive mul clause and the already-proved addition recovery.
Claim. For distinction naturals $a$ and $b$ (orbit positions), if $(\cdot).\mathrm{toNat}$ reads off the iteration count into ordinary $\mathbb{N}$, then $(a \cdot b).\mathrm{toNat} = a.\mathrm{toNat} \cdot b.\mathrm{toNat}$.
background
Distinction naturals are the orbit-arithmetic carrier in the primitive recognition calculus: positions generated by iterating a step from zero, parallel to the LogicNat construction in ArithmeticFromLogic. The map toNat is the forward verifier: it reads the iteration count into Lean Nat (identity/zero maps to 0; successor increments).
Multiplication on this carrier is defined recursively by the Peano clause $a \cdot S(n) = a \cdot n + a$ (and $a \cdot 0 = 0$), so it is not assumed to match ordinary Nat multiplication a priori. The sibling recovery theorem for addition already states that addition of orbit positions agrees with Nat addition under toNat.
Upstream, ArithmeticFromLogic proves the same recovery for LogicNat multiplication by an identical induction. Here the statement is restated for DistinctionNat so factorization and integer layers can quote orbit arithmetic directly.
proof idea
Induct on the second factor $b$.
Zero case: rewrite with the orbit mul-zero identity and toNat_zero; both sides become zero (closed by omega).
Successor case: the recursive clause gives $a \cdot S(n) = a \cdot n + a$. Apply the addition recovery toNat_add, the successor identity toNat_succ, the inductive hypothesis, and Lean Nat.mul_succ to match $a.\mathrm{toNat} \cdot S(n.\mathrm{toNat})$.
why it matters
This is K4.7 in the orbit-arithmetic layer: the verifier display of orbit multiplication matches Lean Nat. Downstream, ChartTransition uses it as the body of factorPairProduct_toNat (product of a factor pair displays as the ordinary product) and in the concrete ambiguity $2\cdot 6 = 3\cdot 4$ under magnitude, which shows magnitude alone is not a factor oracle. CoordinateUniqueness quotes it for prime-coordinate products and factorization-product agreement.
It also feeds IntegersFromLogic: integer multiplication is defined on pairs of LogicNat via the usual $(ac+bd, ad+bc)$ formula, and toInt_mul recovers ordinary integer multiplication, relying on this Nat-level agreement. In the Recognition foundation stack this is pure arithmetic recovery, not a physics forcing step (T5–T8), but it is the bridge that lets later period-readout and factorization arguments treat orbit products as ordinary magnitudes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.