chi8
plain-language theorem explainer
The mod-8 character χ₈ maps each natural number to an integer that vanishes on even residues modulo 8, returns +1 on residues 1 and 7, and returns -1 on residues 3 and 5. Number theorists building sieve or wheel-factorization arguments inside the Recognition framework cite this definition when they need an explicit integer-valued filter for mod-8 periodicity. The definition is realized by exhaustive pattern matching on the remainder n % 8.
Claim. The function χ₈ : ℕ → ℤ satisfies χ₈(n) = 0 whenever n ≡ 0,2,4,6 (mod 8), χ₈(n) = 1 whenever n ≡ 1,7 (mod 8), and χ₈(n) = -1 whenever n ≡ 3,5 (mod 8).
background
The module introduces modular tools for prime-friendly wheels, beginning with the soundness of wheel-840 that excludes the primes 2,3,5,7. The character χ₈ supplies the mod-8 gate used throughout the subsequent lemmas. It is the integer-valued counterpart of the real character defined upstream in RecognitionTheta, which records the same eight-tick alternation but returns values in ℝ.
proof idea
The definition proceeds by direct case analysis on the remainder when n is divided by 8, assigning the prescribed integer to each of the eight residue classes and defaulting to zero on any unexpected remainder.
why it matters
This definition supplies the common reference for the eight modular evaluation lemmas (chi8_mod0 through chi8_mod7) and the equivalence chi8_eq_zero_iff_even that appears immediately downstream. It encodes the eight-tick octave (T7) of the forcing chain and supplies the concrete filter needed for wheel factorization in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.