GeometricStrain

formal source

  25
  26/-- **DEFINITION: Geometric Strain (Q_geom)**
  27    The strain of a scale r relative to its nearest resonant neighbor. -/
  28noncomputable def GeometricStrain (r : ℝ) : ℝ :=
  29    if h : r > 0 then
  30      -- Use floor(log_phi(r) + 1/2) as a proxy for the nearest integer rung
  31      let n := Int.floor (Real.log r / Real.log phi + 1/2)
  32      Jcost (r / (phi ^ (n : ℝ)))
  33    else
  34      1.0 -- Arbitrary positive value for non-positive scales
  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