cumulativeCooling_zero
plain-language theorem explainer
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.
Claim. Let $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
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$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.