logChar_prime
plain-language theorem explainer
At a prime p the log-character built from weights a recovers exactly the weight a(p). Anyone proving faithfulness of prime axes or the prime-axis coherence theorem cites this identity. The argument unfolds the factorization sum and collapses the single-support Finsupp sum at p.
Claim. For any weight map $a:\mathbb{N}\to\mathbb{R}$ and any prime $p$, the log-character of $a$ at $p$ equals $a(p)$: $\mathrm{logChar}(a)(p)=a(p)$.
background
In this module a log-character is the additive extension of a real weight map $a$ through prime factorization: on $n$ one sums $k\cdot a(p)$ over the prime-power factors $p^k$ in $n$. The value $a(p)$ is the log-weight assigned to the prime axis $p$.
The local setting is prime-axis coherence for Recognition Science characters: whether independent prime weights can be synchronized to a single global scale. The companion one-point identity at $1$ and the multiplicative law for coprime arguments sit beside this lemma; together they say the character is completely determined by its prime weights.
Upstream, the definition of the log-character is exactly that factorization sum. No deeper forcing-chain input is required here; the lemma is pure arithmetic of the support of a prime.
proof idea
Term-style rewrite proof. Unfold the log-character to the factorization sum. Replace the factorization of a prime $p$ by the single-point Finsupp that sends $p$ to multiplicity $1$. Apply the single-index sum identity for Finsupp (the zero-at-missing-keys side condition is discharged by simp). A final simp reduces $1\cdot a(p)$ to $a(p)$.
why it matters
This is the evaluation lemma that makes prime weights genuine coordinates. Downstream, faithfulness rewrites agreement of two characters on all naturals down to agreement of their prime weights by applying the identity at each prime. The Prime-Axis Coherence Theorem (power-law iff weights aligned) likewise evaluates characters on primes via this fact when it compares a global power law against the reference scale to pointwise alignment of prime weights.
In the broader framework the result underwrites the claim that the prime axes are independent coordinates of a character, the discrete skeleton on which continuum/order conditions later force a single scale. It does not itself invoke T5–T8 or the RCL; it is infrastructure those coherence statements sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.