max_safety_ratio
plain-language theorem explainer
For a prime p and positive integer k not divisible by p, the safety ratio lcm(p,k)/k equals p. Researchers modeling cyclic resonance or avoidance strategies in periodic systems would cite this to confirm the maximal separation window. The proof reduces the ratio directly via the cicada safety interval lemma then cancels over the rationals.
Claim. Let $p$ be prime and $k$ a positive integer with $p$ not dividing $k$. Then $lcm(p,k)/k = p$.
background
The Resonance module formalizes the Cicada Principle: prime periods minimize intersections with predator cycles of length k by maximizing the least common multiple. The safety ratio is defined as lcm(p,k) divided by k. The cicada safety interval theorem states that when p is prime and does not divide k, lcm(p,k) equals p times k, which follows from coprimality and the identity gcd times lcm equals the product.
proof idea
The term proof rewrites safety ratio by its definition and applies the cicada safety interval lemma to substitute lcm(p,k) with p times k. It then casts k to rationals, commutes the product, and cancels via field simplification after confirming the denominator is nonzero.
why it matters
This result establishes the upper bound on the safety ratio under coprimality, directly supporting the structural advantage of primes in the Cicada Principle. It closes the local argument in the Resonance module for maximal alignment avoidance. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.