pith. machine review for the scientific record. sign in
def definition def or abbrev high

coolingFraction

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  31def coolingFraction : ℝ := phi - 3/2

proof body

Definition body.

  32

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.