chi8_five
plain-language theorem explainer
The declaration proves that the eight-tick character evaluates to negative one at five. Workers formalizing the Recognition Theta series cite this value to fix the sign of the fifth summand. The proof is a direct term reduction that unfolds the character definition and closes by reflexivity.
Claim. The eight-tick character satisfies $χ_8(5) = -1$.
background
The Recognition Theta function augments the cost theta series with the eight-tick character (T7) and phi-ladder weights (T6) to support a modular identity under t ↦ 1/t. The character chi8 is defined by cases on n modulo 8: it returns +1 for residues 1 and 3, -1 for 5 and 7, and zero for even residues. This evaluation is one of several chi8 lemmas that pin down signs for odd integers in the theta sum.
proof idea
The term proof unfolds the definition of chi8 and applies reflexivity to verify the match for input 5.
why it matters
This result supplies an explicit sign for the n=5 term in the Recognition Theta sum, supporting the elementary properties listed in the module. It instantiates the eight-tick character required by the T7 octave in the forcing chain. The evaluation contributes to the arithmetic foundation before the modular identity is imposed as a hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.