boltzmann_analog_bounds
plain-language theorem explainer
Recognition Science sets the Boltzmann analog k_R equal to the natural log of the golden ratio phi. The theorem confirms the strict bound 0 < log phi < 0.5 that matches the predicted range for k_R. Workers verifying constant predictions in the unification registry cite this result. The proof is a direct conjunction introduction that invokes the positivity lemma and the upper-bound lemma.
Claim. $0 < log phi < 0.5$ where phi denotes the golden ratio.
background
The module supplies calculated proofs for constants drawn from the Recognition Science registry. Item C-006 requires the bound 0 < k_R < 0.5 for the Boltzmann analog k_R, which is identified with log phi. The golden ratio itself is the self-similar fixed point forced by the J-uniqueness step in the foundation chain.
proof idea
The proof is a term-mode wrapper. It opens the conjunction with constructor and then applies exact to the sibling theorems boltzmann_analog_positive and boltzmann_analog_lt_half.
why it matters
The result discharges the proof obligation for registry item C-006 inside the constants predictions module. It supplies a rigorous verification of the phi-derived range that is consistent with the forcing chain landmarks T5-T6 and the eight-tick octave. No downstream theorems depend on it in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.