costTheta
plain-language theorem explainer
The cost theta function is introduced as the formal series summing exponentials of negative parameter times a cost sequence on the naturals. Researchers formalizing the Mellin pullback of reciprocal symmetry for the J-cost function cite this definition when building the series representation. The definition is a direct abbreviation using the infinite sum operator from Mathlib.
Claim. Let $t$ be a real parameter and let $c:ℕ→ℝ$ be a cost sequence. The cost theta function is defined by $θ(t,c) := ∑_{n∈ℕ} exp(−t⋅c(n))$.
background
The MellinPullback module shows that the reciprocal symmetry J(x)=J(1/x) of the Recognition Science cost function induces reflection symmetry under the Mellin transform, yielding the abstract form of the zeta functional equation. Upstream results supply the cost function: ObserverForcing.cost defines it as the J-cost of a recognition event, while MultiplicativeRecognizerL4.cost derives it from a comparator on positive ratios. The cost theta function aggregates these into a series at positive t, with convergence following from J(p)>0 and the growth J(p)∼p/2.
proof idea
This is a direct definition that sets the function equal to the tsum over naturals of the exponential term. No lemmas are applied beyond the built-in sum operator.
why it matters
The definition supplies the theta series whose non-negativity is established in the downstream theorem costTheta_nonneg. It supports the module's central claim that the Mellin pullback of J-reciprocal symmetry produces s↔1-s reflection, linking to the Recognition Composition Law and J-uniqueness from the T5 forcing step. It remains an abstract structural result without the Poisson summation or complex analysis needed for the full zeta equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.