module module high

`IndisputableMonolith.NumberTheory.Primes.Modular`

Modular prime theory module establishes the wheel modulus 840 as 2 cubed times 3 times 5 times 7 for handling periodic chi functions. It supports downstream prime analysis in Recognition Science by providing modular arithmetic primitives. Researchers studying prime distributions or RS constants would reference these definitions. The module contains direct definitions of wheel840 and chi8 variants with their periodicity properties.

claimThe wheel modulus is $840 = 2^3 3 5 7$, with associated functions $chi_8$ that are periodic with period 8 and satisfy $chi_8(n) = 0$ precisely when $n$ is even.

background

Upstream the Basic module supplies axiom-free prime footholds that reuse Mathlib's Nat.Prime without reinventing definitions. The RSConstants module anchors decidable arithmetic facts about integers including 840 and prime markers such as 11, 17, 37, 103, 137. This module sits inside the NumberTheory.Primes namespace to organize modular tools for the reality repo.

proof idea

This is a definition module, no proofs. It declares wheel840 as the explicit product 8 times 105 and introduces the family of chi8 functions together with their periodicity and zero conditions via direct computation.

why it matters in Recognition Science

This module feeds the parent IndisputableMonolith.NumberTheory.Primes aggregator, whose doc-comment states to prefer importing the full namespace from downstream code. It supplies the modular arithmetic layer needed for prime facts in RS and anchors the repeated use of 840 as a stable constant from RSConstants.

scope and limits

Does not prove any primality theorems.
Does not introduce conditional hypotheses.
Does not extend beyond modular arithmetic.
Does not depend on external axioms or sorrys.

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