module module high

`IndisputableMonolith.NumberTheory.Primes.Modular`

This module defines the wheel modulus 840 and modular functions such as chi8 variants for prime sieves in Recognition Science. Number theorists working on modular constraints or RS constants would cite it when bridging algebraic primes to later analytic steps. The module is a collection of definitions and basic arithmetic facts with no proof bodies.

claimThe wheel modulus is $840 = 2^3 imes 3 imes 5 imes 7$. Associated objects include the function $\\_8$ (periodic with period 8) and its restrictions modulo 0 through 7, together with the equivalence $\\chi_8(n) = 0 \iff n$ even.

background

The module belongs to the NumberTheory.Primes namespace and imports Mathlib, Basic, and RSConstants. Basic supplies axiom-free footholds that reuse Nat.Prime and provide small sanity theorems. RSConstants collects decidable arithmetic facts about repeated integers including 840, 8, 45, 360 and prime markers such as 11, 17, 37, 103, 137. The DOC_COMMENT identifies the wheel modulus 840 as the central object.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module is imported by the parent Primes aggregator, which states that downstream code should prefer importing this module rather than individual files. It supplies the wheel modulus 840 as a stable anchor that keeps later bridge lemmas readable and avoids re-proving the same arithmetic repeatedly.

scope and limits

Does not contain any theorems or sorry statements.
Does not extend into analytic number theory.
Does not introduce new axioms or hidden hypotheses.
Does not redefine Nat.Prime from Mathlib.

used by (1)

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

IndisputableMonolith.NumberTheory.Primes module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.NumberTheory.Primes.Basic module_import
IndisputableMonolith.NumberTheory.Primes.RSConstants module_import

declarations in this module (17)

def wheel840 L22
def chi8 L33
theorem chi8_periodic L40
theorem chi8_mod0 L48
theorem chi8_mod1 L52
theorem chi8_mod2 L56
theorem chi8_mod3 L60
theorem chi8_mod4 L64
theorem chi8_mod5 L68
theorem chi8_mod6 L72
theorem chi8_mod7 L76
theorem chi8_eq_zero_iff_even L81
theorem chi8_ne_zero_iff_odd L113
theorem wheel840_accepts L118
theorem prime_dvd_wheel840 L133
theorem wheel840_rejects L157
theorem wheel840_rejects_of_gcd_ne_one L181