semanticFreeEnergy

formal source

 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
 140  have hMul : berryWeight * berry₁ ≤ berryWeight * berry₂ :=
 141    mul_le_mul_of_nonneg_left hBerry hWeight
 142  unfold semanticFreeEnergy
 143  linarith
 144
 145/-- Query-level semantic admissibility region. -/
 146def SemanticCondensationGate
 147    (entropy entropyFloor attention signature signatureMin signatureMax z : ℝ) : Prop :=
 148  entropyFloor < entropy ∧
 149    signatureMin ≤ signature ∧
 150    signature ≤ signatureMax ∧
 151    attention ≤ phi ^ (3 : ℕ) ∧