refrigerator_one_statement
plain-language theorem explainer
The theorem asserts that the per-cycle cooling fraction J(φ) is positive and lies strictly inside (0.11, 0.13), while cumulative cooling after n cycles is strictly monotonic in n. Recognition Science engineers modeling phantom-cavity refrigerators would cite the bound to fix Q_per_cycle = J(φ) k_B T_bath. The proof is a one-line term that assembles positivity, the numerical band, and the strict-mono theorem for cumulativeCooling.
Claim. Let $J(φ) := φ - 3/2$. Then $0 < J(φ)$, $0.11 < J(φ) < 0.13$, and for all natural numbers $n < m$ one has $n · J(φ) < m · J(φ)$.
background
coolingFraction is the definition J(φ) = φ - 3/2. cumulativeCooling(n) is the definition n · coolingFraction, giving total cooling after n cycles in units of k_B T_bath. The module sets the local context as the phantom-cavity refrigerator (RS_PAT_029) whose per-cycle heat extraction is exactly J(φ) k_B T_bath, with cumulative cooling therefore additive in cycle count.
proof idea
The proof is a term-mode conjunction that directly supplies coolingFraction_pos, the left and right conjuncts of coolingFraction_band, and the theorem cumulativeCooling_strict_mono.
why it matters
The declaration supplies the single-statement engineering summary for the identity-tick refrigerator specification. It encodes the falsifier criterion given in the module (bench measurement outside [J(φ)/2, 2 J(φ)] k_B T_bath) and closes the J5 track derivation of per-cycle cooling bounds inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.