chi8_periodic
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.