shadow_fringe_wavelength_exists
plain-language theorem explainer
The declaration shows that for any positive Schwarzschild radius Rs and distance dist a fringe wavelength exists and equals c_SI times 8 times tau0 times (Rs/dist). Workers modeling black-hole shadow fringes under the eight-tick cycle cite this existence result when separating definitional wavelength from empirical resolution questions. The proof is a direct one-line construction that supplies the explicit formula as witness to the existential quantifier.
Claim. For any $R_s>0$ and $d>0$ there exists a wavelength $λ$ such that $λ=c_{SI}⋅8⋅τ_0⋅(R_s/d)$, where $c_{SI}$ is the speed of light in SI units and $τ_0$ is the fundamental tick duration.
background
The module formalizes ILG-corrected lensing predictions for black-hole shadows with the explicit objective of showing that the eight-tick cycle produces a detectable phase fringe at the event horizon. Upstream, tau0 is defined as the fundamental tick duration (appearing in Constants, Derivation, and Compat layers) while c_SI is the exact SI value 299792458 m/s. The theorem therefore supplies a concrete spatial wavelength built from these two constants and the angular size theta_Rs = Rs/dist.
proof idea
The proof is a one-line wrapper that applies the 'use' tactic to the explicit term c_SI * 8 * tau0 * (Rs / dist), thereby discharging the existential quantifier without further rewriting or case analysis.
why it matters
The result fills the definitional step required by the module's goal of proving an 8-tick phase fringe at the horizon (T7 eight-tick octave). It supplies the wavelength whose observability is later assessed by sibling declarations such as shadow_fringe_observable_trivial. No downstream theorems yet depend on it, leaving open the empirical question of whether the constructed wavelength exceeds any given instrumental resolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.