recognitionThetaTerm_one
plain-language theorem explainer
The declaration shows that the first term of the Recognition Theta function equals one for every real t. Researchers constructing the constant term or verifying the truncated sums in the theta expansion would cite it. The proof is a one-line wrapper that unfolds the term definition and simplifies using the vanishing of the cost spectrum at one.
Claim. Let the Recognition Theta term be defined by $Θ(t,n) = χ_8(n) φ^{-r(n)} exp(-t c(n))$, where $χ_8$ is the mod-8 character, $r(n)$ the phi-rung index, and $c(n)$ the cost spectrum value. Then $Θ(t,1) = 1$.
background
The module constructs the Recognition Theta function as a candidate completion of the ordinary cost theta sum that incorporates the eight-tick character and phi-ladder weights. The term itself is the product $χ_8(n) φ^{-r(n)} exp(-t c(n))$, with phiRung supplying the completely additive rung index and chi8 the bounded character mod 8. Upstream, costSpectrumValue_one establishes that the cost spectrum vanishes at one, while the term definition itself encodes the three multiplicative factors whose values at n=1 are each unity.
proof idea
The proof unfolds the definition of recognitionThetaTerm and applies simp with the lemma costSpectrumValue_one. The resulting expression reduces to the product of χ_8(1), φ^0 and exp(0), which equals one by the elementary properties of the character and the rung index at one.
why it matters
This supplies the constant term needed for the structural certificate of the Recognition Theta function and for the evaluation of the truncated sum at N=2. It fills the elementary arithmetic step that supports the eight-tick octave and phi-ladder structure inside the Recognition Science framework, while leaving the analytic sub-conjectures (convergence, modular identity, Mellin factor) as open hypothesis structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.