chi8_periodic
The mod-8 character χ₈ satisfies χ₈(n + 8k) = χ₈(n) for all natural numbers n and k. Number theorists formalizing Recognition Science would cite this to reduce character evaluations modulo 8 inside wheel factorizations or theta-function arguments. The proof is a short tactic script that unfolds the definition, invokes Nat.add_mod to obtain the congruence (n + 8k) % 8 = n % 8, and finishes by simplification.
claimFor all natural numbers $n$ and $k$, the mod-8 character satisfies $χ_8(n + 8k) = χ_8(n)$, where $χ_8$ takes the value 0 on residues 0, 2, 4, 6, the value +1 on residues 1 and 7, and the value -1 on residues 3 and 5.
background
The module supplies modular-arithmetic tools for prime-friendly wheel filters. Its opening result records that coprimality to 840 excludes the small primes 2, 3, 5, 7. The central definition is the mod-8 character χ₈, which is zero on even residues, +1 on 1 and 7, and -1 on 3 and 5; it is constructed directly from n % 8. Upstream results on Recognition Theta and phase-lift bounds already employ this character to control additive functions and angular Lipschitz constants on the circle.
proof idea
The proof is a tactic-mode script. It unfolds the definition of χ₈, proves the auxiliary congruence (n + 8k) % 8 = n % 8 by simp with Nat.add_mod, then applies simp to the main goal, reducing it to reflexivity.
why it matters in Recognition Science
The periodicity feeds the Recognition Theta certificate, which assembles additivity of the phi-rung, its vanishing at 1, and the bound |χ₈| ≤ 1. It supplies the concrete invariance needed for the eight-tick octave (T7) in the forcing chain, allowing modular reductions inside character sums without altering the Recognition Science mass ladder or Berry threshold. The result closes the modular-reduction step required by the Recognition Composition Law when arguments are shifted by multiples of the period-8 tick.
scope and limits
- Does not prove periodicity for any period other than multiples of 8.
- Does not extend χ₈ to negative integers or real arguments.
- Does not derive summation formulas or orthogonality relations for χ₈.
- Does not address the full wheel-840 filter beyond the mod-8 case.
formal statement (Lean)
40theorem chi8_periodic (n k : ℕ) : chi8 (n + 8 * k) = chi8 n := by
proof body
Tactic-mode proof.
41 -- `chi8` depends only on `n % 8`.
42 unfold chi8
43 have : (n + 8 * k) % 8 = n % 8 := by
44 simp [Nat.add_mod]
45 -- rewrite by the mod-8 equality and the result is definitional
46 simp [this]
47