thermal_equilibrium
plain-language theorem explainer
This theorem states that the recognition cost vanishes at unit scale, encoding thermal equilibrium as uniform recognition with no temperature gradient. Physicists deriving thermodynamics from the Recognition Science functional equation cite it as the formal statement of the zeroth law. The proof is a direct one-line application of the base unit-cost lemma.
Claim. The recognition cost satisfies $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$ expresses the squared-ratio cost of a scale factor.
background
In Recognition Science the J-cost function quantifies recognition cost of a scale factor x via the explicit form J(x) = (x-1)^2/(2x). Thermal equilibrium is identified with the case of uniform temperature, which maps exactly to zero recognition cost. The module ThermalPhysicsFromRS derives five canonical heat-transfer mechanisms from the configuration dimension D = 5 and treats J = 0 as the equilibrium condition.
proof idea
This is a one-line wrapper that applies the Jcost_unit0 lemma, which itself reduces J(1) = 0 by direct simplification of the cost expression.
why it matters
The result supplies the equilibrium field for both the thermalPhysicsCert definition and the thermodynamicCert definition. It formalizes the zeroth law inside the RS derivation of thermodynamics, where J = 0 marks the absence of any recognition cost. Downstream certificates use it to close the statement that thermal equilibrium holds under the core RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.