boltzmann_analog_bounds
plain-language theorem explainer
The theorem establishes that the natural logarithm of the golden ratio satisfies 0 < log phi < 0.5. Researchers verifying Recognition Science predictions for the Boltzmann analog constant k_R would cite this bound. The proof is a one-line wrapper that combines the positivity lemma and the upper-bound lemma for log phi.
Claim. $0 < \log \phi < 0.5$, where $\phi$ is the golden ratio and $k_R$ denotes the Boltzmann analog.
background
The module supplies calculated proofs for constants listed in the COMPLETE_PROBLEM_REGISTRY, specifically covering the fine-structure constant (0 < alpha < 0.1), speed of light (c = 1 in RS-native units), and Boltzmann analog k_R (0 < k_R < 0.5). Here k_R is identified with Real.log phi. The local setting uses explicit numerical bounds and positivity tactics on the golden ratio fixed point.
Upstream results include boltzmann_analog_positive, which applies Real.log_pos to one_lt_phi, and boltzmann_analog_lt_half, which compares phi < 1.62 against e^{0.5}.
proof idea
The term proof uses the constructor tactic to split the conjunction into two goals. It then applies boltzmann_analog_positive to discharge the lower bound and boltzmann_analog_lt_half to discharge the upper bound.
why it matters
This declaration completes registry item C-006 inside the Constants Predictions module. It supplies the required bound on the Boltzmann analog that follows from the phi fixed point (T6) and the eight-tick octave structure. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.