universalCost_pos
plain-language theorem explainer
The universal cost on a nonzero finitely supported function over a prime norm structure is strictly positive. Number theorists studying abstract cost spectra for the Selberg class would cite this to guarantee that the spectrum vanishes only at the zero element. The proof extracts one prime with positive multiplicity from the support and splits the sum into a nonnegative remainder plus one strictly positive term.
Claim. Let $P$ be equipped with a norm structure. For any nonzero $f : P →_0 ℕ$, the universal cost satisfies $0 < ∑_p f(p) · J(‖p‖), where $J$ is the Recognition Science cost function on positive reals.
background
The module abstracts the prime cost spectrum to any PrimeNormStructure P, a typeclass supplying a set of primes together with a real norm ‖p‖ > 1. The universal cost is defined by c(f) := Σ_p f(p) · J(‖p‖) on finitely supported maps f : P →_0 ℕ. This construction unifies classical primes and monic irreducibles in F_q[T] and supplies the elementary arithmetic properties needed for the Cost-Reciprocity synthesis paper.
proof idea
The tactic proof invokes Finsupp.support_nonempty_iff to obtain a prime p with f p > 0. It applies primeJcost_pos to obtain 0 < primeJcost p, casts the coefficient to reals, and forms the positive product via mul_pos. After unfolding universalCost and rewriting the sum via Finset.sum_erase_add, it applies add_pos_of_nonneg_of_pos. The erased sum is shown nonnegative by Finset.sum_nonneg together with mul_nonneg and primeJcost_nonneg.
why it matters
The result is invoked by the master certificate universal_cost_certificate that bundles all elementary properties of the universal cost spectrum. It supplies the strict-positivity clause required by the module's abstract framework, which treats every cost spectrum in the Selberg class as an instance of the same J-based construction. The step aligns with the Recognition Science derivation of cost from the J-function and the multiplicative recognizer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.