chi8_one
plain-language theorem explainer
The eight-tick character evaluates to one at the integer one. Workers on the Recognition Theta function cite this as the base case in the character definition. The proof is a direct unfolding of the definition followed by reflexivity.
Claim. The eight-tick real character satisfies $χ_8(1) = 1$.
background
The Recognition Theta module constructs a candidate completion of the cost theta function that incorporates the eight-tick character and the phi-ladder weights to achieve modular properties. The eight-tick character is defined to vanish on even natural numbers and to alternate between +1 and -1 on odd numbers according to their residue class modulo 8, specifically taking the value +1 at 1 and 3, and -1 at 5 and 7. This theorem supplies the evaluation at the unit, serving as a base case alongside the upstream definition of the character.
proof idea
The proof unfolds the definition of the eight-tick character and concludes by reflexivity.
why it matters
This result provides the initial value for the eight-tick character used in the Recognition Theta sum. It supports the structural properties listed in the module, including evaluations at specific points, and connects to the eight-tick octave in the forcing chain T7. The full modular identity remains a hypothesis structure pending further development of the phi-ladder Poisson summation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.