IndisputableMonolith.Relativity.Lensing.ShadowPredictions
The ShadowPredictions module defines fringe density and related lensing quantities for shadow predictions in Recognition Science relativity. Researchers modeling black-hole observations or RS-derived interference patterns would cite these definitions. It assembles imported constants, metric, and spherical geometry into a set of definitions and existence statements with no internal proofs.
claim$ρ_{fringe}=sin(2π t/(8τ_0))$ where $t$ is the local tick coordinate and $τ_0$ is the fundamental RS time quantum; the module also introduces lensing corrections and fringe existence statements built on the static spherical metric.
background
The module resides in the Relativity.Lensing section and imports the RS time quantum $τ_0=1$ tick from Constants, the metric structure from Geometry.Metric, and static spherical solutions from Compact.StaticSpherical. It introduces PhaseFringeDensity as the interference fringe density at the event horizon boundary together with sibling objects such as LensingCorrection, ShadowFringeFrequency, and several existence lemmas. The factor of 8 in the sine argument aligns with the eight-tick octave period of the forcing chain.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
These definitions supply the fringe and shadow observables required by downstream lensing calculations in the Recognition Science framework. They connect the imported metric and spherical geometry to concrete predictions for fringe frequency and detectability, consistent with the eight-tick structure (T7) and the overall forcing chain from T0 to T8.
scope and limits
- Does not derive the underlying metric or static spherical solutions.
- Does not prove existence of event horizons or gravitational lensing.
- Does not compute numerical shadow diameters for specific masses.
- Does not address dynamical or non-spherical metrics.
depends on (3)
declarations in this module (11)
-
def
PhaseFringeDensity -
def
LensingCorrection -
theorem
shadow_fringe_exists -
theorem
shadow_diameter_correction -
theorem
pbh_shadow_detectable -
def
H_ShadowFringeObservable -
theorem
shadow_fringe_wavelength_exists -
theorem
shadow_fringe_observable_trivial -
def
ShadowFringeFrequency -
theorem
shadow_fringe_frequency_identity -
theorem
fringe_frequency_grounded