inverseTemperature
plain-language theorem explainer
The definition supplies the scaled inverse temperature E₀/T for use in J-cost Boltzmann weights within the thermodynamics bridge. Researchers deriving partition functions or free-energy minima from J-cost minimization would cite it when introducing the Lagrange multiplier. It arises by direct division of the reference energy by the positive temperature parameter.
Claim. The inverse temperature parameter is the scaled Lagrange multiplier defined by $E_0/T$ for $T>0$, enforcing the J-cost constraint in the Boltzmann weight $P(E)∝exp(-(E_0/T)J(E/E_0))$.
background
The J-Cost to Thermodynamics Bridge module connects Recognition Science's J-cost functional to thermodynamic distributions. J-cost is the derived cost J(x)=½(x+1/x)-1 on positive ratios, taken from the comparator in MultiplicativeRecognizerL4 and the recognition-event cost in ObserverForcing. Temperature enters as the Lagrange multiplier that minimizes average J-cost subject to ledger-balance constraints, with the eight-tick phase structure supplying the spin-statistics link to Fermi-Dirac and Bose-Einstein forms. Upstream, Breath1024 supplies the fundamental period T and QuantumLedger supplies the Born-rule probability.
proof idea
Direct definition that sets inverseTemperature E₀ T hT to the quotient E₀/T. No lemmas or tactics are invoked; the body is the elementary scaling of the inverse temperature by the reference energy.
why it matters
This definition supplies the Lagrange multiplier that converts J-cost minimization into the standard Boltzmann factor inside the thermodynamics bridge. It supports the module's core claim that exp(-βJ(E/E₀)) emerges from free-energy minimization and feeds the subsequent siblings that construct jcostBoltzmann and partitionFunction. It thereby closes the step from the Recognition Composition Law and eight-tick octave to thermodynamic equilibrium distributions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.