shadow_diameter_correction
plain-language theorem explainer
The theorem states that a correction term delta_D to black hole shadow diameter equals (lambda_rec / Rs) times approximately 5.196 Rs. Astrophysicists testing ILG fringe effects on lensing would cite it when evaluating primordial black hole signals. The proof is a one-line wrapper that supplies the explicit witness and closes by reflexivity.
Claim. There exists a real number $δ_D$ such that $δ_D = (λ_{rec} / R_s) ⋅ (5.196 ⋅ R_s)$, given $R_s > 0$ and $λ_{rec} > 0$.
background
The module sets the local setting for ILG-corrected lensing predictions, with the objective to prove that the 8-tick cycle produces a detectable phase fringe at the event horizon. Upstream, lambda_rec is defined as the recognition wavelength √(ħ G / c³) from Bridge.DataCore and as ell0 in Constants, the fundamental length in the 8-tick cycle. The DOC_COMMENT identifies the correction as the ILG fringe factor ε_fringe ∼ λ_rec / R_s, negligible for supermassive holes such as M87* but potentially detectable for primordial ones.
proof idea
The proof is a one-line wrapper. It applies the 'use' tactic to construct the existential witness as the term (lambda_rec / Rs) * (5.196 * Rs), then closes with 'rfl' to discharge the equality by reflexivity. The body comments note that 5.196 approximates 3√3 and that full derivation awaits ILG geodesic integration.
why it matters
This declaration fills the module objective of formalizing shadow predictions under the 8-tick cycle, directly supporting the DOC_COMMENT claim that the correction becomes detectable for primordial black holes. It references the Recognition Science T7 eight-tick octave landmark through the phase-fringe mechanism. No downstream uses are recorded, leaving its role as an interface to later astrophysical tests.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.