chi8_mod5
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish χ₈ values for any residue other than 5 modulo 8.
- Does not address the RecognitionTheta variant of χ₈ or higher moduli.
- Does not prove coprimality or primality statements.
formal statement (Lean)
68@[simp] theorem chi8_mod5 (k : ℕ) : chi8 (8 * k + 5) = -1 := by
proof body
Term-mode proof.
69 unfold chi8
70 simp [Nat.add_mod]
71