chi8_ne_zero_iff_odd
plain-language theorem explainer
chi8(n) is nonzero precisely when the natural number n is odd. Number theorists constructing modular filters or wheel factorizations would cite the equivalence to isolate parity conditions without separate casework. The proof is a one-line term wrapper that negates the evenness statement via congruence and rewrites the result with the standard odd predicate.
Claim. For every natural number $n$, the modular filter value satisfies $chi_8(n) neq 0$ if and only if $n$ is odd.
background
The module develops modular arithmetic and wheel filters that certify soundness for prime sieving: coprimality to 840 forces a number to avoid the prime factors 2, 3, 5, and 7. The filter chi8 is the 8-periodic character whose zero set encodes parity, with the companion result establishing that chi8(n) vanishes exactly on the even numbers. This local setting supplies the basic parity gate needed before higher wheel constructions such as wheel840.
proof idea
The proof is a one-line wrapper that applies not_congr to the evenness equivalence and then simplifies the resulting negation with Nat.not_even_iff_odd.
why it matters
The equivalence supplies the odd-case half of the parity detection for chi8, completing the basic modular filter layer that supports wheel factorization soundness. It aligns with the mod-8 gating step in the Recognition Science forcing chain and feeds the prime-friendly arithmetic used in later number-theoretic scaffolding. No open questions are closed here, but the result removes a routine parity case from downstream proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.