theorem
proved
shadow_fringe_observable_trivial
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Relativity.Lensing.ShadowPredictions on GitHub at line 111.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
108
109 This is a pure existence result - given any resolution res > 0,
110 we can find a wavelength that exceeds it. -/
111theorem shadow_fringe_observable_trivial (res : ℝ) :
112 ∃ lambda_fringe : ℝ, lambda_fringe > res := by
113 use res + 1
114 linarith
115
116/-- **EXPERIMENTAL PREDICTION: Shadow Fringe Frequency**
117 The interference fringe at the event horizon has a fundamental
118 frequency determined by the 8-tick cycle. -/
119def ShadowFringeFrequency (tau0 : ℝ) : ℝ := 1 / (8 * tau0)
120
121/-- **THEOREM: Fringe Frequency forced by 8-Tick**
122 The frequency of the shadow fringe is identically the inverse of the
123 8-tick cycle duration. -/
124theorem shadow_fringe_frequency_identity (tau0 : ℝ) (h_tau0 : tau0 > 0) :
125 ShadowFringeFrequency tau0 = 1 / (8 * tau0) := by
126 rfl
127
128theorem fringe_frequency_grounded (tau0 : ℝ) (h_tau0 : tau0 > 0) :
129 ShadowFringeFrequency tau0 > 0 := by
130 unfold ShadowFringeFrequency
131 positivity
132
133end Lensing
134end Relativity
135end IndisputableMonolith