recognitionThetaTerm_zero
plain-language theorem explainer
Recognition Theta term vanishes at n=0 for any real scaling parameter t. Analysts of the modular completion of the cost theta series cite this vanishing to handle the origin in the sum. The argument unfolds the explicit term formula and reduces via simplification.
Claim. For every real number $t$, the zero-indexed term of the Recognition Theta function satisfies $χ_8(0) ⋅ ϕ^{-r(0)} exp(-t ⋅ c(0)) = 0$, where $r$ is the phi-rung index and $c$ the cost spectrum value.
background
The Recognition Theta function is constructed as a sum whose n-th term is χ₈(n) ⋅ ϕ^{-r(n)} ⋅ exp(-t ⋅ c(n)), with r the phi-rung index (completely additive, r(p) = ⌊log_ϕ p⌋ for primes) and χ₈ the mod-8 character. This module builds the candidate modular completion of the cost theta function Θ_J(t) by incorporating the eight-tick character and phi-ladder weights so the sum can inherit a t ↦ 1/t identity. The upstream definition of recognitionThetaTerm supplies the explicit product formula used here.
proof idea
One-line wrapper that unfolds the definition of recognitionThetaTerm and applies simp, which reduces the product to zero from the character value χ₈(0) = 0.
why it matters
This base case anchors term evaluation inside the Recognition Theta construction, which targets the modular identity (Sub-conjecture A.2) via the eight-tick octave (T7) and phi-ladder (T6). It supports later properties such as recognitionThetaTerm_pos and the constant term at n=1, preparing the ground for the full sum and its convergence hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.