pith. machine review for the scientific record. sign in
theorem proved term proof high

recognitionThetaTerm_two

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 202theorem recognitionThetaTerm_two (t : ℝ) :
 203    recognitionThetaTerm t 2 = 0 := by

proof body

Term-mode proof.

 204  unfold recognitionThetaTerm
 205  rw [chi8_two]
 206  ring
 207
 208/-- Even-residue terms vanish.  Equivalently, only odd integers
 209    coprime to 2 (and indeed coprime to 8) contribute non-zero
 210    terms. -/

depends on (3)

Lean names referenced from this declaration's body.