criticalBand_not_overloaded

formal source

 106  rw [div_lt_one hB] at hlt
 107  simpa using hlt
 108
 109theorem criticalBand_not_overloaded
 110    {rhoMin area demand : ℝ} (hArea : 0 < area)
 111    (h : InCriticalBand rhoMin area demand) :
 112    ¬ IsOverloaded area demand := by
 113  unfold IsOverloaded
 114  have hSub : demand < bandwidth area := by
 115    simpa [IsSubcritical] using criticalBand_implies_subcritical hArea h
 116  exact not_le_of_gt hSub
 117
 118/-! ## §3. Semantic free energy and condensation gate -/
 119
 120/-- Query-level semantic free energy. -/
 121def semanticFreeEnergy
 122    (refCost entropy attention berryWeight berry : ℝ) : ℝ :=
 123  refCost - attention * entropy - berryWeight * berry
 124
 125theorem higher_entropy_lowers_freeEnergy
 126    {refCost attention berryWeight berry entropy₁ entropy₂ : ℝ}
 127    (hAttention : 0 ≤ attention) (hEntropy : entropy₁ ≤ entropy₂) :
 128    semanticFreeEnergy refCost entropy₂ attention berryWeight berry ≤
 129      semanticFreeEnergy refCost entropy₁ attention berryWeight berry := by
 130  have hMul : attention * entropy₁ ≤ attention * entropy₂ :=
 131    mul_le_mul_of_nonneg_left hEntropy hAttention
 132  unfold semanticFreeEnergy
 133  linarith
 134
 135theorem higher_berry_lowers_freeEnergy
 136    {refCost entropy attention berryWeight berry₁ berry₂ : ℝ}
 137    (hWeight : 0 ≤ berryWeight) (hBerry : berry₁ ≤ berry₂) :
 138    semanticFreeEnergy refCost entropy attention berryWeight berry₂ ≤
 139      semanticFreeEnergy refCost entropy attention berryWeight berry₁ := by