primeJcost_pos
Any prime p in an abstract PrimeNormStructure has strictly positive J-cost. Researchers formalizing the universal cost spectrum or the Cost-Reciprocity synthesis cite this to anchor positivity of the full cost function on nonzero Finsupp elements. The proof is a direct term-mode wrapper that unfolds the definition and feeds the norm-greater-than-one axiom into the general J-cost positivity lemma via two linarith steps.
claimFor every element $p$ of a type $P$ carrying a norm function with value strictly greater than one, the associated J-cost satisfies $0 < Jcost(norm(p))$.
background
The module abstracts prime-cost constructions to any type $P$ equipped with the PrimeNormStructure typeclass. This class supplies a real-valued norm map together with the axiom that the norm of every element exceeds one; both ordinary primes in the naturals and monic irreducibles over finite fields are instances. The auxiliary definition primeJcost then applies the J-cost map (imported from the Cost module) to this norm, yielding the cost attached to each abstract prime generator.
proof idea
The term proof first unfolds primeJcost to expose the direct application of Jcost to the norm. It then invokes the upstream lemma Jcost_pos_of_ne_one (appearing in Cost, JcostCore and LocalCache) and discharges the two side conditions (norm positive and norm not equal to one) by linarith on the norm_gt_one axiom of PrimeNormStructure.
why it matters in Recognition Science
The lemma supplies the first conjunct of the master certificate universal_cost_certificate and is used to prove universalCost_pos for any nonzero finitely supported function. It therefore closes the positivity requirement for the prime generators in the abstract cost-spectrum framework that the Cost-Reciprocity synthesis paper treats as the common substrate for all Selberg-class L-functions.
scope and limits
- Does not establish positivity for composite or non-prime elements.
- Does not compute explicit numerical values of the cost.
- Does not relax the norm-greater-than-one hypothesis.
- Does not address analytic continuation or convergence questions.
Lean usage
example (p : Nat.Primes) : 0 < primeJcost p := primeJcost_pos pformal statement (Lean)
80theorem primeJcost_pos (p : P) : 0 < primeJcost p := by
proof body
Term-mode proof.
81 unfold primeJcost
82 apply Jcost_pos_of_ne_one
83 · linarith [PrimeNormStructure.norm_gt_one p]
84 · linarith [PrimeNormStructure.norm_gt_one p]
85