`alphaInv_predicted_range_check`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.AlphaNumericsScaffold
domain: Constants
line: 18 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants.AlphaNumericsScaffold on GitHub at line 18.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  15noncomputable section
  16
  17/-- Check: derived α⁻¹ is approximately 137.036. -/
  18def alphaInv_predicted_range_check : Prop :=
  19  137.030 < alphaInv ∧ alphaInv < 137.039
  20
  21/-- Check: the 8-tick gap weight is approximately 2.49057. -/
  22theorem gap_weight_approx :
  23    2.490 < w8_from_eight_tick ∧ w8_from_eight_tick < 2.491 := by
  24  constructor
  25  · calc (2.490 : ℝ) < (2.490564399 : ℝ) := by norm_num
  26      _ < w8_from_eight_tick := Numerics.W8Bounds.w8_computed_gt
  27  · calc w8_from_eight_tick < (2.490572090 : ℝ) := Numerics.W8Bounds.w8_computed_lt
  28      _ < 2.491 := by norm_num
  29
  30end
  31end Constants
  32end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.