recognitionThetaTruncated_zero
plain-language theorem explainer
The finite truncation of the Recognition Theta at zero terms evaluates to zero for every real scaling parameter t. Researchers constructing finite approximations ahead of the modular identity would cite this base case. The proof is a one-line wrapper that unfolds the partial-sum definition and reduces the empty sum via simplification.
Claim. For any real number $t$, the truncated Recognition Theta satisfies $tilde Theta_RS(t,0)=0$, where the truncation is the partial sum over $n$ in Finset.range $N$ of the term recognitionThetaTerm $t$ $n$ evaluated at $N=0$.
background
The Recognition Theta is the candidate completion of the cost theta sum that folds in the 8-tick character and phi-ladder weights so as to support a modular identity under $t mapsto 1/t$. The truncated version is introduced as a finite-sum approximation for numerical checks and truncation theorems. Its definition is the sum over the first $N$ terms of recognitionThetaTerm $t$ $n$, each term carrying the exponential cost factor together with the rung and character multipliers.
proof idea
The proof is a one-line wrapper that unfolds the definition of recognitionThetaTruncated and applies the simp tactic to reduce the empty sum (range 0) to zero.
why it matters
This zero base case anchors all subsequent finite-truncation arguments in the Recognition Theta module. It supplies the starting point before the hypothesis structures for convergence (Sub-conjecture A.1) and the modular identity (Sub-conjecture A.2) that invoke the phi-ladder Poisson summation. The result sits inside the elementary arithmetic layer that precedes the T7 eight-tick and T6 phi-ladder landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.