recognitionThetaTruncated
plain-language theorem explainer
recognitionThetaTruncated supplies the partial sum of the first N terms of the Recognition Theta series for numerical checks and truncation arguments. Analysts working on finite approximations to the modular theta or on explicit evaluations at small cutoffs cite this definition directly. The construction is a direct summation over Finset.range N of the individual weighted terms that embed the 8-tick character and phi-rung scaling.
Claim. The truncated Recognition Theta at cutoff $N$ is defined by the finite sum $S_N(t) = ∑_{n=0}^{N-1} χ_8(n) φ^{-r(n)} exp(-t · c(n))$, where $r(n)$ denotes the phi-rung index, $χ_8$ the mod-8 character, and $c(n)$ the cost-spectrum value of the $n$-th term.
background
The module constructs the Recognition Theta as a candidate completion of the ordinary cost theta Σ exp(-t c(n)) that incorporates the eight-tick character (T7) and the phi-ladder weighting (T6) so that a modular identity under $t ↦ 1/t$ becomes plausible. Core supporting definitions are phiRung n (completely additive, r(p) = ⌊log_φ p⌋ on primes), chi8 (the simplest nontrivial real character mod 8), and recognitionThetaTerm t n = chi8 n · φ^{-phiRung n} · exp(-t · costSpectrumValue n), whose value at n=1 is identically 1.
proof idea
The declaration is a one-line definition that unfolds directly to the Finset sum over range N of recognitionThetaTerm t n. No auxiliary lemmas are invoked; the body simply assembles the partial sum that the downstream evaluation theorems then simplify by unfolding and simp.
why it matters
The definition supplies the concrete object needed by the three immediate downstream theorems recognitionThetaTruncated_zero, _one and _two that compute its values at N=0,1,2. It therefore implements the finite-truncation layer required for numerical work and for the truncation arguments referenced in the module doc-comment, while the full modular identity remains a hypothesis structure (Sub-conjecture A.2).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.