`AlphaGScoreCardCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Masses.AlphaGScoreCard
domain: Masses
line: 213 · 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 213.

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

used by

formal source

 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.