chi8_mod3
plain-language theorem explainer
The mod-8 character χ₈ evaluates to -1 on every natural number congruent to 3 modulo 8. Researchers formalizing sieve methods or quadratic character sums would invoke this to handle residue class 3 without case analysis. The proof is a direct reduction: unfolding the definition and simplifying the modulus computation yields the constant -1.
Claim. For every natural number $k$, the mod-8 character satisfies $χ_8(8k + 3) = -1$, where $χ_8(n)$ returns -1 precisely when $n ≡ 3$ or $5$ (mod 8).
background
The module develops modular arithmetic tools for wheel factorization in prime sieves, motivated by mod-8 gating. The character χ₈ is defined by cases on n mod 8: zero on even residues, +1 on 1 and 7, -1 on 3 and 5. This theorem is one of several that tabulate the values on each residue class. It depends on the definition of χ₈ in the same module and a related real-valued version in RecognitionTheta whose doc-comment states: 'χ₈(1) = +1, χ₈(3) = +1, χ₈(5) = -1, χ₈(7) = -1, and zero otherwise.'
proof idea
The term-mode proof unfolds the definition of chi8 and invokes simp on Nat.add_mod to compute (8*k + 3) mod 8 = 3, which the match expression maps to -1.
why it matters
This lemma completes the case analysis for the mod-8 character on odd residues, supporting the eight-tick octave structure (T7) in the Recognition Science forcing chain. It provides the value needed for wheel-840 filters that exclude small primes. No downstream uses are recorded yet, but it closes the modular tabulation started by the chi8 definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.