`etherington_duality_preserved`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.Cosmology.OpticalExtension
domain: Relativity
line: 52 · 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 52.

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

  49
  50/-- Main Theorem (Target G): Etherington duality is preserved under optical rescaling.
  51    Regardless of the Upsilon rescaling, D_L = (1 + z)^2 * D_A remains satisfied. -/
  52theorem etherington_duality_preserved (z : ℝ) (bg_DA bg_DL : ℝ) (P : ILG.KernelParams)
  53    (h_bg_dual : bg_DL = (1 + z)^2 * bg_DA) :
  54    DL_rescaled z bg_DL P = (1 + z)^2 * DA_rescaled z bg_DA P := by
  55  unfold DL_rescaled
  56  rw [h_bg_dual]
  57  field_simp
  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.