boltzmann_analog_bounds
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 in Recognition Science
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.
scope and limits
- Does not derive the exact numerical value of log phi.
- Does not connect k_R to the Recognition Composition Law.
- Does not address the mass formula or phi-ladder rungs.
- Does not treat the Berry creation threshold or Z_cf.
formal statement (Lean)
161theorem boltzmann_analog_bounds : Real.log phi > 0 ∧ Real.log phi < (0.5 : ℝ) := by
proof body
Term-mode proof.
162 constructor
163 · exact boltzmann_analog_positive
164 · exact boltzmann_analog_lt_half
165
166/-! ## Section: Additional Phi Bounds -/
167
168/-- **CALCULATED**: φ⁻¹ = φ - 1 (inverse formula). -/