k_R_lt_half
plain-language theorem explainer
The theorem shows that the RS Boltzmann constant k_R equals ln phi and satisfies k_R < 0.5 in natural units. Workers deriving thermal energy scales from the ledger bit cost would cite this bound when calibrating against the phi-ladder. The proof unfolds the definition, applies the lemma phi_lt_onePointSixTwo, and closes the inequality via log monotonicity plus a Taylor estimate that exp(0.5) exceeds 1.62.
Claim. Let $k_R :=$ ln$phi$ where $phi = (1 + sqrt(5))/2$ is the golden ratio. Then $k_R < 1/2$.
background
In the BoltzmannConstant module the RS analog k_R is introduced as the fundamental ledger bit cost: k_R = ln phi. The module states that this quantity replaces k_B because temperature measures average cost per degree of freedom and the ledger self-similarity scale is fixed by phi (T6). The upstream lemma phi_lt_onePointSixTwo supplies the concrete numerical bound phi < 1.62, obtained from sqrt(5) < 2.24. The definition k_R = Real.log Constants.phi is the only noncomputable constant appearing in the signature.
proof idea
The tactic proof first unfolds k_R to Real.log phi. It then invokes phi_lt_onePointSixTwo to obtain log phi < log 1.62. A separate block shows log 1.62 < 0.5 by proving exp(0.5) > 1.62 via Real.exp_bound with n=4 and a four-term Taylor sum, followed by two applications of Real.log_lt_log and linarith to finish the chain.
why it matters
The result supplies the upper half of the C-006 bounds on k_R, confirming the interval (0.47, 0.49) once paired with the matching lower bound. It directly supports the thermal_energy_at_unit_T sibling and the C006_certificate. Within the framework it anchors the Boltzmann constant to the J-bit cost forced by T5 J-uniqueness and T6 phi, closing one link in the constants derivation that begins from the LawOfExistence structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.