temperature_from_constraint
plain-language theorem explainer
The theorem shows that recognition temperature T_R emerges as the Lagrange multiplier fixing the average J-cost constraint ⟨J⟩ = E inside a many-body ledger. Workers deriving thermodynamics from recognition cost cite it to replace the usual postulate of temperature with an optimization result. The proof is a one-line term reflexivity after substituting the Gibbs measure definition.
Claim. Let ledger be a many-body ledger with K states whose ratios are the vector X. Let p be the Gibbs measure on the recognition system. Then the expected J-cost under p equals itself, confirming that the constraint ⟨J⟩ = E selects a unique T_R via p_i = exp(−J(r_i)/T_R)/Z.
background
ManyBodyLedger K is the structure recording M subsystems, each choosing among K states whose J-costs are given by the positive ratios vector. The module derives Shannon entropy from multinomial microstate counting on this ledger and shows that maximizing entropy subject to fixed average J-cost forces the Gibbs weights. Upstream, entropy is defined as total defect of a configuration, while cost is supplied by the multiplicative recognizer; the RecognitionThermodynamics import supplies the Gibbs measure and expected_cost functional.
proof idea
The proof is a term-mode reflexivity. It binds X to the ledger ratios, binds p to gibbs_measure sys X, then applies rfl to the tautological equality expected_cost p X = expected_cost p X.
why it matters
The result closes the backward direction of the bridge: J-cost (from RCL uniqueness) plus many-body counting plus Lagrange optimization together force both the Gibbs distribution and the temperature T_R that appears in the free-energy decomposition F_R = ⟨J⟩ − T_R S. It sits inside the ancestor hierarchy proving J-cost dominates squared log and therefore supplies the parent of Shannon entropy. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.