theorem
proved
native_very_not_codata
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 198.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
bridge -
consistent -
G -
G -
m_e -
G -
of -
one -
A -
of -
one -
of -
G -
of -
alphaG_codata -
alphaG_pred_lower -
row_alphaG_pred -
A -
A -
and -
electron_structural_mass -
one -
value -
one -
electron_structural_mass
used by
formal source
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