deflection_pos
plain-language theorem explainer
The theorem establishes that the deflection angle on the phi-ladder is strictly positive for every natural number k. Cosmologists assembling the five-regime lensing certificate in Recognition Science would cite it to close the positivity requirement. The proof is a one-line wrapper that applies pow_pos directly to the known positivity of phi.
Claim. For every natural number $k$, if the deflection angle is defined by $d(k) := phi^k$, then $d(k) > 0$.
background
In the Recognition Science module on gravitational lensing, the deflection angle is introduced as the explicit power $phi^k$ on the phi-ladder. The module organizes five canonical regimes (weak lensing, strong lensing, microlensing, cluster lensing, time-delay), each assigned a characteristic deflection on this ladder. The upstream definition supplies the concrete expression $deflectionAngle(k) := phi^k$ that the present theorem takes as input.
proof idea
The proof is a one-line wrapper that applies the lemma pow_pos to the positivity of phi.
why it matters
This result supplies the deflection_always_pos field required by gravitationalLensingCert, which packages the five regimes, the phi ratio, and strict positivity into a single certificate. It thereby completes the positivity leg of the RS lensing model and is referenced in downstream engineering certificates that reuse analogous positivity statements for trajectory shaping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.