module module

`IndisputableMonolith.Relativity.Lensing.ShadowPredictions`

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

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Relativity.Compact.StaticSpherical module_import
IndisputableMonolith.Relativity.Geometry.Metric module_import

declarations in this module (11)

def PhaseFringeDensity L21
def LensingCorrection L27
theorem shadow_fringe_exists L33
theorem shadow_diameter_correction L55
theorem pbh_shadow_detectable L69
def H_ShadowFringeObservable L90
theorem shadow_fringe_wavelength_exists L102
theorem shadow_fringe_observable_trivial L111
def ShadowFringeFrequency L119
theorem shadow_fringe_frequency_identity L124
theorem fringe_frequency_grounded L128