deflectionAngle
plain-language theorem explainer
The definition assigns to each natural number k the real value phi raised to the power k as the characteristic deflection angle for the k-th gravitational lensing regime. Cosmologists working within Recognition Science would cite it when computing angles across the five canonical regimes on the phi-ladder. It is introduced as a direct noncomputable definition with no further reduction steps.
Claim. For each natural number $k$, the deflection angle in the $k$-th lensing regime equals $phi^k$, where $phi$ denotes the self-similar fixed point.
background
The module organizes gravitational lensing into five canonical regimes (weak, strong, microlensing, cluster, time-delay) that match configDim D = 5. Each regime receives a characteristic deflection angle placed on the phi-ladder, the sequence of successive powers of the self-similar fixed point phi forced at step T6 of the unified forcing chain. The module states that Lean status is zero sorry and zero axiom.
proof idea
This is a one-line definition that directly sets the deflection angle for regime k to phi^k.
why it matters
The definition populates the GravitationalLensingCert structure, which records the five regimes, the exact phi ratio between successive angles, and strict positivity of every angle. It supplies the explicit phi-ladder realization needed for the cosmology module and connects to the eight-tick octave and D = 3 from the forcing chain. Downstream theorems such as deflection_ratio recover the defining property phi exactly from this assignment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.