chi8_mod1
The declaration proves that the mod-8 character χ₈ evaluates to +1 on every natural number congruent to 1 modulo 8. Number theorists building wheel factorizations or modular sieves would cite it to simplify character sums over arithmetic progressions. The proof is a direct term-mode reduction that unfolds the definition and applies modular arithmetic simplification.
claimFor every natural number $k$, let $n = 8k + 1$. Then the mod-8 character satisfies $χ_8(n) = 1$, where $χ_8(n) = 0$ if $n ≡ 0,2,4,6$ (mod 8), $χ_8(n) = +1$ if $n ≡ 1,7$ (mod 8), and $χ_8(n) = -1$ if $n ≡ 3,5$ (mod 8).
background
The module develops modular tools for prime-related arguments in Recognition Science, beginning with the wheel-840 filter whose soundness rests on coprimality to 840 excluding divisibility by 2, 3, 5, 7. The central definition is the mod-8 character χ₈ on naturals, given by case analysis on n % 8 that returns 0 on even residues, +1 on residues 1 and 7, and -1 on residues 3 and 5. An upstream definition in RecognitionTheta supplies the corresponding real-valued character on odd inputs, with the same sign pattern for residues 1, 3, 5, 7.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of χ₈ and invokes the simplifier with Nat.add_mod to reduce (8 * k + 1) % 8 to 1, which selects the case returning +1.
why it matters in Recognition Science
This result supplies one entry in the explicit evaluation table for χ₈, enabling later modular reductions inside the prime theory layer. It directly supports the eight-tick octave structure by tabulating the periodic character of period 8. No parent theorems appear among the top used-by edges, so the lemma functions as foundational scaffolding for wheel-840 and periodicity arguments in the same module.
scope and limits
- Does not establish values of χ₈ on any residue class other than 1 mod 8.
- Does not relate the integer-valued χ₈ to its real-valued version in RecognitionTheta.
- Does not address coprimality to 840 or wheel-840 soundness.
- Does not connect to the forcing chain, J-uniqueness, or phi-ladder constructions.
formal statement (Lean)
52@[simp] theorem chi8_mod1 (k : ℕ) : chi8 (8 * k + 1) = 1 := by
proof body
Term-mode proof.
53 unfold chi8
54 simp [Nat.add_mod]
55