cumulativeCooling_pos
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.
claimFor 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 in Recognition Science
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}$.
scope and limits
- Does not compute a numerical value for the cooling fraction itself.
- Does not incorporate external heat leaks or non-ideal cycle inefficiencies.
- Does not address non-integer or continuous-time cycle counts.
formal statement (Lean)
55theorem cumulativeCooling_pos {n : ℕ} (h : 1 ≤ n) :
56 0 < cumulativeCooling n := by
proof body
Term-mode proof.
57 unfold cumulativeCooling
58 exact mul_pos (by exact_mod_cast (by omega : 0 < n)) coolingFraction_pos
59