pith. machine review for the scientific record. sign in
theorem proved tactic proof high

chi8_eq_zero_iff_even

show as:
view Lean formalization →

The theorem states that the mod-8 character chi8 vanishes exactly on even natural numbers. Number theorists building wheel sieves or modular prime filters cite it to separate parity cases cleanly. The proof reduces the input to its remainder modulo 8, verifies the eight cases by interval_cases and decide, then chains equivalences through mod-2 reduction back to the Even predicate.

claim$chi_8(n) = 0$ if and only if $n$ is even, where $chi_8 : mathbb{N} to mathbb{Z}$ returns 0 on residues 0,2,4,6 mod 8, +1 on 1 and 7, and -1 on 3 and 5.

background

The module supplies modular-arithmetic primitives for wheel factorization, starting with soundness of the 840-wheel that excludes the primes 2, 3, 5 and 7. The character chi8 is introduced by direct case analysis on n mod 8 and is zero precisely when the residue is even. This theorem converts that definition into an equivalence with the standard Even predicate on naturals. Upstream material includes the chi8 definition itself together with foundational is theorems that guarantee the underlying algebraic identities hold without extra axioms.

proof idea

The tactic proof sets r := n % 8, proves chi8 n = chi8 r by simplification, then applies interval_cases to r (bounded by 8) and decides the eight cases to obtain chi8 r = 0 iff r % 2 = 0. It next invokes mod_mod_of_dvd to equate r % 2 with n % 2, rewrites the even condition via Nat.even_iff, and assembles the chain of equivalences.

why it matters in Recognition Science

The result is the direct parent of chi8_ne_zero_iff_odd, which negates the equivalence to characterize odd inputs. It supplies a basic parity gate inside the wheel-840 construction and aligns with the eight-tick octave (period 2^3) of the Recognition framework. No open scaffolding remains; the declaration is fully proved.

scope and limits

Lean usage

example (n : ℕ) (h : chi8 n = 0) : Even n := (chi8_eq_zero_iff_even n).mp h

formal statement (Lean)

  81theorem chi8_eq_zero_iff_even (n : ℕ) : chi8 n = 0 ↔ Even n := by

proof body

Tactic-mode proof.

  82  -- Reduce to the remainder `r = n % 8`, which is bounded (`r < 8`).
  83  set r := n % 8 with hr
  84  have hr_lt : r < 8 := by
  85    have : n % 8 < 8 := Nat.mod_lt n (by decide)
  86    simpa [hr] using this
  87  have hchi : chi8 n = chi8 r := by
  88    -- Both sides reduce to the same `match r with ...` form.
  89    simp [chi8, hr.symm, Nat.mod_eq_of_lt hr_lt]
  90  have hhelp : (chi8 r = 0 ↔ r % 2 = 0) := by
  91    interval_cases r <;> decide
  92  have hmod : r % 2 = n % 2 := by
  93    -- `r = n % 8`, and `2 ∣ 8`, so `(n % 8) % 2 = n % 2`.
  94    simpa [hr.symm] using (mod_mod_of_dvd n (by decide : 2 ∣ 8))
  95  calc
  96    chi8 n = 0 ↔ chi8 r = 0 := by
  97      constructor
  98      · intro hn0
  99        simpa [hchi.symm] using hn0
 100      · intro hr0
 101        simpa [hchi] using hr0
 102    _ ↔ r % 2 = 0 := hhelp
 103    _ ↔ n % 2 = 0 := by
 104      constructor
 105      · intro hr0
 106        simpa [hmod] using hr0
 107      · intro hn0
 108        simpa [hmod.symm] using hn0
 109    _ ↔ Even n := by
 110      simpa using (Nat.even_iff (n := n)).symm
 111
 112/-- `chi8 n ≠ 0` exactly when `n` is odd. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.