theorem proved term proof

`w8_value`

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

formal statement (Lean)

  18theorem w8_value : abs (w8_from_eight_tick - 2.490569275454) < 5e-6 := by

proof body

Term-mode proof.

  19  -- Follows from the verified interval bounds
  20  have h := w8_matches_certified
  21  rw [abs_lt]
  22  constructor <;> linarith
  23
  24end Constants
  25end IndisputableMonolith

depends on (5)

Lean names referenced from this declaration's body.

w8_from_eight_tick in IndisputableMonolith.Constants.GapWeight decl_use
w8_matches_certified in IndisputableMonolith.Constants.GapWeightNumericsScaffold decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
interval in IndisputableMonolith.Unification.SpacetimeEmergence decl_use