k_R_bounds
plain-language theorem explainer
Bounds on the RS Boltzmann constant are established by showing that ln(φ) lies strictly between 0.47 and 0.49 whenever φ is between 1.61 and 1.62. Researchers deriving thermodynamic relations in RS-native units cite this to anchor the ledger bit cost scale. The tactic proof applies logarithm monotonicity together with Taylor remainder estimates on the exponential to certify the numerical inequalities.
Claim. $0.47 < k_R < 0.49$ where $k_R = $ ln($φ$) and $φ$ is the golden ratio satisfying $1.61 < φ < 1.62$.
background
In the module on Boltzmann constant derivation, k_R is introduced as the ledger bit cost k_R := ln(φ), replacing the conventional k_B in RS thermodynamics. This follows from the self-similar structure where each recognition bit carries cost ln(φ) with φ the golden ratio forced by the ledger (T6). The local setting derives k_R from the Recognition Composition Law and the fixed point phi. Upstream lemmas supply the tight bounds 1.61 < φ < 1.62, which are used here to pin down the numerical interval for k_R.
proof idea
The proof unfolds the definition of k_R to Real.log phi. It invokes the lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo to obtain the interval for phi. For the lower bound it applies Real.log_lt_log to show log(1.61) < log(phi), then uses Real.exp_bound' to verify 0.47 < log(1.61) via exp(0.47) < 1.61. The upper bound proceeds symmetrically with Real.exp_bound to show log(1.62) < 0.49.
why it matters
This declaration is theorem C-006.4 in the Boltzmann constant section. It supplies the numerical bounds needed to confirm k_R ≈ 0.481 lies inside (0.47, 0.49), supporting the identification k_R = J_bit. It closes the derivation chain from the phi fixed point (T6) to the thermal energy scale, with no open questions indicated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.