theorem
proved
alphaG_pred_lower
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Masses.AlphaGScoreCard on GitHub at line 149.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
model -
independent -
of -
of -
from -
independent -
of -
of -
alphaG_pred_closed -
row_alphaG_pred -
phi_gt_1618 -
phi_gt_1618 -
phi_gt_1618
used by
formal source
146
147/-! ## Bracket: single-φ function (avoids a fake independence assumption) -/
148
149theorem alphaG_pred_lower : (4.5e9 : ℝ) < row_alphaG_pred := by
150 have hφ : (1.618 : ℝ) < phi := by
151 simpa [show phi = (Real.goldenRatio : ℝ) from rfl] using phi_gt_1618
152 have hpiUB : (Real.pi : ℝ) < 3.142 := by
153 linarith [Real.pi_lt_d6, Real.pi_pos]
154 have hN :
155 (2 : ℝ) ^ (-(44 : ℤ)) * (1.618 : ℝ) ^ (112 : ℝ) < (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) := by
156 have hr112 : (1.618 : ℝ) ^ (112 : ℝ) < phi ^ (112 : ℝ) := by
157 exact Real.rpow_lt_rpow (by norm_num) hφ (by nlinarith)
158 nlinarith [hr112, zpow_pos (by norm_num : (0 : ℝ) < (2 : ℝ))]
159 have h0 : (4.5e9 : ℝ) * (3.142 : ℝ) < (2 : ℝ) ^ (-(44 : ℤ)) * (1.618 : ℝ) ^ (112 : ℝ) := by
160 -- conservative numeric bound (independent of the model)
161 nlinarith
162 have hltNum : (4.5e9 : ℝ) * Real.pi < (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) := by
163 nlinarith [h0, hN, hpiUB, Real.pi_pos]
164 have h1 : (4.5e9 : ℝ) < (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) / Real.pi := by
165 rw [lt_div_iff₀ Real.pi_pos]
166 simpa [mul_assoc, mul_left_comm, mul_comm] using hltNum
167 simpa [alphaG_pred_closed] using h1
168
169theorem alphaG_pred_upper : row_alphaG_pred < (4.85e9 : ℝ) := by
170 have hφ : phi < (1.6185 : ℝ) := by
171 simpa [show phi = (Real.goldenRatio : ℝ) from rfl] using phi_lt_16185
172 have hpiLB : (3.1415 : ℝ) < (Real.pi : ℝ) := by
173 linarith [Real.pi_gt_d6, Real.pi_pos]
174 have hN : (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) < (2 : ℝ) ^ (-(44 : ℤ)) * (1.6185 : ℝ) ^ (112 : ℝ) := by
175 have hr112 : (phi : ℝ) ^ (112 : ℝ) < (1.6185 : ℝ) ^ (112 : ℝ) := by
176 exact Real.rpow_lt_rpow (by nlinarith [phi_pos, hφ]) hφ (by nlinarith)
177 nlinarith [hr112, zpow_pos (by norm_num : (0 : ℝ) < (2 : ℝ))]
178 have h0 :
179 (2 : ℝ) ^ (-(44 : ℤ)) * (1.6185 : ℝ) ^ (112 : ℝ) < (4.85e9 : ℝ) * (3.1415 : ℝ) := by