boltzmann_analog_lt_half
plain-language theorem explainer
The inequality ln(φ) < 1/2 holds for the golden ratio φ. Researchers verifying Recognition Science constant bounds cite it to close the upper limit on the Boltzmann analog k_R. The tactic proof chains the explicit bound φ < 1.62 with monotonicity of log and a square comparison of 1.62 against exp(0.5) using the Taylor lower bound exp(1) ≥ 8/3.
Claim. $k_R = {ln} φ < 1/2$, where $φ = (1 + √5)/2$ is the golden ratio and $k_R$ is the RS Boltzmann analog.
background
The module supplies calculated proofs for registry items C-001 (α), C-005 (c = 1), and C-006 (0 < k_R < 0.5). The Boltzmann analog is defined as k_R := ln(φ) and replaces k_B in RS-native thermodynamics. Upstream, phi_lt_onePointSixTwo supplies the tighter numerical bound φ < 1.62 obtained from √5 < 2.24. All proofs in the module rely on norm_num, nlinarith, and positivity tactics with explicit decimal bounds.
proof idea
The proof invokes phi_lt_onePointSixTwo to obtain φ < 1.62, then applies Real.log_lt_log (with positivity) to deduce ln(φ) < ln(1.62). It next rewrites the target to the equivalent claim 1.62 < exp(0.5) by showing 1.62² < exp(1) and verifying exp(1) ≥ 8/3 > 2.6244 via the partial sum of the exponential series up to 1/3!. The final step uses nlinarith on the squared inequality and positivity of exp(0.5).
why it matters
This lemma is applied directly by boltzmann_analog_bounds to obtain the closed interval 0 < k_R < 0.5 and by constants_predictions_cert_exists to witness the full ConstantsPredictionsCert. It supplies the calculated upper bound for registry item C-006 in the module documentation, supporting the framework claim that the RS Boltzmann analog lies strictly below one half in native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.