safety_ratio
plain-language theorem explainer
safety_ratio computes the ratio of the least common multiple of natural numbers p and k to k. Researchers analyzing periodic resonance and cycle alignment, such as in the cicada principle, cite this definition to quantify the effective extension of intersection periods. It is introduced as a direct abbreviation that converts the LCM operation into a rational number.
Claim. For natural numbers $p$ and $k$, define the safety ratio by $safety_ratio(p,k) := lcm(p,k)/k$.
background
The module Resonance and Cycle Dynamics formalizes resonance phenomena in which primes minimize the frequency of intersections between cycles. The cicada principle illustrates the point: a prime period p and a predator cycle k intersect every lcm(p,k) years, and the safety ratio measures how much this interval is stretched relative to k. When p is prime and does not divide k the ratio reaches its largest value p, which is the content of the downstream theorem that applies this definition.
proof idea
One-line definition that directly casts the least common multiple into the rationals and divides by k.
why it matters
The definition supplies the quantity whose maximum value is established by the theorem max_safety_ratio. That theorem shows safety_ratio p k equals p precisely when p is prime, k is positive, and p does not divide k, thereby confirming the structural advantage of prime periods in the resonance setting described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.