identityTickRefrigeratorCert
plain-language theorem explainer
The definition constructs a certificate structure bundling positivity, the interval (0.11, 0.13), and the additive strictly monotonic behavior of cumulative cooling for the phantom-cavity refrigerator. Device modelers working with J(φ)-scaled thermal extraction would cite the certificate to confirm the per-cycle energy removal. It is assembled by direct record-field assignment from six sibling lemmas that already establish the numerical bounds on the cooling fraction and the arithmetic properties of its cumulative sum.
Claim. Let $c$ denote the cooling fraction per cycle. The certificate asserts $0 < c$, $0.11 < c < 0.13$, the cumulative function $C(n) := n c$ satisfies $C(0) = 0$, $C(n+1) = C(n) + c$ for all $n$, $C(n) > 0$ whenever $n ≥ 1$, and $n < m$ implies $C(n) < C(m)$.
background
In the Identity-Tick Refrigerator Spec module the cooling fraction is the per-cycle energy extraction normalized to $k_B T_{bath}$, numerically equal to $J(φ)$ where $J(x) = (x + x^{-1})/2 - 1$. Cumulative cooling after $n$ cycles is defined by $C(n) = n · c$. The module presents this construction as the engineering realization of the phantom-cavity refrigerator (RS_PAT_029) with $Q_{per cycle} = J(φ) · k_B · T_{bath} ≈ 0.118 k_B T_{bath}$.
proof idea
The definition builds the IdentityTickRefrigeratorCert record by direct field assignment: fraction_pos receives coolingFraction_pos, fraction_band receives coolingFraction_band, cumulative_zero receives cumulativeCooling_zero, cumulative_succ receives cumulativeCooling_succ, cumulative_pos receives cumulativeCooling_pos, and cumulative_strict_mono receives cumulativeCooling_strict_mono. No further tactics or reductions are applied.
why it matters
The definition supplies the complete bundled certificate for the refrigerator specification, closing the J5 engineering track. It packages the J-uniqueness (T5) and phi fixed-point (T6) properties into a single usable object for Recognition Science device modeling. The module doc states the falsifier: a bench refrigerator whose per-cycle cooling lies outside $[J(φ)/2, 2·J(φ)] · k_B T_{bath}$. No downstream theorems yet reference the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.