module module high

`IndisputableMonolith.NumberTheory.Primes.RSConstants`

This module assembles the small primes and factorizations central to Recognition Science constants, notably deriving the beat numerator 37 from the difference 45 minus 8. Researchers working on prime-based modular filters or RS mass formulas would import it for the explicit values of 5, 11, 17, 37, 103, and 137. The module structure is a set of direct definitions and equality checks that verify the arithmetic identities without deeper proofs.

claimThe module defines the primes $5, 11, 17, 37, 103, 137$ and the identities $8 = 2^3$, $45 = 3^2 · 5$, gcd$(8,45) = 1$, lcm$(8,45) = 360$, along with the prime factorizations of 360 and the wheel 840.

background

This module sits in the NumberTheory.Primes namespace, importing Basic for reuse of Mathlib's Nat.Prime and Factorization for the vp exponent interface. The doc comment highlights that the RS beat numerator arises as 45 - 8 = 37. Upstream, Basic provides axiom-free sanity theorems on primes, while Factorization supplies algebraic laws like vp_mul for building squarefree and Möbius functions downstream.

proof idea

This is a definition module with no proofs. It declares the prime constants and states the factorization equalities directly, relying on Mathlib's built-in arithmetic for verification.

why it matters in Recognition Science

The module supplies the explicit prime values and relations that feed the Primes aggregator and the Modular module for wheel filters. It instantiates the RS beat numerator 37 and the alpha-related prime 137, supporting the framework's constants in the phi-ladder and the eight-tick structure. Downstream code uses these for modular soundness proofs in prime-friendly arithmetic.

scope and limits

Does not contain analytic number theory results.
Does not prove primality of numbers beyond the listed small primes.
Does not define general functions over these constants.
Does not address the full RS forcing chain or mass formulas.

used by (2)

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

IndisputableMonolith.NumberTheory.Primes module_import
IndisputableMonolith.NumberTheory.Primes.Modular module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.NumberTheory.Primes.Basic module_import
IndisputableMonolith.NumberTheory.Primes.Factorization module_import

declarations in this module (47)

theorem prime_five L22
theorem prime_eleven L25
theorem prime_seventeen L28
theorem prime_thirtyseven L31
theorem prime_onehundredthree L34
theorem prime_onehundredthirtyseven L37
theorem eight_eq_two_pow_three L42
theorem fortyfive_eq_three_sq_mul_five L45
theorem gcd_eight_fortyfive_eq_one L48
theorem lcm_eight_fortyfive_eq_360 L51
theorem threehundredsixty_factorization L54
theorem wheel840_factorization L57
theorem one_div_eight_sub_one_div_fortyfive L62
theorem aliasing_ratio L66
theorem fortyfive_sub_eight_eq_thirtyseven L72
theorem coprime_eight_fortyfive L76
theorem vp_eight_two L82
theorem vp_eight_three L83
theorem vp_eight_five L84
theorem vp_fortyfive_two L87
theorem vp_fortyfive_three L88
theorem vp_fortyfive_five L89
theorem vp_360_two L92
theorem vp_360_three L93
theorem vp_360_five L94
theorem vp_360_seven L95
theorem vp_840_two L98
theorem vp_840_three L99
theorem vp_840_five L100
theorem vp_840_seven L101
theorem lcm_eight_fortyfive_vp_characterization L104
theorem coprime_eight_fortyfive_vp L113
theorem prime_beat_numerator L118
theorem coprime_thirtyseven_360 L121
theorem prime_thirteen L126
theorem prime_seven L129
theorem not_squarefree_fortyfive L133
theorem not_squarefree_360 L139
theorem not_squarefree_eight L145
theorem not_squarefree_840 L151
theorem radical_360 L157
theorem radical_eight L160
theorem radical_fortyfive L163
theorem eight_dvd_360 L168
theorem fortyfive_dvd_360 L171
theorem threehundredsixty_div_eight L174
theorem threehundredsixty_div_fortyfive L177