logChar_mul
plain-language theorem explainer
Any real weight assignment on primes extends additively through factorization: the log-character of a product of nonzero naturals is the sum of the log-characters. This is the freedom half of prime-axis coherence: axes stay independent until a global scale is imposed. Cited by the Phase 5 headline and by the synchronized-character power-map theorem. Proof is factorization multiplicativity plus Finsupp sum additivity.
Claim. For any weight map $a:\mathbb{N}\to\mathbb{R}$ and any $m,n\in\mathbb{N}$ with $m\neq 0$ and $n\neq 0$, the additive extension of $a$ through prime factorization satisfies $\chi_a(mn)=\chi_a(m)+\chi_a(n)$, where $\chi_a(n)=\sum_p v_p(n)\,a(p)$.
background
In the Prime Axis Coherence module, each prime is an independent axis carrying a real weight $a(p)$. The log-character is the unique additive extension of those weights through the prime factorization of $n$: $\chi_a(n)=\sum_p v_p(n),a(p)$, written in Lean as a Finsupp sum over n.factorization.
Multiplicativity of factorization on nonzero naturals is classical: $v_p(mn)=v_p(m)+v_p(n)$. The present lemma lifts that identity to the weighted sum, so every assignment $a$ automatically defines a completely additive arithmetic function on $\mathbb{N}_{>0}$. No relation among the $a(p)$ is assumed; that is the content of the Freedom paragraph in the doc-comment.
Downstream, alignment of the $a(p)$ to a single log-scale turns $\chi_a$ into $c\log n$ and $\exp\circ\chi_a$ into the power map $n\mapsto n^c$. The present additivity is the structural prerequisite for that collapse.
proof idea
Unfold the definition of the log-character to a Finsupp sum over factorization. Rewrite the factorization of the product via Nat.factorization_mul (valid because $m,n\neq 0$), which replaces the summand index by the pointwise sum of the two factorizations. Apply Finsupp.sum_add_index': the zero-homomorphism side is immediate by simp, and the additivity side is $(k_1+k_2)\cdot a(p)=k_1\cdot a(p)+k_2\cdot a(p)$ after push_cast and ring. No special properties of $a$ are used.
why it matters
This is the Freedom clause of Phase 5. The headline theorem prime_axis_coherence packages three facts: (i) every weight assignment yields a multiplicative character (this lemma), (ii) distinct prime weights give distinct characters (faithful), and (iii) a global power law against a fixed reference holds iff the weights are aligned (powerLaw_iff_aligned). Coherence is then the synchronization of independent prime axes into one scale.
It is also the first step inside character_is_rpow: once weights are locked to $a(p)=c\log p$, additivity plus the log-product formula produce $\chi_a(n)=c\log n$, hence $\exp(\chi_a(n))=n^c$. In the broader Recognition chain this is the arithmetic skeleton on which later mass-ladder and gap constructions sit; it does not yet force $\phi$, the eight-tick octave, or $D=3$, but it supplies the free multiplicative characters those structures will later constrain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.