recognitionThetaTerm_even
plain-language theorem explainer
The Recognition Theta term vanishes for every even natural number n. Researchers formalizing the structural properties of the Recognition Theta function ahead of its modular identity would cite this to restrict the sum to odd indices. The proof unfolds the term definition, shows via case analysis on n mod 8 that the mod-8 character vanishes on even residues, and finishes with algebraic simplification.
Claim. Let $n$ be an even natural number and let $t$ be real. Then the $n$-th term of the Recognition Theta sum is identically zero.
background
The Recognition Theta function is the candidate completion of the cost theta sum that incorporates the 8-tick character and the phi-ladder weight so as to inherit a modular identity under $t$ to $1/t$. The module defines the term as the contribution from each integer $n$, built from the completely additive phi-rung index and the character chi8 mod 8. This lemma belongs to the elementary arithmetic layer that precedes the convergence and modular-identity hypotheses (Sub-conjectures A.1 and A.2).
proof idea
The proof unfolds the definition of the term, then establishes that chi8 n equals zero by unfolding chi8, deriving that n even forces n mod 8 even, and applying interval_cases on the eight possible residues mod 8. The even cases (0,2,4,6) return zero by definition of chi8; the result follows by rewriting the zero and applying the ring tactic.
why it matters
The lemma supplies one of the structural facts collected in the Recognition Theta certificate theorem. It enforces the eight-tick octave (T7) by eliminating even indices, consistent with the period-8 character required by the forcing chain. The modular identity itself remains a hypothesis; this result isolates the arithmetic content that any future Poisson-summation argument must respect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.