mul_assoc
plain-language theorem explainer
Multiplication of distinction-orbit positions is associative: (a·b)·c = a·(b·c). Anyone building monoid or ring structure on the primitive recognition orbit cites this. The proof transports the claim through the injective Nat display and invokes ordinary Nat associativity.
Claim. For all orbit positions $a,b,c$ in the base-neutral finite distinction orbit $\mathrm{DistinctionNat}$, $(a \cdot b) \cdot c = a \cdot (b \cdot c)$.
background
DistinctionNat is the inductive type of finite orbit positions under repeated distinction (zero and successor), the K2.12 base-neutral counting object of the primitive recognition calculus. Its verifier display toNat sends zero to 0 and successor to Nat.succ, and is injective: equal Nat displays come from equal orbit positions.
Orbit arithmetic equips DistinctionNat with multiplication that agrees with Nat multiplication under that display (toNat_mul). The same pattern already appears one layer down for LogicNat in ArithmeticFromLogic and for PRCInt in IntegerRational: algebraic laws are recovered by transporting through an injective embedding into classical arithmetic.
This module sits in Foundation.PrimitiveRecognitionCalculus and develops native orbit divisibility (a divides b when some orbit factor multiplies a to b). Associativity is the monoid law needed before units, primes, and nontrivial factorizations make sense on the orbit.
proof idea
Term-mode transport proof. Apply injectivity of the orbit-to-Nat display (toNat_inj). Rewrite both sides with the recovery theorem toNat_mul four times so the goal becomes equality of Nat products. Discharge with Nat.mul_assoc on the three underlying natural numbers. No induction on the orbit itself is required.
why it matters
This is the associativity instance for DistinctionNat multiplication. Downstream it is used heavily: CostAlgebra builds CommSemigroup/CommMonoid instances for shifted cost carriers (shiftedCompose and shiftedComposeH) whose mul_assoc clauses need an associative product; PhiRing's integer-phi structure and gap-weight positivity arguments rely on the same arithmetic spine; CosmogenesisSim's flow-product conservation rewrites with mul_assoc when posting paired events; AlphaGenesis resummation forcing and J-cost small-strain bounds sit further up the same dependency cone.
In the Recognition stack this is scaffolding for native divisibility and prime orbits on the distinction ladder, not a physics forcing step (T5–T8) by itself. It closes the monoid law so later orbit-divisibility lemmas (units, primes, nontrivial factorization) can treat DistinctionNat as a genuine multiplicative monoid rather than a bare inductive type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.