refrigerator_one_statement
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value of J(φ) from the forcing chain or RCL.
- Does not model cavity losses, thermal noise, or non-ideal heat leaks.
- Does not prove experimental achievability beyond the fraction interval.
- Does not address equilibrium after many cycles or entropy production.
formal statement (Lean)
88theorem refrigerator_one_statement :
89 0 < coolingFraction ∧
90 (0.11 : ℝ) < coolingFraction ∧ coolingFraction < 0.13 ∧
91 (∀ {n m : ℕ}, n < m → cumulativeCooling n < cumulativeCooling m) :=
proof body
Term-mode proof.
92 ⟨coolingFraction_pos, coolingFraction_band.1, coolingFraction_band.2,
93 @cumulativeCooling_strict_mono⟩
94
95end
96
97end IdentityTickRefrigeratorSpec
98end Engineering
99end IndisputableMonolith