theorem
proved
criticalBand_implies_subcritical
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Unification.CriticalRecognitionLoading on GitHub at line 98.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
95 unfold loadRatio
96 exact div_pos hDemand (bandwidth_pos hArea)
97
98theorem criticalBand_implies_subcritical
99 {rhoMin area demand : ℝ} (hArea : 0 < area)
100 (h : InCriticalBand rhoMin area demand) :
101 IsSubcritical area demand := by
102 rcases h with ⟨_, hlt⟩
103 unfold IsSubcritical
104 unfold loadRatio at hlt
105 have hB : 0 < bandwidth area := bandwidth_pos hArea
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 ≤