third_law
plain-language theorem explainer
The third law asserts that J-cost vanishes in the limit as the recognition ratio approaches its ground-state value of one. Researchers deriving thermodynamics from recognition primitives cite this when establishing the zero-temperature limit from the J-functional. The term proof rewrites the target using the unit lemma for Jcost then applies continuity at that point.
Claim. $J(r) = (r-1)^2/(2r)$ satisfies $J(r) → 0$ as $r → 1$, where $r$ is a positive ratio and $J$ is the J-cost functional.
background
In Recognition Science the J-cost functional is defined by $J(r) = (r-1)^2/(2r)$ and vanishes exactly at the ground-state ratio $r=1$, as recorded in the upstream lemma Jcost_unit0. The module ThermodynamicLawsFromJCost derives the four thermodynamic laws from properties of this single functional, with the third law corresponding to the zero-temperature limit. The module documentation states that the third law encodes $T → 0$ implies $J → 0$ (ground state as $T → 0$).
proof idea
This is a term-mode proof consisting of one rewrite followed by an exact application. It replaces the target value 0 with Jcost 1 via the symmetric form of the unit lemma Jcost_unit0, then invokes the continuousAt property of Jcost_continuous at the point 1.
why it matters
The theorem supplies the third_law field of the ThermodynamicLawsCert structure that certifies all four thermodynamic laws follow from the J-cost functional. It closes the zero-temperature limit in the structural derivation and aligns with the ground-state condition in the forcing chain where J-uniqueness forces the minimum at the identity ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.