chi8_two
The theorem establishes that the eight-tick real character evaluates to zero at the integer 2. Researchers constructing the Recognition Theta sum cite this to confirm the n=2 term vanishes identically. The proof is a direct one-line wrapper that expands the character definition and closes by reflexivity.
claim$χ_8(2) = 0$, where $χ_8$ is the real character modulo 8 that vanishes on all even arguments and satisfies $χ_8(1) = +1$, $χ_8(3) = +1$, $χ_8(5) = -1$, $χ_8(7) = -1$.
background
The Recognition Theta function is built as a candidate completion of the cost theta series that folds in the eight-tick character (T7) together with phi-ladder weights (T6) so that a modular identity under $t ↦ 1/t$ becomes plausible. The character $χ_8$ is defined on the naturals by cases on residue modulo 8: it returns zero on even inputs and alternates in sign on odd inputs according to the explicit rule $χ_8(1)=+1$, $χ_8(3)=+1$, $χ_8(5)=-1$, $χ_8(7)=-1$. This evaluation at 2 is one of a short list of base cases that support the structural lemmas for the full Recognition Theta sum.
proof idea
The proof is a one-line wrapper. It unfolds the definition of $χ_8$ (the local match on $n % 8$) and closes immediately by reflexivity, confirming the value 0 at argument 2.
why it matters in Recognition Science
The result is invoked directly by recognitionThetaTerm_two to show that the n=2 term of the Recognition Theta series is identically zero. It therefore supplies one concrete instance of the eight-tick character (T7) vanishing on even arguments, a property required before the modular identity (Sub-conjecture A.2) can be stated. The evaluation belongs to the elementary arithmetic layer that precedes any appeal to Poisson summation on the phi-ladder.
scope and limits
- Does not prove the modular identity under $t ↦ 1/t$.
- Does not evaluate $χ_8$ at any integer other than 2.
- Does not address convergence of the Recognition Theta series.
- Does not incorporate phi-ladder rung weights.
Lean usage
unfold recognitionThetaTerm; rw [chi8_two]; ringformal statement (Lean)
147theorem chi8_two : chi8 2 = 0 := by
proof body
Term-mode proof.
148 unfold chi8; rfl
149
150/-- `χ₈(3) = 1`. -/