recognitionThetaTruncated_one
plain-language theorem explainer
The finite truncation of the Recognition Theta at level N=1 evaluates to zero for every real t. Researchers building inductive arguments or numerical checks on partial sums of the cost theta would cite this base case. The proof is a one-line wrapper that unfolds the sum definition and simplifies the singleton range containing only the n=0 term.
Claim. Let $N=1$ and let $t$ be real. The truncated Recognition Theta function defined by the finite sum of terms from $n=0$ to $N-1$ satisfies $0$.
background
The Recognition Theta function is the candidate completion of the cost theta function that incorporates the 8-tick character and the phi-ladder weight so as to inherit a modular identity under $t$ to $1/t$. The truncated version is the finite sum up to $N-1$ of the individual terms, each built from the phi-rung index and the character mod 8. This module formalizes the elementary arithmetic properties provable without the full Poisson summation hypothesis.
proof idea
The proof is a one-line wrapper that unfolds the definition of the truncated sum and applies simplification to the sum over Finset.range 1, which reduces to the single term at n=0 whose contribution is zero.
why it matters
This base case anchors the finite approximations used to approach the eight-tick octave and phi-ladder fixed point. It supplies the evaluation at the smallest truncation level as part of the structural properties provable from arithmetic, prior to the modular identity hypothesis. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.