`alphaG_codata`

definition

show as: view math explainer →

module: IndisputableMonolith.Masses.AlphaGScoreCard
domain: Masses
line: 193 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Masses.AlphaGScoreCard on GitHub at line 193.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

 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
 219  not_codata := native_very_not_codata
 220
 221theorem cert_inhabited : Nonempty AlphaGScoreCardCert := ⟨cert⟩
 222
 223end

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.