theorem
proved
term proof
bcs_ratio_approx
show as:
view Lean formalization →
formal statement (Lean)
125theorem bcs_ratio_approx : (1.7 : ℝ) < bcsDeltaTcRatio ∧ bcsDeltaTcRatio < (2.1 : ℝ) := by
proof body
Term-mode proof.
126 dsimp [bcsDeltaTcRatio]
127 -- Use proven bounds from Numerics.Interval.Log: 0.48 < log(φ) < 0.483
128 -- Constants.phi = (1 + √5)/2 = Real.goldenRatio
129 have h_phi_eq : Constants.phi = Real.goldenRatio := rfl
130 rw [h_phi_eq]
131 have hlo : (0.48 : ℝ) < Real.log Real.goldenRatio := Numerics.log_phi_gt_048
132 have hhi : Real.log Real.goldenRatio < (0.483 : ℝ) := Numerics.log_phi_lt_0483
133 constructor
134 · -- 1.7 < 2 * log(φ) + 1 ⟺ 0.35 < log(φ)
135 -- Since 0.48 > 0.35, we have log(φ) > 0.48 > 0.35
136 linarith
137 · -- 2 * log(φ) + 1 < 2.1 ⟺ log(φ) < 0.55
138 -- Since log(φ) < 0.483 < 0.55, we have the result
139 linarith
140
141end Chemistry
142end IndisputableMonolith