pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.NumberTheory.Primes

show as:
view Lean formalization →

The NumberTheory.Primes module assembles prime-number interfaces for the Recognition Science monolith by importing nine submodules on basics, factorization, Möbius functions, modular wheels, and resonance. Researchers extending the framework to arithmetic or cycle phenomena would cite these stable wrappers. The module contains no central theorem but organizes axiom-free lemmas and definitions over Mathlib.

claimThe module defines the prime exponent function $v_p(n)$, the Möbius function $μ(n)$, wheel coprimality conditions modulo 840, and resonance properties for prime periods in cycle dynamics.

background

The NumberTheory.Primes module acts as the organizational hub for prime-related work in the Recognition Science monolith. It imports submodules that establish basic prime footholds, factorization interfaces, and related algebraic tools while remaining axiom-free and sorry-free. The theoretical setting reuses Mathlib's Nat.Prime without new axioms, providing small sanity theorems to confirm correct wiring before analytic layers are added.

proof idea

This is a definition module with no proofs. It structures the development as a sequence of imported submodules that build from algebraic foundations (Basic, GCDLCM, Factorization) to modular utilities, arithmetic functions including the Möbius wrapper, squarefree properties, and finally resonance dynamics.

why it matters in Recognition Science

The module supplies number-theoretic primitives that support higher-level constructions in the Recognition Science framework, such as constants on the phi-ladder and resonance in cycle dynamics. It aligns with the eight-tick octave and prepares for extensions once the algebraic layer stabilizes. No specific downstream theorems are listed in the used-by edges.

scope and limits

depends on (9)

Lean names referenced from this declaration's body.