pith. sign in
module module high

IndisputableMonolith.Constants.BoltzmannConstant

show as:
view Lean formalization →

The module defines the RS Boltzmann analog k_R as ln(φ), the fundamental cost per ledger bit replacing k_B in native thermodynamics. Bandwidth unification modules for black holes, consciousness, and recognition cite this definition when computing maintenance costs. The module supplies the core definition plus lemmas establishing positivity, bounds, and equivalence to J-bit cost.

claimThe RS Boltzmann analog is the constant \(k_R = \ln \phi\), where \(\phi\) is the golden ratio; it equals the fundamental cost per ledger bit and replaces the classical Boltzmann constant in Recognition Science thermodynamics.

background

The module belongs to the Constants domain and imports the parent Constants module, which supplies the RS time quantum (\tau_0 = 1) tick. Definition C-006 introduces (k_R = \ln \phi) as the cost per ledger bit. Sibling declarations establish that (k_R > 0), (k_R \neq 0), (k_R < 1/2), and (k_R = J)-bit cost, where J denotes the Recognition cost function.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the Boltzmann analog required by the bandwidth unification arguments. It feeds BlackHoleBandwidth (maximal recognition saturation), ConsciousnessBandwidth (holographic constraint on conscious extent), and RecognitionBandwidth (core definitions linking holographic bound, k_R cost, ILG parameters, and 8-tick cadence). It directly implements definition C-006 in the Recognition Science framework.

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)