recognitionThetaTerm_two
plain-language theorem explainer
The theorem shows that the n=2 term in the Recognition Theta sum is identically zero for every real t. Researchers building the modular completion of the cost theta function cite it to confirm that even residues drop out under the mod-8 character. The proof is a direct algebraic reduction that unfolds the term definition, substitutes the known character value at 2, and simplifies the product to zero.
Claim. For every real number $t$, the second term of the Recognition Theta function vanishes: $χ_8(2) ⋅ ϕ^{-r(2)} exp(-t ⋅ c(2)) = 0$, where $χ_8$ is the character modulo 8, $r(n)$ is the phi-rung index, and $c(n)$ is the cost spectrum value.
background
The Recognition Theta function $Θ̃_RS(t)$ extends the cost theta function $Θ_J(t) = ∑ exp(-t c(n))$ by weighting each term with the 8-tick character $χ_8$ (T7) and the phi-ladder rung index $r(n)$ (T6) to target a modular identity under $t ↦ 1/t$. The module defines the n-th term explicitly as $χ_8(n) ⋅ ϕ^{-r(n)} ⋅ exp(-t ⋅ c(n))$, with $r(n)$ completely additive and $r(p) = ⌊log_ϕ p⌋$ for primes. An upstream result states that $χ_8(2) = 0$.
proof idea
The proof unfolds the definition of the term at n=2, rewrites using the theorem that the character evaluates to zero at 2, and applies ring simplification to reach zero.
why it matters
This result confirms that even residues vanish, so only odd integers coprime to 8 contribute nonzero terms to the sum. It supplies one of the elementary arithmetic facts listed in the module (all with zero sorry) that underpins the Recognition Theta construction ahead of the modular identity hypothesis (Sub-conjecture A.2). The eight-tick character (T7) is the direct source of the vanishing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.