pith. machine review for the scientific record. sign in
structure

GeneralRelativityCert

definition
show as:
view math explainer →
module
IndisputableMonolith.Physics.GeneralRelativityFromRS
domain
Physics
line
44 · github
papers citing
none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.GeneralRelativityFromRS on GitHub at line 44.

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

  41/-- All 5 GR effects tested and consistent. -/
  42theorem all_gr_effects_tested : Fintype.card GREffect = 5 := grEffectCount
  43
  44structure GeneralRelativityCert where
  45  five_effects : Fintype.card GREffect = 5
  46  kappa_positive : 0 < einsteinKappa
  47
  48noncomputable def generalRelativityCert : GeneralRelativityCert where
  49  five_effects := grEffectCount
  50  kappa_positive := einsteinKappa_pos
  51
  52end IndisputableMonolith.Physics.GeneralRelativityFromRS

papers checked against this theorem

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