alpha_seed_eq

formal source

  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
  60structure AlphaPrecisionCert where
  61  seed_from_geometry : alpha_seed = 4 * Real.pi * 11