coolingFraction
plain-language theorem explainer
The definition supplies the J-cost coefficient J(φ) = φ - 3/2 ≈ 0.118 for phantom-cavity refrigerator cooling. Engineers computing per-cycle heat extraction Q_per_cycle = J(φ) · k_B · T_bath cite this constant. It is introduced by direct assignment of the real number phi minus three halves.
Claim. The cooling fraction is defined as $φ - 3/2$, where $φ$ is the golden ratio.
background
The Identity-Tick Refrigerator Spec module models phantom-cavity cooling (RS_PAT_029) with per-cycle extraction Q_per_cycle = J(φ) · k_B · T_bath, where J(φ) ≈ 0.118 is the fraction of bath thermal energy. The J-cost function satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and evaluates at the golden ratio to φ - 3/2. Cumulative cooling after n cycles is then n times this fraction in units of k_B · T_bath.
proof idea
The declaration is a direct definition that assigns the real number phi minus three halves. No lemmas or tactics are applied.
why it matters
This definition anchors the IdentityTickRefrigeratorCert structure and supplies the base value for the refrigerator_one_statement theorem, which asserts the fraction lies in (0.11, 0.13) with strictly monotonic cumulative cooling. It fills the engineering derivation track J5 of Plan v5, linking the phi fixed point (T6) to the eight-tick octave and D = 3. It leaves open experimental verification of the phi-cavity carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.