pith. sign in
module module moderate

IndisputableMonolith.Engineering.IdentityTickRefrigeratorSpec

show as:
view Lean formalization →

This module specifies the identity tick refrigerator in the Recognition Science engineering layer by defining coolingFraction and cumulativeCooling from the J-cost coefficient J(φ) = φ - 3/2. Engineers or physicists modeling tick-based cooling systems would cite these objects. The module consists of a sequence of definitions and elementary lemmas on positivity and monotonicity.

claimLet $J(φ) = φ - 3/2 ≈ 0.118$. Define the cooling fraction function and the cumulative cooling function, together with the certificate IdentityTickRefrigeratorCert asserting the refrigerator specification.

background

The module imports the RS time quantum τ₀ = 1 tick from Constants and cost structures from the Cost module. It introduces coolingFraction and cumulativeCooling to quantify refrigeration effects based on the J-cost coefficient. The local theoretical setting is the engineering application of Recognition Science to identity-tick cooling systems.

proof idea

This is a definition module, no proofs. It supplies the specification through definitions of coolingFraction, cumulativeCooling and their basic properties (positivity, strict monotonicity) together with the IdentityTickRefrigeratorCert.

why it matters in Recognition Science

The module supplies the engineering specification for identity tick refrigerators. It applies the J-cost coefficient to practical refrigeration modeling and positions these objects for parent theorems on cooling systems in the Recognition framework (no current downstream uses listed).

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (11)