theorem proved term proof

`abs_beta_running_pos`

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

formal statement (Lean)

  72theorem abs_beta_running_pos : 0 < abs beta_running := by

proof body

Term-mode proof.

  73  exact abs_pos.mpr (ne_of_lt beta_running_neg)
  74
  75/-- At r_ref = r, G_ratio(r, r) = 1 + |β|.
  76    The base (r/r) = 1, and 1^β = 1 for any β. -/

used by (4)

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

G_ratio_at_self_pos in IndisputableMonolith.Gravity.RunningG decl_use
G_ratio_mono in IndisputableMonolith.Gravity.RunningG decl_use
r_ref_exact_gt_r in IndisputableMonolith.Gravity.RunningG decl_use
r_ref_exact_pos in IndisputableMonolith.Gravity.RunningG decl_use

depends on (5)

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
beta_running in IndisputableMonolith.Gravity.RunningG decl_use
beta_running_neg in IndisputableMonolith.Gravity.RunningG decl_use
G_ratio in IndisputableMonolith.Gravity.RunningG decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use