cicada_safety_interval
plain-language theorem explainer
The Cicada Lemma states that if p is prime and does not divide k then lcm(p, k) equals p times k. Modelers of periodic biological cycles or resonance in number theory cite this result to bound synchronization intervals. The proof derives coprimeness from the prime hypothesis and substitutes into the standard gcd-lcm product identity.
Claim. Let $p$ be a prime and let $k$ be a natural number not divisible by $p$. Then the least common multiple of $p$ and $k$ equals the product $p k$.
background
The module formalizes resonance phenomena where primes minimize alignment frequency with other cycles. The Cicada Principle notes that periodical cicadas use prime periods to maximize time between encounters with predators of cycle k. Upstream, the result relies on the identity that gcd times lcm equals the product of the arguments, together with the characterization that a prime is coprime to k precisely when it does not divide k.
proof idea
The proof first invokes the prime coprimeness criterion to obtain gcd(p, k) = 1. It then applies the gcd-lcm product identity and rewrites using the fact that one times any number equals that number to conclude the lcm equals the product.
why it matters
This lemma supplies the key algebraic step for the max_safety_ratio theorem, which shows that the safety ratio reaches its maximum value p precisely under these conditions. It instantiates the Cicada Principle within the Recognition framework, where prime periods maximize the safety window in cycle dynamics. The result closes a basic case in the resonance module without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.