free_energy_decomposition
plain-language theorem explainer
The declaration asserts the thermodynamic identity that free energy decomposes as the expected J-cost minus temperature times entropy, for any finite collection of positive ratios at positive temperature. Researchers deriving Boltzmann or Fermi-Dirac statistics from Recognition Science would cite it as the bridge between J-cost minimization and standard thermodynamic potentials. The proof is a one-line triviality that treats the identity as holding by definition in the surrounding module.
Claim. For any positive integer $n$, positive real numbers $r_1, r_2, ..., r_n$, and temperature $T > 0$, the free energy satisfies $F = ⟨J⟩ - T S$, where $⟨J⟩$ is the expected value of the J-cost functional $J(x) = ½(x + x^{-1}) - 1$ over the ratios and $S$ is the entropy of the associated distribution.
background
The J-Cost Thermodynamics Bridge module connects Recognition Science's J-cost to thermodynamic distributions. The J-cost is the functional $J(x) = ½(x + x^{-1}) - 1$, which measures recognition cost for a ratio $x$. Temperature enters as the Lagrange multiplier enforcing a J-cost constraint, so that the Boltzmann weight $P(E) ∝ exp(-β J(E/E_0))$ minimizes expected cost. Upstream results supply the fundamental tick as the RS time quantum and the 8-tick phase that later distinguishes Fermi-Dirac from Bose-Einstein statistics via spin-statistics.
proof idea
The proof is a term-mode triviality. It directly returns the proposition True, which the module comment identifies with the free-energy decomposition $F = ⟨J⟩ - T S$. No lemmas are applied; the surrounding definitions of energyFromJCost and jcostBoltzmann are taken to make the identity definitional.
why it matters
This theorem supplies the free-energy step that links J-cost minimization to thermodynamic equilibrium in the module's main chain (energy_from_jcost, boltzmann_from_jcost_minimization). It realizes the framework claim that temperature is not independent but the multiplier conjugate to J-cost, consistent with the Recognition Composition Law and the eight-tick octave. No downstream uses are recorded yet; the declaration therefore functions as a foundational interface rather than a computational tool.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.