IndisputableMonolith.NumberTheory.Primes.Resonance
The Resonance module formalizes the Cicada Lemma on prime synchronization via LCM, asserting that for prime p not dividing k the first encounter occurs at exactly p*k. Number theorists studying periodic resonances or cicada-like cycles in the Recognition framework would cite it. The module supplies supporting definitions for safety intervals and ratios on top of the axiom-free Basic primes layer.
claimIf $p$ is prime and $p$ does not divide $k$, then $p$ and $k$ first synchronize at LCM$(p,k)=p k$, maximizing the interval between encounters.
background
The module lives in the NumberTheory.Primes namespace and imports the Basic module, whose design goals are to reuse Mathlib's Nat.Prime, remain axiom-free and sorry-free, and supply small sanity theorems before any analytic extensions. The Cicada Lemma is the central object, framed as maximizing time between encounters for a prime and a non-multiple integer. Sibling definitions cicada_safety_interval, safety_ratio and max_safety_ratio supply the concrete resonance machinery.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module feeds the parent Primes aggregator, which downstream code is instructed to import in preference to individual files. It supplies the resonance and synchronization layer that the prime-number namespace requires for later use in the Recognition Science monolith.
scope and limits
- Does not reinvent Mathlib prime predicates.
- Does not contain axioms or sorry statements.
- Does not extend into analytic number theory.
- Does not address composite synchronization cases.