chi8_mod0
plain-language theorem explainer
The theorem establishes that the mod-8 character χ₈ vanishes on every multiple of eight. Number theorists formalizing wheel factorizations or modular sieves would cite this basic case. The proof is a one-line wrapper that unfolds the definition of χ₈ and applies simplification to confirm the residue is zero.
Claim. For every natural number $k$, the mod-8 character satisfies $χ_8(8k)=0$, where $χ_8(n)$ equals zero on even residues modulo 8, plus one on residues 1 and 7, and minus one on residues 3 and 5.
background
The mod-8 character χ₈ is defined by cases on n modulo 8: it returns zero on even residues (0,2,4,6), plus one on 1 and 7, and minus one on 3 and 5. This definition appears in the same module and is mirrored by a real-valued version in RecognitionTheta that vanishes on evens and alternates signs on odds. The module develops modular arithmetic tools motivated by wheel factorization, specifically the soundness that numbers coprime to 840 avoid divisibility by 2, 3, 5, or 7.
proof idea
The proof is a one-line wrapper. It unfolds the definition of chi8 and applies the simp tactic to reduce the expression 8*k modulo 8 to zero, yielding the result directly.
why it matters
This result anchors the properties of the eight-tick character χ₈ within the Recognition framework's T7 octave structure. It supports downstream modular filtering in prime sieves, consistent with the eight-tick period. No immediate parent theorems are listed, but it closes a basic case for the character used in wheel-840 constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.