forcingFn_mul
plain-language theorem explainer
The universal forcing map between any two strict logic realizations preserves multiplication on the forced naturals. Anyone building the forced-semiring certificate cites this to get a monoid homomorphism on LogicNat. The proof is a one-line application of the general fact that zero-fixing, successor-commuting maps preserve multiplication.
Claim. For any two strict logic realizations $R$ and $S$, and any $a,b$ in the logic naturals, the universal forcing map $F_{R,S}$ satisfies $F_{R,S}(a\cdot b)=F_{R,S}(a)\cdot F_{R,S}(b)$.
background
LogicNat is the inductive type forced by the Law of Logic: identity is the zero-cost multiplicative identity in the orbit, and step is one more generator iteration. Its two-constructor shape mirrors the orbit ${1,\gamma,\gamma^2,\ldots}$ as the smallest positive-real subset closed under multiplication by $\gamma$ and containing 1.
A StrictLogicRealization packages a concrete carrier realizing that structure. The forcing map between two such realizations is the unique structure map supplied by universal forcing; here it is presented as a self-map of LogicNat.
Upstream, any map that fixes zero and commutes with successor already preserves addition. Multiplication is defined by recursion on the second argument via addition, so the same hypotheses force multiplicative preservation.
proof idea
One-line term wrapper. Apply the general lemma that a map fixing zero and commuting with successor preserves multiplication, instantiating the map by the forcing map, the zero hypothesis by the forcing-map zero lemma, and the successor hypothesis by the forcing-map successor lemma. Those two lemmas unpack the universal-forcing axioms (zero to zero, step to step).
why it matters
Feeds the forced-semiring certificate, which records that the forcing map is bijective and preserves zero, one, addition, and multiplication. That certificate is the local claim that arithmetic on the forced carrier is unique up to unique isomorphism: the semiring structure is forced, not chosen.
In the Recognition Science stack this sits in the foundation layer beneath the J-cost uniqueness step (T5), the self-similar fixed point $\phi$ (T6), and the later dimensional forcing. Without a forced semiring there is no canonical arithmetic on which the $\phi$-ladder and mass formula can act.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.