coolingFraction_pos
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.