cumulativeCooling_strict_mono
plain-language theorem explainer
Engineers verifying the phantom-cavity refrigerator model cite this result to confirm that total extracted energy increases strictly with each additional cycle. It states that for natural numbers n less than m the product of n and the cooling fraction is less than the product of m and the same fraction. The short tactic proof unfolds the scaling definition, casts the inequality to the reals, and applies the right-multiplication lemma under positivity of the fraction.
Claim. Let $c > 0$ denote the cooling fraction. For natural numbers $n, m$ with $n < m$, the inequality $n c < m c$ holds in the reals.
background
The Identity-Tick Refrigerator Spec defines cumulative cooling after n cycles as the product of the cycle count and the cooling fraction, the latter being the per-cycle extraction J(φ) expressed in units of k_B T_bath. The upstream theorem coolingFraction_pos establishes positivity of this fraction by reduction to phi greater than 1.5. The module places the construction in the engineering derivation track, where repeated application of the J-cost yields additive cooling.
proof idea
The tactic proof unfolds the definition of cumulative cooling to expose multiplication by the cooling fraction. It casts the hypothesis n < m from naturals to reals via exact_mod_cast. It then applies the lemma mul_lt_mul_iff_of_pos_right instantiated with the positivity result coolingFraction_pos.
why it matters
The theorem supplies the strict monotonicity clause required by refrigerator_one_statement and by the bundled certificate identityTickRefrigeratorCert. It thereby completes the one-statement engineering summary for the refrigerator spec inside the Recognition Science framework. The result aligns with the additive structure expected from the J-cost functional and the phi-ladder scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.