def definition def or abbrev

`beta_lin`

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

formal statement (Lean)

  43noncomputable def beta_lin  (C_lag α : ℝ) : ℝ := 1 + (1/20 : ℝ) * (C_lag * α)

Definition body.

  44
  45/-- Bound: if |C_lag·α| ≤ κ then |γ−1| ≤ (1/10) κ. -/

From the project-wide theorem graph. These declarations reference this one in their body.

beta_bound_small in IndisputableMonolith.Relativity.ILG.PPN decl_use
ppn_derivation_holds in IndisputableMonolith.Relativity.ILG.PPNDerive decl_use
PPNDerivationHolds in IndisputableMonolith.Relativity.ILG.PPNDerive decl_use

Lean names referenced from this declaration's body.