Pith. sign in
module module high

IndisputableMonolith.Constants.BoltzmannConstant

show as:
view Lean formalization →

This module defines the RS Boltzmann analog k_R as ln(φ), the fundamental cost per ledger bit that replaces k_B in RS-native thermodynamics. Workers on holographic bounds, black-hole saturation, or consciousness bandwidth cite it when converting recognition events into energy scales. The module supplies the core definition plus supporting lemmas on positivity, bounds, and equivalence to J-bit cost.

claim$k_R := \ln(\phi)$, the recognition cost per ledger bit in RS-native units, with $\phi$ the golden-ratio fixed point.

background

The module lives in the Constants domain and imports the base Constants module whose sole content is the RS time quantum $\tau_0 = 1$ tick. It introduces the ledger-bit cost that appears in every subsequent bandwidth calculation. The definition is labeled C-006 and is stated directly as $k_R = \ln(\phi)$.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definition supplies the per-bit recognition cost required by the holographic arguments in RecognitionBandwidth, BlackHoleBandwidth, and ConsciousnessBandwidth. It implements the ledger cost that converts the eight-tick octave and phi-ladder into thermodynamic statements.

scope and limits

used by (3)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)