coolingFraction_pos
The cooling fraction J(φ) = φ - 3/2 is strictly positive in the identity-tick refrigerator model. Engineers deriving per-cycle heat extraction for phi-cavity devices cite this to guarantee net cooling. The proof unfolds the definition and reduces the claim to the known bound φ > 1.5 via linear arithmetic.
claim$0 < J(φ)$ where $J(φ) := φ - 3/2$
background
The module derives the phantom-cavity refrigerator (RS_PAT_029) with per-cycle cooling Q_per_cycle = J(φ) · k_B · T_bath, where J(φ) ≈ 0.118 is the J-cost coefficient. coolingFraction is defined directly as phi - 3/2. The upstream lemma phi_gt_onePointFive supplies the tighter bound φ > 1.5, obtained from the quadratic definition of φ and the inequality √5 > 2.
proof idea
Unfold coolingFraction to phi - 3/2. Invoke phi_gt_onePointFive to obtain 1.5 < phi. Apply linarith to conclude strict positivity.
why it matters in Recognition Science
This supplies the positivity fact required by cumulativeCooling_pos, cumulativeCooling_strict_mono, and the packaging into identityTickRefrigeratorCert. It completes the engineering one-statement that J(φ) lies in (0.11, 0.13) and that cumulative cooling is strictly monotonic in cycle count, anchoring the J5 track of the Recognition Science plan.
scope and limits
- Does not establish numerical bounds beyond positivity.
- Does not model thermal losses outside the J-cost term.
- Does not prove physical realizability of the phi-cavity.
- Does not address equilibrium after many cycles.
Lean usage
theorem use_in_cumulative : 0 < cumulativeCooling 3 := by exact cumulativeCooling_pos (by norm_num)formal statement (Lean)
33theorem coolingFraction_pos : 0 < coolingFraction := by
proof body
Term-mode proof.
34 unfold coolingFraction
35 have := phi_gt_onePointFive; linarith
36