thermal_cost
plain-language theorem explainer
The declaration defines the thermal cost per recognition tick as the product of temperature T and the natural logarithm of 2 in RS-native units. Researchers closing dissipation bounds in the Landauer limit within discrete recognition frameworks would cite this when anchoring entropy production to the eight-tick cycle. The definition is a direct one-line scaling that supplies the information-theoretic minimum energy per bit erased.
Claim. The base thermal cost per tick at temperature $T$ equals $T$ times the natural logarithm of 2.
background
This definition appears in the module on Landauer Limit and 8-Tick Dissipation, which formalizes the link between Recognition Science cost and thermodynamic entropy. It draws on the J-cost from upstream results: ObserverForcing.cost states that the cost of any recognition event is the J-cost of its state, while MultiplicativeRecognizerL4.cost gives the derived cost of a comparator on positive ratios. Breath1024.T supplies the fundamental period and LedgerFactorization.of calibrates the J function on the positive reals under multiplication.
proof idea
The definition is a direct one-line expression that multiplies the input temperature by the natural logarithm of 2, implementing the standard Landauer energy scale per bit.
why it matters
This definition supplies the base thermal scale required in Phase 7.5.2 to anchor the theory in the Landauer limit. It provides the constant factor needed for sibling results such as landauer_bound_holds and total_dissipation_bound that close the eight-tick dissipation limit. It connects the recognition cost framework (T5 J-uniqueness and T7 eight-tick octave) to physical dissipation bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.