twistedPrimeCostSum_zero
plain-language theorem explainer
The twisted prime cost sum up to zero vanishes for any real-valued function chi. Researchers building inductive arguments on partial sums in twisted arithmetic functions would cite this base case when the cutoff is empty. The proof is a one-line simplification that unfolds the sum definition and discards the zero term via the fact that zero is not prime.
Claim. For any function $chi : ℕ → ℝ$, the partial sum $Π_chi(0) := ∑_{p ≤ 0, p prime} J(p) chi(p) equals 0.
background
The Cost-Twisted L-Series module extends the prime cost spectrum by twisting with a completely multiplicative function chi : ℕ → ℝ. The twisted prime cost sum is defined as the finite sum over primes p ≤ N of primeCost p times chi(p), where primeCost p extracts the J-cost of the prime. J-cost itself is the derived cost of a multiplicative recognizer comparator, equivalently the J-function J(x) = (x + x^{-1})/2 - 1 applied to positive ratios. The definition iterates over the range 0 to N and returns zero on non-primes.
proof idea
The proof is a one-line wrapper that applies simp to the definition of twistedPrimeCostSum together with the lemma that zero is not prime, so the single candidate term at p=0 contributes nothing to the sum.
why it matters
This zero-case identity anchors the twisted prime cost sums that generalize the untwisted spectrum to character-twisted L-series in the Recognition framework. It supplies the base for any later inductive development of Π_chi(N) and aligns with the J-uniqueness step (T5) and the Recognition Composition Law. No downstream theorems are recorded yet, but the result closes the empty-range case required by the forcing chain that derives spatial dimension D=3 from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.