cumulativeCooling_zero
The theorem establishes that cumulative cooling after zero cycles equals zero in the identity-tick refrigerator model. Engineers verifying phantom-cavity cooling systems cite this base case when building the full certification record. The proof is a one-line wrapper that unfolds the definition of cumulativeCooling and simplifies the resulting product.
claimLet $C(n)$ be the cumulative cooling after $n$ cycles measured in units of $k_B T_bath$. Then $C(0) = 0$.
background
The Identity-Tick Refrigerator Spec module derives engineering properties for a phantom-cavity refrigerator whose per-cycle cooling equals $J(φ) · k_B · T_bath$. Cumulative cooling is defined directly as $C(n) = n · f$, where $f$ is the cooling fraction (equal to $J(φ)$ in the chosen units). The module supplies the zero-cycle case as one of the fields required by the refrigerator certification record.
proof idea
The proof is a one-line wrapper that unfolds the definition of cumulativeCooling (which expands to the product of zero and the cooling fraction) and applies simp to obtain the equality with zero.
why it matters in Recognition Science
This base case is required to populate the IdentityTickRefrigeratorCert record, which assembles positivity, band, and monotonicity properties for the refrigerator specification. It supplies the initial condition for the cumulative-cooling ladder in the J5 engineering track and supports the falsifier that any realized device must stay inside the interval $[J(φ)/2, 2·J(φ)] · k_B · T_bath$.
scope and limits
- Does not compute cooling for any positive cycle count.
- Does not incorporate non-ideal thermal losses or fluctuations.
- Does not determine the numerical value of the cooling fraction.
formal statement (Lean)
48theorem cumulativeCooling_zero : cumulativeCooling 0 = 0 := by
proof body
One-line wrapper that applies unfold.
49 unfold cumulativeCooling; simp
50