theorem
proved
alphaG_pred_bracket
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Masses.AlphaGScoreCard on GitHub at line 188.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
185 simpa [mul_assoc, mul_left_comm, mul_comm] using hltNum
186 simpa [alphaG_pred_closed] using h1
187
188theorem alphaG_pred_bracket : (4.5e9 : ℝ) < row_alphaG_pred ∧ row_alphaG_pred < (4.85e9 : ℝ) :=
189 ⟨alphaG_pred_lower, alphaG_pred_upper⟩
190
191/-! ## CODATA reference (SI units, dimensionless) -/
192
193def alphaG_codata : ℝ := 1.7518e-45
194
195theorem codata_very_small : alphaG_codata < 1e-40 := by
196 unfold alphaG_codata; norm_num
197
198theorem native_very_not_codata : alphaG_codata < row_alphaG_pred := by
199 have h1 := alphaG_pred_lower
200 have h0 : alphaG_codata < (1e9 : ℝ) := by
201 unfold alphaG_codata; norm_num
202 linarith [h0, h1]
203
204/-!
205## Falsifier (one line)
206
207A CODATA-consistent dimensionless `α_G` in SI and the RS-native
208`G m_e^2 / (ℏ c)` written with `electron_structural_mass` cannot be the same
209real number: matching experiment requires the explicit SI mass bridge, not
210identification of the raw coherence-mass value with the kilogram number.
211-/
212
213structure AlphaGScoreCardCert where
214 native_bracket : (4.5e9 : ℝ) < row_alphaG_pred ∧ row_alphaG_pred < (4.85e9 : ℝ)
215 not_codata : alphaG_codata < row_alphaG_pred
216
217def cert : AlphaGScoreCardCert where
218 native_bracket := alphaG_pred_bracket