IndisputableMonolith.NumberTheory.Primes.Resonance
The Resonance module formalizes the Cicada Lemma: for prime p not dividing k, lcm(p,k) equals p*k and thereby maximizes the interval to first synchronization. Number theorists studying periodic prime encounters or Recognition Science contributors modeling resonance would cite the result. The module extends the imported Basic primes layer with resonance-specific definitions and lemmas while remaining axiom-free.
claimIf $p$ is prime and $p \nmid k$, then $\operatorname{lcm}(p,k)=p\cdot k$. This equality maximizes the time between encounters.
background
The module lives in NumberTheory.Primes.Resonance and imports Mathlib together with IndisputableMonolith.NumberTheory.Primes.Basic. The upstream Basic module supplies axiom-free sanity theorems that reuse Mathlib’s Nat.Prime and confirm correct wiring of the prime namespace. The Resonance module adds the Cicada Lemma together with sibling definitions cicada_safety_interval, safety_ratio and max_safety_ratio.
proof idea
This is a definition-and-lemma module; it contains no single overarching proof but assembles the Cicada Lemma and its immediate corollaries on top of the imported Basic results.
why it matters in Recognition Science
The module is imported by the parent Primes aggregator, which downstream code is instructed to prefer. It supplies the Cicada Lemma as the concrete number-theoretic content needed for resonance analysis inside the Recognition Science prime ladder.
scope and limits
- Does not treat the case where p divides k.
- Does not extend the statement to composite integers.
- Does not derive analytic estimates such as prime gaps.
- Does not link the lemma to physical constants or the phi ladder.