logChar_one
plain-language theorem explainer
Any real prime-weight assignment has log-character zero at 1. Cite this as the unit normalization when building additive characters from prime axes. The proof unfolds the factorization sum and simplifies: 1 has empty support, so the weighted sum is zero.
Claim. For every weight assignment $a:\mathbb{N}\to\mathbb{R}$, the additive extension of $a$ through prime factorization evaluates to $0$ at $1$.
background
In Prime Axis Coherence, each prime is an independent axis carrying a real weight $a(p)$. The log-character is the additive extension of those weights through prime factorization: for $n=\prod p^k$ it returns $\sum k,a(p)$. The definition is the natural bridge from free prime weights to a function on all naturals.
The surrounding module develops freedom of weight assignments before coherence is imposed. Multiplicativity on products and evaluation on primes are sibling facts; the value at the unit is the base case of that additive structure. Upstream cost-algebra multiplicativity and axis-independence supply the broader language of free axes, but are not needed for this identity.
proof idea
Unfold the log-character definition. The sum runs over the prime factorization of $1$, which is the empty Finsupp, so the sum is definitionally $0$. A single simp closes the goal. No external lemmas are required.
why it matters
This is the unit clause for the log-character. It underwrites the freedom statement that every weight assignment extends to a multiplicative character additive on products of nonzero naturals, with prime axes independent before coherence enters. Sibling results cover multiplicativity on products, evaluation at primes, faithfulness, and the power-law alignment criterion that leads to prime-axis coherence. In the Recognition foundation layer it normalizes characters on free prime axes prior to J-cost or forcing-chain constraints (T5--T8). The export graph lists no direct dependents, yet as a @[simp] lemma it keeps later character calculations reduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.