H_ShadowFringeObservable
plain-language theorem explainer
This definition encodes the predicate asserting existence of a positive spatial wavelength for the phase fringe induced by the eight-tick cycle on a black hole shadow of radius Rs viewed at distance dist. Observational astrophysicists forecasting EHT-class data on small shadows would cite it to obtain the predicted modulation scale. The predicate is realized by direct construction of the wavelength as eight times the fundamental tick duration multiplied by the speed of light and the angular size Rs over dist.
Claim. The predicate $H(R_s, d, r)$ holds when there exists a positive real number $lambda$ satisfying $lambda = 8 tau_0 c (R_s / d)$, where $tau_0$ is the fundamental tick duration and $c$ is the speed of light in SI units.
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. Local notation introduces Rs as shadow radius, dist as observer distance, and res as instrumental resolution, though the predicate itself does not reference res.
proof idea
The definition first sets theta_Rs to Rs divided by dist and f_fringe to the reciprocal of eight times tau0. It then asserts existence of a positive lambda_fringe equal to c_SI divided by f_fringe times theta_Rs. This is a direct constructive definition with no external lemmas invoked.
why it matters
The declaration supplies the concrete empirical hypothesis for testing the eight-tick octave (T7) of the unified forcing chain through shadow observations. It supplies the wavelength scale referenced by sibling declarations such as shadow_fringe_wavelength_exists and fringe_frequency_grounded. The noted open question is the precise conversion from temporal frequency 1 over 8 tau0 to spatial wavelength, which requires further input from the geodesic structure near the horizon.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.