logChar
plain-language theorem explainer
Defines the log-character of a natural number from an arbitrary assignment of real weights to primes: sum multiplicity times weight over the prime factorization. Anyone working on prime-axis coherence or multiplicative characters on ℕ cites it as the basic additive lift. The body is a one-line Finsupp sum over Nat.factorization.
Claim. For a weight assignment $a:\mathbb{N}\to\mathbb{R}$ and $n\in\mathbb{N}$, the log-character is $\mathrm{logChar}(a,n)=\sum_{p^{k}\| n} k\, a(p)$, the sum of multiplicity times weight over the prime factorization of $n$ (empty sum is $0$).
background
In the Prime Axis Coherence module, each prime is treated as an independent axis that can carry a real log-weight. A map $a:\mathbb{N}\to\mathbb{R}$ is read only on primes: $a(p)$ is the log-value assigned to the prime axis $p$.
The log-character is the unique additive extension of those weights through unique factorization. Writing $n=\prod p^{k_p}$, one sets $\mathrm{logChar}(a,n)=\sum k_p, a(p)$. For $n=1$ the factorization is empty, so the value is $0$. Multiplicativity of the underlying character is then equivalent to additivity of this sum on products of nonzero naturals.
The reference scale is the ordinary logarithm on primes, $w(p)=\log p$. Against that scale one later asks whether a character is a pure power law (single global exponent) and whether the prime weights are aligned.
proof idea
Pure definition: unfold to the Finsupp sum of $n$.factorization, sending each prime power contribution $(p,k)$ to $(k:\mathbb{R})\cdot a, p$. No lemmas are applied; noncomputable only because factorization and real arithmetic are involved.
why it matters
This is the primitive object of the prime-axis calculus. Downstream, logChar_one and logChar_mul establish that every weight assignment extends to a multiplicative character (freedom of the axes). faithful shows the axes are independent coordinates: agreement of log-characters on all naturals recovers the prime weights. IsPowerLaw and WeightsAligned phrase global power-law structure as a single exponent relating two log-characters; powerLaw_iff_aligned equates that to pointwise alignment on primes. logChar_log identifies the reference weights $p\mapsto\log p$ with the ordinary real logarithm, and character_is_rpow upgrades aligned characters to genuine power maps $n\mapsto n^c$. Together these feed prime_axis_coherence: once independent prime axes lock to one log scale, they produce a single global power law on the positive rationals, the continuum/order condition that selects the recognition scale in the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.