LensingCorrection
plain-language theorem explainer
The definition supplies the ILG-adjusted deflection angle as the GR value scaled by one plus the fringe epsilon. Astrophysicists modeling black hole shadows in Recognition Science would cite this when computing observable fringe effects from the eight-tick cycle. The definition is a direct algebraic product with no further reduction.
Claim. $δθ_{ILG} = δθ_{GR} ⋅ (1 + ε_{fringe})$
background
The module formalizes ILG-corrected lensing predictions for black hole shadows with the goal of proving that the eight-tick cycle creates a detectable phase fringe at the event horizon. The eight-tick cycle is the fundamental evolution period of period 2^3 whose phases are given by kπ/4 for k = 0..7. The tick is the fundamental RS time quantum with value 1 in RS-native units.
proof idea
one-line wrapper that multiplies the general-relativity deflection angle by one plus the fringe correction term.
why it matters
It supplies the explicit correction factor arising from the eight-tick cycle (T7) for lensing predictions. The definition directly implements the modification to the deflection angle stated in the module objective and supports downstream shadow-diameter and fringe-observable statements in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.