`codata_very_small`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Masses.AlphaGScoreCard on GitHub at line 195.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

alphaG_codata IndisputableMonolith.Masses.AlphaGScoreCard

formal source

 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
 224
 225end IndisputableMonolith.Masses.AlphaGScoreCard

papers checked against this theorem

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