higher_entropy_lowers_freeEnergy
plain-language theorem explainer
Higher entropy reduces semantic free energy when attention is non-negative. Researchers analyzing stability in recognition bandwidth control would cite this monotonicity property. The proof is a direct algebraic reduction: multiply the entropy inequality by non-negative attention, unfold the free-energy definition, and close with linear arithmetic.
Claim. Let $refCost, attention, berryWeight, berry, entropy_1, entropy_2$ be real numbers with $attention ≥ 0$ and $entropy_1 ≤ entropy_2$. Then $semanticFreeEnergy(refCost, entropy_2, attention, berryWeight, berry) ≤ semanticFreeEnergy(refCost, entropy_1, attention, berryWeight, berry)$, where $semanticFreeEnergy(refCost, entropy, attention, berryWeight, berry) := refCost - attention · entropy - berryWeight · berry$.
background
The module sketches control theorems for the load ratio rho = R_dem / R_max inside recognition bandwidth systems. Operation stays inside the sub-saturation interval rho_min < rho < 1, with the actuator on the native 8-tick cadence and stability judged over the 360-tick supervisory horizon. Semantic free energy is the query-level cost function refCost minus attention times entropy minus berryWeight times berry.
proof idea
Apply mul_le_mul_of_nonneg_left to the entropy inequality and the hypothesis attention ≥ 0, obtaining attention · entropy_1 ≤ attention · entropy_2. Unfold the definition of semanticFreeEnergy and invoke linarith to finish the comparison.
why it matters
The result supplies a basic monotonicity fact for the semantic free energy function used in the module's control sketch. It shows that entropy growth (for example from increased recognition activity) lowers the cost, consistent with condensation-gate ideas in the unification setting. No downstream theorems yet reference it, so its role in fuller runtime or physics deployment statements remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.