`gap_correction`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.AlphaPrecision
domain: Constants
line: 50 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.AlphaPrecision on GitHub at line 50.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  47theorem curvature_correction_positive : 0 < curvature_correction := by
  48  unfold curvature_correction; exact zpow_pos phi_pos _
  49
  50noncomputable def gap_correction (w : ℝ) (seed : ℝ) : ℝ :=
  51  seed * Real.exp (-(w * Real.log phi) / seed)
  52
  53theorem gap_correction_positive (w seed : ℝ) (hw : 0 < w) (hs : 0 < seed) :
  54    0 < gap_correction w seed := by
  55  unfold gap_correction
  56  exact mul_pos hs (Real.exp_pos _)
  57
  58/-! ## Certificate -/
  59
  60structure AlphaPrecisionCert where
  61  seed_from_geometry : alpha_seed = 4 * Real.pi * 11
  62  seed_positive : 0 < alpha_seed
  63  curvature_positive : 0 < curvature_correction
  64  gap_positive : ∀ w seed, 0 < w → 0 < seed → 0 < gap_correction w seed
  65
  66theorem alpha_precision_cert_exists : Nonempty AlphaPrecisionCert :=
  67  ⟨{ seed_from_geometry := alpha_seed_eq
  68     seed_positive := alpha_seed_positive
  69     curvature_positive := curvature_correction_positive
  70     gap_positive := gap_correction_positive }⟩
  71
  72end
  73
  74end IndisputableMonolith.Constants.AlphaPrecision

papers checked against this theorem

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