SystemStability

formal source

  35
  36/-- **DEFINITION: System Stability (S_sys)**
  37    Stability is higher when geometric strain is lower. -/
  38noncomputable def SystemStability (r : ℝ) : ℝ :=
  39    1 / (1 + GeometricStrain r)
  40
  41/-- **THEOREM: Resonant Minimization**
  42    Resonant scales minimize the geometric strain.
  43    If r is a power of φ, its strain is zero. -/
  44theorem resonant_minimization (r : ℝ) (hr : r > 0) :
  45    ResonantScale r → GeometricStrain r = 0 := by
  46  intro h
  47  unfold ResonantScale at h
  48  rcases h with ⟨n, rfl⟩
  49  unfold GeometricStrain
  50  simp only [hr, ↓reduceDIte]
  51  -- We need to show that floor(log(phi^n)/log(phi) + 1/2) = n
  52  have h_val : Real.log (phi ^ (n : ℝ)) / Real.log phi = n := by
  53    rw [Real.log_rpow phi_pos]
  54    have h_log_phi_pos : 0 < Real.log phi := Real.log_pos one_lt_phi
  55    field_simp [h_log_phi_pos.ne']
  56  rw [h_val]
  57  -- floor(n + 1/2) = n for integer n
  58  have h_floor : Int.floor ((n : ℝ) + 1 / 2) = n := by
  59    apply Int.floor_eq_iff.mpr
  60    constructor
  61    · linarith
  62    · linarith
  63  rw [h_floor]
  64  simp only [div_self (Real.rpow_pos_of_pos phi_pos _).ne', Jcost_unit0]
  65
  66/-- **THEOREM: Coherence Increases System Stability**
  67    Using resonant scales increases the overall stability of the biological system. -/
  68theorem resonance_increases_stability (r_init r_resonant : ℝ) (hr_init : r_init > 0) (hr_res : r_resonant > 0) :