chi8_mod4
plain-language theorem explainer
The theorem shows that the mod-8 character χ₈ vanishes on every natural number congruent to 4 modulo 8. Number theorists building wheel sieves or modular filters for small primes would cite this case when enumerating residue classes. The proof is a one-line wrapper that unfolds the definition of χ₈ and reduces the argument via Nat.add_mod.
Claim. For every natural number $k$, the mod-8 character satisfies $χ_8(8k + 4) = 0$, where $χ_8(n)$ returns zero on all even residues modulo 8.
background
The module introduces modular arithmetic tools for wheel filters that certify coprimality to 840 and thereby exclude the primes 2, 3, 5, 7. The central object is the mod-8 character χ₈, defined by cases on $n % 8$: it equals zero for residues 0, 2, 4, 6; +1 for 1, 7; and -1 for 3, 5. The upstream definition in RecognitionTheta supplies the corresponding real-valued version that likewise vanishes on evens and alternates signs on the odd residues.
proof idea
The term proof unfolds the definition of χ₈ and invokes Nat.add_mod to compute (8 * k + 4) % 8 = 4, which the match expression maps directly to zero.
why it matters
This lemma supplies one of the eight explicit residue cases required by the eight-tick octave (T7) in the Recognition Science forcing chain. It supports the modular soundness statements that underpin wheel-840 constructions in the module documentation. No downstream theorems are recorded, leaving the full set of χ₈_mod lemmas as scaffolding for later sieve applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.