k_R_eq_J_bit
plain-language theorem explainer
The declaration equates the Recognition Science Boltzmann constant k_R to the ledger bit cost J_bit. Researchers deriving thermodynamic relations from the recognition ledger would cite this identity to anchor thermal energy scales. The proof is a one-line reflexivity that follows immediately from the shared definition of both quantities as the natural logarithm of the golden ratio phi.
Claim. $k_R = J_{bit}$ where $k_R := ln φ$ is the Recognition Science Boltzmann analog and $J_{bit}$ is the fundamental cost of one bit in the recognition ledger.
background
In the BoltzmannConstant module the RS Boltzmann analog is defined by k_R := Real.log Constants.phi, with φ the golden ratio forced by the ledger self-similarity (T6). The module doc states that this replaces k_B in native units and supplies the exchange rate between thermal energy and ledger cost: E = k_R · T at unit temperature yields the bit cost ln(φ). Upstream the same definition appears in Gravity.UltramassiveBH and the Constants structure from LawOfExistence bundles related ledger parameters without altering the equality.
proof idea
The proof is a one-line term-mode reflexivity that applies rfl directly to the shared definitional expression Real.log Constants.phi.
why it matters
This identity completes the C-006 series by identifying the thermal energy quantum with the ledger bit cost, directly feeding the thermal-energy-at-unit-T result that follows in the same module. It realizes the framework claim that temperature is not postulated but emerges from the phi-ladder cost structure (T6, RCL). No open scaffolding remains for this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.