`GREffect`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.GeneralRelativityFromRS
domain: Physics
line: 26 · 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 26.

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

used by

formal source

  23namespace IndisputableMonolith.Physics.GeneralRelativityFromRS
  24open Constants
  25
  26inductive GREffect where
  27  | gravitationalLensing | timeDilation | perihelionPrecession | frameDragging | gravitationalWaves
  28  deriving DecidableEq, Repr, BEq, Fintype
  29
  30theorem grEffectCount : Fintype.card GREffect = 5 := by decide
  31
  32/-- Einstein coupling constant κ = 8φ^5/π > 0. -/
  33noncomputable def einsteinKappa : ℝ := 8 * phi ^ 5 / Real.pi
  34
  35theorem einsteinKappa_pos : 0 < einsteinKappa := by
  36  unfold einsteinKappa
  37  apply div_pos
  38  · apply mul_pos (by norm_num) (pow_pos phi_pos 5)
  39  · exact Real.pi_pos
  40
  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.