theorem proved term proof

`GW_constraint_framework`

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

formal statement (Lean)

  19theorem GW_constraint_framework :
  20  ∃ bound, bound = gw170817_bound ∧ bound < 0.001 := by

Term-mode proof.

  21  refine ⟨gw170817_bound, rfl, ?_⟩
  22  simp [gw170817_bound]
  23  norm_num
  24
  25end GW
  26end Relativity
  27end IndisputableMonolith

Lean names referenced from this declaration's body.