chi8_mod7
plain-language theorem explainer
The mod-8 character evaluates to +1 on every natural number congruent to 7 modulo 8. Number theorists formalizing sieve methods or quadratic character sums would cite this when reducing evaluations over arithmetic progressions. The proof is a one-line wrapper that unfolds the piecewise definition and simplifies the residue via modular arithmetic.
Claim. For every natural number $k$, let $n=8k+7$. Then the mod-8 character satisfies $n=8k+7$ implies $n$ is odd and $n$ mod 8 equals 7, so the character equals +1.
background
The module supplies modular filters for wheel factorization, beginning with the 840-wheel that excludes multiples of the small primes 2, 3, 5 and 7. The character chi8 is defined by cases on n mod 8: it returns 0 on even residues, +1 on residues 1 and 7, and -1 on residues 3 and 5. This theorem belongs to the family of mod-r lemmas that establish the full table of values for the character.
proof idea
The proof is a one-line wrapper. It unfolds the definition of chi8, then applies the simp tactic with the lemma Nat.add_mod to reduce (8*k + 7) mod 8 to 7, which the case analysis maps directly to 1.
why it matters
The result completes the case analysis for residue 7, supplying one of the eight required evaluations that together confirm the 8-tick periodicity of the character. It supports the modular arithmetic layer used in prime sieving and aligns with the eight-tick octave (T7) in the forcing chain. No downstream theorems are recorded yet, so the lemma remains available for later character-sum reductions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.