pith. sign in
module module moderate

IndisputableMonolith.NumberTheory.Primes

show as:
view Lean formalization →

The NumberTheory.Primes module aggregates nine submodules to supply stable, axiom-free prime interfaces for the Recognition Science monolith. It covers basic primes, factorization with valuations, GCD/LCM, modular wheels, Möbius functions, squarefree checks, and resonance including the Cicada Principle. Number theorists building on the framework cite these wrappers for consistent algebraic access. The module itself contains no proofs and functions only as an import organizer.

claimThe module collects interfaces for the Möbius function $μ(n)$, the prime valuation $v_p(n)$, wheel coprimality to 840, and resonance properties of prime cycles such as 13 and 17.

background

This module occupies the NumberTheory domain and imports Basic, RSConstants, GCDLCM, Wrappers, Modular, Factorization, Squarefree, ArithmeticFunctions, and Resonance. Basic reuses Mathlib's Nat.Prime while remaining axiom-free and sorry-free. Factorization defines the repo-local vp with laws such as vp_mul and vp_pow. GCDLCM exposes stable gcd/lcm wrappers. Modular formalizes soundness of wheel filters. ArithmeticFunctions wraps the Möbius function μ. Resonance formalizes the Cicada Principle for prime periods that minimize alignment conflicts.

proof idea

This is a definition module with no proofs; it structures the primes namespace solely by importing the nine listed submodules.

why it matters in Recognition Science

The module supplies the algebraic prime layer that supports higher Recognition Science constructions, including resonance phenomena tied to the eight-tick octave and phi-ladder. It has no listed downstream uses in the current graph but forms the base for any prime-dependent results in the monolith.

scope and limits

depends on (9)

Lean names referenced from this declaration's body.