IndisputableMonolith.NumberTheory.Primes.Resonance

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.Primes.Basic
   3
   4/-!
   5# Resonance and Cycle Dynamics
   6
   7This module formalizes the "Cicada Principle" and other resonance phenomena
   8where primes play a structural role in minimizing or maximizing alignment.
   9
  10## The Cicada Principle
  11
  12Periodical cicadas (Magicicada) appear in 13- and 17-year cycles. These are prime numbers.
  13This strategy minimizes the frequency of intersection with predator lifecycles.
  14
  15If a predator has a cycle `k`, it meets the cicada every `lcm(p, k)` years.
  16If `p` is prime and `¬ p ∣ k`, then `lcm(p, k) = p * k`.
  17This maximizes the "safety window" compared to composite cycles.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace NumberTheory
  22namespace Primes
  23
  24open Nat
  25
  26/-- **The Cicada Lemma**:
  27    If `p` is prime and does not divide `k`, then their first synchronization
  28    (LCM) occurs at exactly `p * k`.
  29
  30    This maximizes the time between encounters. -/
  31theorem cicada_safety_interval (p k : ℕ) (hp : Prime p) (h_ndvd : ¬ p ∣ k) :
  32    Nat.lcm p k = p * k := by
  33  -- Since p is prime and does not divide k, gcd(p, k) must be 1.
  34  have h_coprime : Nat.Coprime p k := (Nat.Prime.coprime_iff_not_dvd hp).mpr h_ndvd
  35  have h_gcd : Nat.gcd p k = 1 := h_coprime
  36  -- Use gcd * lcm = a * b
  37  have h_mul := Nat.gcd_mul_lcm p k
  38  rw [h_gcd, one_mul] at h_mul
  39  exact h_mul
  40
  41/-- The "safety ratio" is maximized when cycles are coprime.
  42    Safety ratio = LCM(p, k) / k = p (the max possible value). -/
  43def safety_ratio (p k : ℕ) : ℚ := (Nat.lcm p k : ℚ) / (k : ℚ)
  44
  45theorem max_safety_ratio (p k : ℕ) (hp : Prime p) (hk : k > 0) (h_ndvd : ¬ p ∣ k) :
  46    safety_ratio p k = p := by
  47  rw [safety_ratio, cicada_safety_interval p k hp h_ndvd]
  48  have hk_q_pos : (k : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.ne_of_gt hk)
  49  rw [mul_comm p k]
  50  simp only [Nat.cast_mul]
  51  field_simp [hk_q_pos]
  52
  53end Primes
  54end NumberTheory
  55end IndisputableMonolith
  56