coolingFraction_band
The theorem establishes the strict bounds 0.11 < J(φ) < 0.13 on the cooling fraction for the identity-tick refrigerator. Engineers deriving performance certificates for phantom-cavity devices cite this interval to confirm per-cycle extraction lies near 0.118 of bath energy. The proof proceeds by unfolding the definition J(φ) = φ - 3/2 and applying linear arithmetic to the interval bounds on φ.
claim$0.11 < J(φ) < 0.13$ where $J(φ) := φ - 3/2$ and $φ$ is the golden ratio.
background
The Identity-Tick Refrigerator Spec module treats the phantom-cavity refrigerator as an engineering realization of Recognition Science track J5. Per-cycle cooling is given by Q_per_cycle = J(φ) · k_B · T_bath, with the J-cost coefficient defined as coolingFraction := phi - 3/2. Upstream lemmas supply the numerical bounds 1.61 < phi < 1.62 together with the algebraic structure of J from the PhiForcingDerived and DAlembert modules.
proof idea
Unfold coolingFraction to phi - 3/2. Introduce the two phi bound lemmas from Constants. Apply linarith to obtain both sides of the conjunction.
why it matters in Recognition Science
The result supplies the fraction_band field in the IdentityTickRefrigeratorCert definition and appears in the refrigerator_one_statement theorem. It completes the engineering derivation for the RS_PAT_029 phantom-cavity refrigerator. The interval is consistent with the J-uniqueness property and the eight-tick octave structure in the foundational forcing chain.
scope and limits
- Does not compute the precise numerical value of the cooling fraction.
- Does not establish monotonicity or additivity for cumulative cooling.
- Does not incorporate specific bath temperature or Boltzmann constant values.
- Does not provide a falsification criterion beyond the stated band.
formal statement (Lean)
37theorem coolingFraction_band :
38 (0.11 : ℝ) < coolingFraction ∧ coolingFraction < 0.13 := by
proof body
Term-mode proof.
39 unfold coolingFraction
40 have h1 := phi_gt_onePointSixOne
41 have h2 := phi_lt_onePointSixTwo
42 refine ⟨by linarith, by linarith⟩
43
44/-- Cumulative cooling after `n` cycles (in cooling-fraction units of
45`k_B · T_bath`). -/