cumulativeCooling_pos
plain-language theorem explainer
The theorem establishes that cumulative cooling after any positive integer number of cycles is strictly positive. Engineers certifying phantom-cavity refrigerators in the Recognition Science framework would cite it to confirm net thermal extraction. The proof is a one-line term that unfolds the definition and applies multiplication positivity to the cast of n > 0 together with the already-established positivity of the cooling fraction.
Claim. For every natural number $n$ with $ngeq 1$, the cumulative cooling satisfies $0 < ncdot f$, where $f$ is the positive cooling fraction per cycle expressed in units of $k_B T_{rm bath}$.
background
The Identity-Tick Refrigerator Spec module treats cumulative cooling after $n$ cycles as the product $ncdot f$, where $f$ is the cooling fraction derived from $J(phi)approx 0.118$. The local setting is the phantom-cavity refrigerator whose per-cycle cooling is $Q_{rm per cycle}=J(phi)cdot k_Bcdot T_{rm bath}$, with cumulative cooling therefore scaling linearly as $ncdot Q_{rm per cycle}$. The upstream theorem coolingFraction_pos supplies $0<f$ by unfolding the fraction definition and invoking $phi>1.5$ with linarith; the definition cumulativeCooling itself is the direct product $(n:mathbb{R})cdot f$.
proof idea
The term proof first unfolds cumulativeCooling to expose the product form. It then applies mul_pos to the cast (via exact_mod_cast) of the omega-derived fact $0<n$ together with the already-proved coolingFraction_pos.
why it matters
The result populates the cumulative_pos field inside the IdentityTickRefrigeratorCert structure, thereby completing the engineering certificate for the refrigerator specification. It directly supports the linear growth of total extracted energy with cycle count, consistent with the phi-ladder and eight-tick octave structure of the broader Recognition Science framework. The module falsifier requires any physical implementation to exhibit per-cycle cooling inside the interval $[J(phi)/2,2cdot J(phi)]cdot k_B T_{rm bath}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.