chi8
plain-language theorem explainer
The 8-tick real character χ₈ maps each natural number n to +1 when n ≡ 1 or 3 mod 8, to -1 when n ≡ 5 or 7 mod 8, and to 0 otherwise. Constructions of the Recognition Theta function cite this definition to insert the eight-tick structure required by forcing-chain step T7. The definition is realized by direct pattern matching on the remainder n % 8.
Claim. $χ_8 : ℕ → ℝ$ is defined by $χ_8(n) = 1$ if $n ≡ 1,3$ (mod 8), $χ_8(n) = -1$ if $n ≡ 5,7$ (mod 8), and $χ_8(n) = 0$ otherwise.
background
The Recognition Theta module constructs a candidate completion Θ̃_RS(t) of the cost theta function Θ_J(t) by adjoining the 8-tick character (T7) to the phi-ladder weights (T6). The character vanishes on even integers and alternates signs on odd integers according to residue class modulo 8, supplying the periodic factor needed for a possible modular identity under t ↦ 1/t. The module states the full modular identity as a hypothesis structure while proving elementary arithmetic facts with zero sorrys.
proof idea
The definition is a direct match expression on n % 8 that returns the four prescribed values for the odd residues and defaults to zero for all even residues. No lemmas are invoked; the implementation is a one-line wrapper around the built-in modulo operation.
why it matters
This definition supplies the eight-tick character required by the Recognition Theta construction and is referenced by the modular arithmetic theorems chi8_eq_zero_iff_even, chi8_mod0 through chi8_mod3 in the Primes.Modular module. It realizes forcing-chain step T7 (eight-tick octave of period 2^3) inside the theta sum, allowing the period-8 factor to combine with the phi-ladder. The remaining open questions are the modular identity and convergence, both encoded as hypothesis structures in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.