recognitionThetaTruncated_zero
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish convergence of the infinite sum.
- Does not prove the modular identity under $t$ inversion.
- Does not compute values for any positive truncation level.
- Does not invoke the Cayley transform from BRF plumbing.
formal statement (Lean)
236@[simp] theorem recognitionThetaTruncated_zero (t : ℝ) :
237 recognitionThetaTruncated t 0 = 0 := by
proof body
Term-mode proof.
238 unfold recognitionThetaTruncated
239 simp
240
241/-- The truncated theta at `N = 1` includes only `n = 0`. -/