logChar_log
plain-language theorem explainer
With reference weights w(p) = log p, the additive log-character of any positive natural n equals the ordinary real logarithm of n. Anyone proving that synchronized prime-axis characters collapse to a single global power law cites this identity. The argument expands the factorization sum, rewrites n as a product of prime powers over the reals, and applies the product and power rules for Real.log.
Claim. For every positive natural number $n$, if the prime weights are the ordinary logarithms $w(p)=\log p$, then the log-character of $n$ equals the real logarithm: $\sum_{p\mid n} v_p(n)\,\log p = \log n$.
background
In the Primitive Recognition Calculus, each prime is treated as an independent axis. A weight assignment $a:\mathbb{N}\to\mathbb{R}$ records the log-value on that axis. The log-character extends $a$ additively through prime factorization: for $n\neq 0$, $$\mathrm{logChar}(a,n)=\sum_p v_p(n),a(p),$$ where $v_p(n)$ is the $p$-adic valuation (the multiplicity in the factorization support).
The present lemma specializes to the continuum reference scale $a(p)=\log p$. That choice is the one selected by the order/continuum condition in the surrounding module: it is the unique weight system for which the discrete character matches the ordinary real logarithm on every positive integer.
Upstream, the definition of the log-character and the standard Mathlib factorization identity $n=\prod_p p^{v_p(n)}$ are the only structural inputs. Positivity of prime powers is used only to justify the logarithm of a product.
proof idea
Unfold the log-character to a Finsupp sum over the factorization support. Invoke $\mathrm{Nat.factorization_prod_pow_eq_self}$ to recover $n$ as that product of prime powers, then cast the identity into $\mathbb{R}$. Rewrite the goal as equality of $\log n$ with $\log$ of the product, apply $\mathrm{Real.log_prod}$ (side condition: each prime-power factor is strictly positive, from primality), and finish by $\mathrm{Real.log_pow}$ termwise on the sum.
why it matters
This is the calibration step for prime-axis coherence. Downstream, $\mathrm{character_is_rpow}$ quotes it to prove that any weight system aligned to a constant multiple of $\log p$ yields a pure power map $n\mapsto n^c$ after exponentiation. In Recognition Science language: once independent prime axes lock to a single logarithmic scale, the discrete character becomes a global power law on the positive rationals.
That power-law form is the bridge from the discrete PRC ledger to continuum scaling (phi-ladder rungs, spectral indices, and monotone multiplicative cost). The lemma itself is pure number theory; its place in the framework is as the reference-scale identity that the order/continuum condition selects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.