cumulativeCooling_succ
The recurrence for cumulative cooling states that the total after n+1 cycles equals the total after n cycles plus the fixed per-cycle fraction J(φ) = φ - 3/2. Engineers modeling the phantom-cavity refrigerator cite this step to assemble the inductive certificate. The proof is a one-line wrapper that unfolds the cumulative definition and applies ring simplification.
claimLet $C(n) = n · J(φ)$ with $J(φ) = φ - 3/2$. Then $C(n+1) = C(n) + J(φ)$.
background
The Identity-Tick Refrigerator Spec module derives the phantom-cavity refrigerator (RS_PAT_029) with per-cycle cooling $Q = J(φ) · k_B · T_bath$, where $J(φ) ≈ 0.118$. Cumulative cooling after n cycles is defined as n times this fraction. The sibling definition coolingFraction sets $J(φ) := φ - 3/2$, while cumulativeCooling sets the total as the product with n.
proof idea
This is a one-line wrapper. It unfolds the definition of cumulativeCooling, pushes the natural-number cast to reals, and applies the ring tactic to confirm the arithmetic identity.
why it matters in Recognition Science
This successor step supplies the inductive clause for the identityTickRefrigeratorCert certificate, which bundles positivity, band, and monotonicity properties. It closes the J5 engineering track by grounding cumulative cooling in the phi-based J-cost from the Recognition Science forcing chain.
scope and limits
- Does not derive the value of phi or J(φ).
- Does not address physical realizability or losses.
- Does not extend to non-integer cycle counts.
- Does not incorporate temperature dependence.
formal statement (Lean)
51theorem cumulativeCooling_succ (n : ℕ) :
52 cumulativeCooling (n + 1) = cumulativeCooling n + coolingFraction := by
proof body
One-line wrapper that applies unfold.
53 unfold cumulativeCooling; push_cast; ring
54