`alpha_seed`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.AlphaPrecision on GitHub at line 29.

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

  26
  27noncomputable section
  28
  29noncomputable def alpha_seed : ℝ := 44 * Real.pi
  30
  31theorem alpha_seed_eq : alpha_seed = 4 * Real.pi * 11 := by
  32  unfold alpha_seed; ring
  33
  34theorem alpha_seed_positive : 0 < alpha_seed := by
  35  unfold alpha_seed; exact mul_pos (by norm_num) Real.pi_pos
  36
  37theorem alpha_seed_gt_132 : (132 : ℝ) < alpha_seed := by
  38  unfold alpha_seed
  39  nlinarith [Real.pi_gt_three]
  40
  41theorem alpha_seed_lt_176 : alpha_seed < (176 : ℝ) := by
  42  unfold alpha_seed
  43  nlinarith [Real.pi_lt_four]
  44
  45noncomputable def curvature_correction : ℝ := phi ^ (-(5 : ℤ))
  46
  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

papers checked against this theorem

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