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

shadow_fringe_exists

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)

  33theorem shadow_fringe_exists (tau0 : ℝ) (h_tau0 : tau0 > 0) :
  34    ∃ (rho : ℝ → ℝ), ∀ t, rho t = PhaseFringeDensity tau0 t ∧ (∃ t', rho t' ≠ 0) := by

proof body

Tactic-mode proof.

  35  use PhaseFringeDensity tau0
  36  intro t
  37  constructor
  38  · rfl
  39  · use 2 * tau0
  40    unfold PhaseFringeDensity
  41    -- sin(2π * 2τ0 / (8τ0)) = sin(π/2) = 1
  42    have h : 2 * Real.pi * (2 * tau0) / (8 * tau0) = Real.pi / 2 := by
  43      field_simp [h_tau0]
  44      ring
  45    rw [h]
  46    simp [Real.sin_pi_div_two]
  47
  48/-- **CERT(definitional): Shadow Diameter Correction**
  49    The predicted diameter of the black hole shadow is shifted by the ILG
  50    fringe factor $\epsilon_{fringe} \sim \lambda_{rec} / R_s$.
  51
  52    For M87*, Rs ≈ 1.9e10 km and λ_rec ≈ 1.6e-35 m.
  53    The correction is negligible for supermassive holes but becomes
  54    detectable for primordial ones. -/

depends on (16)

Lean names referenced from this declaration's body.