einstein_radius_positive
plain-language theorem explainer
The declaration shows that the squared Einstein angle is positive whenever the mass and the three distances are positive. Gravitational lensing calculations in Recognition Science cite it to guarantee a geometrically real ring radius under aligned source-lens-observer conditions. The proof is a one-line term-mode reduction that unfolds the explicit formula and invokes the positivity tactic on the resulting product of positive reals.
Claim. If $M > 0$, $D_L > 0$, $D_S > 0$, and $D_{LS} > 0$, then $0 < 2M D_{LS}/(D_L D_S)$ in natural units where the squared Einstein angle is defined by that expression.
background
The module derives gravitational lensing observables from the RS action principle and the Schwarzschild metric in natural units. The squared Einstein angle is defined as einstein_angle_sq M DL DS DLS := schwarzschild_radius M * DLS / (DL * DS), where schwarzschild_radius M := 2 * M. Upstream, Time is the real numbers in RS-native units, while the Recognition structure M supplies the underlying cycle for the action principle.
proof idea
The proof unfolds einstein_angle_sq and schwarzschild_radius to obtain the explicit expression 2 * M * DLS / (DL * DS). It then applies the positivity tactic, which reduces the inequality to the product and quotient of the four positive hypotheses.
why it matters
This result guarantees a positive Einstein radius in the aligned lensing geometry, supporting the ring condition derived in RS_Gravitational_Lensing.tex. It sits downstream of the Schwarzschild radius definition and the Recognition structure M. Within the framework it confirms that the geometric optics limit yields observable lensing without sign issues.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.