chi8_mod6
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not evaluate χ₈ on any residue class other than 6 modulo 8.
- Does not extend the result to moduli larger than 8.
- Does not derive any primality or factorization consequences.
- Does not address the real-valued variant of χ₈ defined elsewhere.
formal statement (Lean)
72@[simp] theorem chi8_mod6 (k : ℕ) : chi8 (8 * k + 6) = 0 := by
proof body
Term-mode proof.
73 unfold chi8
74 simp [Nat.add_mod]
75