IdentityTickRefrigeratorCert
plain-language theorem explainer
IdentityTickRefrigeratorCert bundles the positivity, interval membership, zero, recurrence, positivity, and strict monotonicity properties of cumulative cooling under the J-cost fraction f = phi - 3/2. Phantom-cavity refrigerator engineers cite it to certify the per-cycle cooling model against the predicted band. The structure is assembled by direct substitution of the four unfolding lemmas for cumulativeCooling together with the positivity and band facts for coolingFraction.
Claim. Let $f = phi - 3/2$. A certificate asserts $0 < f$, $0.11 < f < 0.13$, $C(0) = 0$, $C(n+1) = C(n) + f$ for all $n$, $C(n) > 0$ for $n >= 1$, and $C(n) < C(m)$ whenever $n < m$, where $C(n) = n f$.
background
The Identity-Tick Refrigerator Spec models phantom-cavity cooling with per-cycle heat extraction $Q = J(phi) k_B T_bath$ where $J(phi) = phi - 3/2 approx 0.118$. Cumulative cooling after n cycles is the linear extension $C(n) = n f$. The structure collects the elementary arithmetic facts that follow from this definition and the imported constants module.
proof idea
The structure is populated by supplying its six fields. Each field is obtained by a one-line wrapper: coolingFraction_pos and coolingFraction_band for the first two, then cumulativeCooling_zero, cumulativeCooling_succ, cumulativeCooling_pos, and cumulativeCooling_strict_mono obtained by unfolding the definition of cumulativeCooling and applying simp, ring, omega, mul_pos, and mul_lt_mul_iff_of_pos_right.
why it matters
The certificate supplies the engineering interface for the phantom-cavity refrigerator, feeding directly into the identityTickRefrigeratorCert constructor. It realizes the J-cost cooling fraction derived from the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain. The module falsifier gives the concrete bench-test criterion that would refute the model if observed cooling falls outside the predicted band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.