IndisputableMonolith.Engineering.IdentityTickRefrigeratorSpec
The module specifies the identity tick refrigerator in the Recognition Science engineering layer using the J-cost coefficient at the golden ratio fixed point. It defines coolingFraction together with cumulativeCooling and proves their basic positivity and monotonicity properties. The central object is IdentityTickRefrigeratorCert, which certifies the cooling behavior against the fundamental tick τ₀. The module consists of definitions and short lemmas that establish the required algebraic facts.
claimThe J-cost coefficient is $J(φ) = φ - 3/2 ≈ 0.118$. Cooling fraction is the constant $f = J(φ)$. Cumulative cooling satisfies $C(0) = 0$ and $C(n+1) = C(n) + f$, with $C(n) > 0$ for $n > 0$ and strict monotonicity.
background
Constants supplies the RS-native time quantum τ₀ = 1 tick. Cost supplies the J-cost function $J(x) = (x + x^{-1})/2 - 1$, which at the self-similar fixed point φ evaluates to φ - 3/2. The module works in the engineering domain and imports Mathlib for ordering and arithmetic facts. It specializes these primitives to the identity-tick refrigerator model whose cooling is governed by the single coefficient J(φ).
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies IdentityTickRefrigeratorCert and the supporting cooling lemmas that feed the engineering layer of the Recognition Science framework. It instantiates the J-uniqueness and phi fixed-point results from the forcing chain (T5-T6) for a concrete cooling specification. The refrigerator_one_statement sibling collects the certified properties into a single usable claim.
scope and limits
- Does not derive J(φ) from the forcing chain.
- Does not model thermal dynamics or heat transfer.
- Does not extend the model beyond identity ticks.
- Does not compute numerical cooling rates for specific hardware.
depends on (2)
declarations in this module (11)
-
def
coolingFraction -
theorem
coolingFraction_pos -
theorem
coolingFraction_band -
def
cumulativeCooling -
theorem
cumulativeCooling_zero -
theorem
cumulativeCooling_succ -
theorem
cumulativeCooling_pos -
theorem
cumulativeCooling_strict_mono -
structure
IdentityTickRefrigeratorCert -
def
identityTickRefrigeratorCert -
theorem
refrigerator_one_statement