def definition def or abbrev

`lensing_param`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  32noncomputable def lensing_param (M b : ℝ) : ℝ := schwarzschild_radius M / b

proof body

Definition body.

  33
  34/-! ## Newtonian vs. GR Deflection -/
  35
  36/-- **Newtonian deflection** (treating photon as particle):
  37    θ_Newton = 2GM/(c²b) = r_s / b -/

depends on (5)

Lean names referenced from this declaration's body.

deflection in IndisputableMonolith.Engineering.AsteroidTrajectoryShaping decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
schwarzschild_radius in IndisputableMonolith.Gravity.GravitationalLensing decl_use
M in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use