Carnot efficiency on the thermodynamic scale:
ProvedSecondLawThermo.carnot_efficiency_eq_one_sub_temp_ratioThroughout, is a type of empirical temperatures carrying a linear order ( means the reservoir at is colder than the one at ), and a cycle is a finitely supported function : for each reservoir temperature , the number is the net heat absorbed by the device from the reservoir at in one complete cycle (negative when heat is rejected to it), and only finitely many reservoirs are touched. The work delivered in the cycle is
which is the first law for a device returning to its initial state. A set of cycles stands for the physically realizable ones; it is assumed to be a convex cone: , (run two devices side by side), and for (scale a device). A cycle is reversible when and . A cycle operates between and when for every . A Carnot engine between a hot reservoir and a cold reservoir is a reversible cycle operating between and with , and . The efficiency relative to the hot reservoir is .
Statement. Let be a scale for which every Carnot engine between reservoirs satisfies . Then every such Carnot engine has efficiency
This combines equation (1) with the definition of the thermodynamic temperature scale: on that scale the efficiency of a reversible engine depends on the two reservoirs only through the ratio of their thermodynamic temperatures.
import Definitions.Def_SecondLawThermo_Defs import Mathlib
namespace SecondLawThermo
theorem carnot_efficiency_eq_one_sub_temp_ratio {Θ : Type*} [LinearOrder Θ] (𝒞 : Set (Cycle Θ))
(T : Θ → ℝ)
(hT : ∀ (h k : Θ) (e : Cycle Θ), k < h → IsCarnotEngine 𝒞 e h k →
|e k| / |e h| = T k / T h)
(h k : Θ) (hkh : k < h) (e : Cycle Θ) (he : IsCarnotEngine 𝒞 e h k) :
efficiency e h = 1 - T k / T h := by sorry
end SecondLawThermoRead-back
What the Lean code literally says, in plain math · Aristotle (Harmonic), the drafting agent itself; non-blind read-back
Disclosure: this read-back is NOT blind. It was written by the same agent (Aristotle, by Harmonic) that drafted these Lean statements, with full knowledge of the source text and of the intended meaning. It is therefore not independent testimony and must not be mistaken for an independent audit. Reviewers should check the Lean code against the source themselves.
Let be a linearly ordered type, an arbitrary set of finitely supported functions , and an arbitrary real-valued function. Assume that for all and every such that , , vanishes outside , , and , one has . Then, for any such and any such ,
The hypothesis on is assumed, not derived, and no positivity of is assumed: if the quotient is the Lean junk value on both sides of the assumed identity, and the conclusion still holds under that reading. No property of such as being a cone is used.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.