chi8_mod5
plain-language theorem explainer
The mod-8 character χ₈ evaluates to -1 at every natural number congruent to 5 modulo 8. Number theorists working on wheel factorizations or mod-8 case splits in prime sieves would cite this reduction. The proof is a one-line wrapper that unfolds the definition of χ₈ and simplifies the arithmetic via Nat.add_mod.
Claim. For every natural number $k$, let $n = 8k + 5$. Then the mod-8 character satisfies $χ_8(n) = -1$, where $χ_8$ returns -1 precisely on residues 3 and 5 modulo 8 and vanishes on even residues.
background
The mod-8 character χ₈ is defined by cases on $n % 8$: it returns 0 on even residues 0,2,4,6; +1 on 1 and 7; and -1 on 3 and 5. A parallel definition in RecognitionTheta records the 8-tick real character that vanishes on evens and alternates +1 on 1 and 3, -1 on 5 and 7. The module develops modular tools for wheel factorization, ensuring numbers coprime to 840 avoid the small primes 2,3,5,7.
proof idea
The term proof unfolds the local definition of chi8, then applies simp with the lemma Nat.add_mod to reduce (8*k + 5) % 8 to 5, which matches the -1 case.
why it matters
This lemma supplies one of the eight exhaustive residue cases for the period-8 character χ₈ that appears in the eight-tick octave (T7) of the forcing chain. It supports modular reductions inside prime sieves and wheel-840 constructions. No downstream theorems are recorded yet, but the result closes the residue-5 slot in the mod-8 filter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.