pith. machine review for the scientific record. sign in
theorem proved tactic proof

shadow_diameter_correction

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  55theorem shadow_diameter_correction (Rs lambda_rec : ℝ) (h_Rs : Rs > 0) (h_lambda : lambda_rec > 0) :
  56    ∃ (delta_D : ℝ), delta_D = (lambda_rec / Rs) * (5.196 * Rs) := by

proof body

Tactic-mode proof.

  57  -- Standard GR shadow diameter is D = 3√3 Rs ≈ 5.196 Rs.
  58  -- The RS correction depends on the ratio of the recognition wavelength to the horizon.
  59  -- SCAFFOLD: The 5.196 factor is an approximation of 3√3.
  60  -- The actual derivation requires the full ILG geodesic integration.
  61  -- See: LaTeX Manuscript, Chapter "Astrophysical Tests", Section "Shadow Fringe".
  62  use (lambda_rec / Rs) * (5.196 * Rs)
  63  rfl
  64
  65/-- **THEOREM: Primordial Black Hole Detectability**
  66    For a primordial black hole with Rs ~ 1 micron, the RS correction
  67    becomes significant (~10^-29 relative shift), potentially detectable
  68    by future high-precision experiments. -/

depends on (17)

Lean names referenced from this declaration's body.