pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Constants.BoltzmannConstant

show as:
view Lean formalization →

The module defines the RS Boltzmann analog k_R = ln(φ) as the fundamental cost per ledger bit in native units. Researchers modeling holographic information bounds or black-hole thermodynamics cite it when replacing k_B with recognition cost. It consists of the core definition plus supporting lemmas establishing positivity, non-zero status, and bounds relative to 1/2.

claim$k_R = ln(φ)$, the recognition cost per ledger bit that replaces $k_B$ in RS-native thermodynamics.

background

Recognition Science works in units where the fundamental time quantum τ₀ equals one tick. The parent Constants module supplies this τ₀. The present module introduces k_R = ln(φ) as the per-bit ledger cost, together with elementary properties (positivity, non-vanishing, and an upper bound k_R < 1/2) that follow directly from the definition of φ as the self-similar fixed point.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the recognition cost k_R that downstream unification results on BlackHoleBandwidth, ConsciousnessBandwidth, and RecognitionBandwidth invoke when bounding information flow. It fills definition C-006 and anchors the connection between the phi-ladder and the eight-tick octave used in holographic arguments.

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)