chi8_mod6
plain-language theorem explainer
The theorem shows that the mod-8 character χ₈ returns zero on every natural number of the form 8k + 6. Number theorists building modular sieves or wheel factorizations cite it as one case in the exhaustive residue analysis modulo 8. The proof is a one-line wrapper that unfolds the character definition and reduces the argument via modular arithmetic.
Claim. For every natural number $k$, let $n = 8k + 6$. Then the mod-8 character satisfies $χ_8(n) = 0$, where $χ_8(m)$ equals 0 on residues 0, 2, 4, 6 modulo 8, equals +1 on residues 1 and 7, and equals -1 on residues 3 and 5.
background
The module introduces modular filters for prime sieves, starting with the soundness of the 840-wheel that excludes multiples of the small primes 2, 3, 5 and 7. The character χ₈ is the integer-valued function defined by cases on n mod 8: it vanishes on all even residues and alternates +1 and -1 on the odd residues 1, 3, 5, 7. This version is distinct from the real-valued χ₈ in RecognitionTheta, which is zero on evens and alternates only on odds. The family of chi8_modN theorems supplies one identity for each residue class modulo 8.
proof idea
The proof is a one-line wrapper. It unfolds the definition of χ₈ and applies the simplification tactic with Nat.add_mod to reduce (8k + 6) mod 8 directly to 6, which the match expression maps to zero.
why it matters
The result fills the residue-6 case in the complete mod-8 case analysis required by the eight-tick octave (T7) of the Recognition framework. It supports the modular gating used in wheel factorization and prime recognition. No downstream theorems are recorded yet, but the declaration pairs with the other chi8_modN siblings to exhaust all classes modulo 8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.