map_preserves_mul
plain-language theorem explainer
Any map on the logic-forced naturals that fixes zero and commutes with successor also preserves multiplication. Cited by anyone assembling the unique forcing homomorphism between strict logic realizations. The proof inducts on the second factor after calling the companion addition-preservation lemma, using the recursive definition of multiplication via addition.
Claim. Let $h:\mathbb{N}_{\mathrm{L}}\to\mathbb{N}_{\mathrm{L}}$ satisfy $h(0)=0$ and $h(n+1)=h(n)+1$ for every $n$. Then $h(ab)=h(a)\,h(b)$ for all $a,b\in\mathbb{N}_{\mathrm{L}}$.
background
LogicNat is the inductive type of naturals forced by the Law of Logic: identity is the zero-cost element and step is one more iteration of the generator (so successor is just step). Multiplication is defined by recursion on the second argument: $n\cdot 0=0$ and $n\cdot\mathrm{succ}(m)=n\cdot m+n$ (the simp lemmas mul_zero and mul_succ).
The module builds the unique structure-preserving map between strict logic realizations. The sibling lemma already shows that any zero-fixing, successor-commuting map preserves addition; the present result lifts that to multiplication because multiplication is defined from addition.
proof idea
First obtain addition preservation by applying the sibling lemma to the same hypotheses on $h$. Fix $a$ and induct on $b$. In the zero case both sides reduce by mul_zero and the zero-fixing hypothesis. In the successor case rewrite with mul_succ, apply addition preservation and the inductive hypothesis, then use successor-commutation and mul_succ again to match the right-hand side.
why it matters
Directly feeds forcingFn_mul, which states that the canonical forcing map between two strict logic realizations preserves multiplication (one-line application of this lemma to forcingFn with its zero and successor lemmas). That is a required piece of the forced-semiring certificate and of uniqueness of the forcing homomorphism. In Recognition Science, arithmetic is forced from logic rather than axiomatized; showing that every zero/succ map is a monoid homomorphism is a step toward unique isomorphism of the forced arithmetic structure that underwrites the Universal Forcing chain (and thereby the T0–T8 landmarks).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.