`optical_reduces_to_gr`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.Cosmology.OpticalExtension
domain: Relativity
line: 61 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.Cosmology.OpticalExtension on GitHub at line 61.

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

formal source

  58  ring
  59
  60/-- Theorem: Optical rescaling reduces to GR when the coupling C = 0. -/
  61theorem optical_reduces_to_gr (z : ℝ) (bg_DA : ℝ) (P : ILG.KernelParams)
  62    (hC : P.C = 0) :
  63    DA_rescaled z bg_DA P = bg_DA := by
  64  unfold DA_rescaled Upsilon
  65  simp [hC]
  66
  67end Cosmology
  68end Relativity
  69end IndisputableMonolith

papers checked against this theorem

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