chi8_mod2
plain-language theorem explainer
The declaration shows that the integer-valued mod-8 character χ₈ evaluates to zero at every natural number of the form 8k + 2. Researchers formalizing sieve methods or wheel factorizations would reference this when establishing vanishing conditions for even residues. The proof is a direct term-mode reduction that unfolds the definition of χ₈ and simplifies the resulting modular expression via Nat.add_mod.
Claim. For every natural number $k$, the mod-8 character satisfies $χ_8(8k + 2) = 0$, where $χ_8(n)$ returns 0 on residues 0, 2, 4, 6 mod 8, +1 on 1 and 7, and -1 on 3 and 5.
background
This result belongs to the NumberTheory.Primes.Modular module, which develops modular filters motivated by wheel factorization for primes. The central object is the mod-8 character χ₈, defined by cases on n mod 8: it vanishes on all even residues and alternates in sign on the odd ones. The upstream definition in the same module supplies the exact case distinction, while the RecognitionTheta version provides the real-valued counterpart used in the broader Recognition Science framework. The module documentation emphasizes soundness of such filters for excluding small prime factors.
proof idea
The proof unfolds the definition of χ₈ and then applies the simp tactic to the expression involving Nat.add_mod, which reduces (8*k + 2) mod 8 to 2 and matches the zero case.
why it matters
This theorem completes one of the eight modular cases for χ₈, supporting the eight-tick structure (T7) in the Recognition Science forcing chain. It contributes to the wheel-840 construction by confirming that numbers congruent to 2 mod 8 are filtered out as even. Although no direct downstream uses appear yet, it underpins later claims about coprimality to 840 and the exclusion of the prime 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.