pith. sign in
module module high

IndisputableMonolith.NumberTheory.Primes.Resonance

show as:
view Lean formalization →

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

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)