alphaInvValueStr

proof body

Definition body.

  68  -- π and φ rationals
  69  let π_num : Int := 104348
  70  let π_den : Nat := 33215
  71  let φ_num : Int := 161803399
  72  let φ_den : Nat := 100000000
  73  -- y = 1/φ = φ_den / φ_num
  74  let y_num : Int := φ_den
  75  let y_den : Nat := φ_num.natAbs
  76  -- ln(1 + y) via alternating series up to N terms
  77  let N : Nat := 80
  78  -- Rational helpers
  79  let addR (aN : Int) (aD : Nat) (bN : Int) (bD : Nat) : (Int × Nat) :=
  80    (aN * bD + bN * (aD : Int), aD * bD)
  81  let negR (aN : Int) (aD : Nat) : (Int × Nat) := (-aN, aD)
  82  let mulR (aN : Int) (aD : Nat) (bN : Int) (bD : Nat) : (Int × Nat) :=
  83    (aN * bN, aD * bD)
  84  -- y^k / k
  85  let rec pow (baseN : Int) (baseD : Nat) (k : Nat) : (Int × Nat) :=
  86    match k with
  87    | 0 => (1, 1)
  88    | k+1 =>
  89      let (pn, pd) := pow baseN baseD k
  90      mulR pn pd baseN baseD
  91  let rec ln1p (k : Nat) (accN : Int) (accD : Nat) : (Int × Nat) :=
  92    if k = 0 then (accN, accD) else
  93      let (ykN, ykD) := pow y_num y_den k
  94      let termN : Int := ykN
  95      let termD : Nat := ykD * k
  96      let (termN, termD) := if k % 2 = 1 then (termN, termD) else negR termN termD
  97      let (n2, d2) := addR accN accD termN termD
  98      ln1p (k - 1) n2 d2
  99  let (lnφN, lnφD) := ln1p N 0 1
 100  -- f_gap = w8 * ln φ with w8 ≈ 2.488254397846 ≈ 2488254397846 / 10^12
 101  let w8N : Int := 2488254397846
 102  let w8D : Nat := 1000000000000
 103  let (gapN, gapD) := mulR lnφN lnφD w8N w8D
 104  -- δκ = -103 / (102 * π^5)
 105  let π5N : Int := π_num ^ 5
 106  let π5D : Nat := π_den ^ 5
 107  let δκN : Int := -103 * (π5D : Int)
 108  let δκD : Nat := 102 * π5N.natAbs
 109  -- f_gap + δκ
 110  let (sumN, sumD) := addR gapN gapD δκN δκD
 111  -- 4 * π * 11 = 44 * π
 112  let aN : Int := 44 * π_num
 113  let aD : Nat := π_den
 114  -- α^{-1} = 44π - (f_gap + δκ)
 115  let (negSumN, negSumD) := negR sumN sumD
 116  let (resN, resD) := addR aN aD negSumN negSumD
 117  NumFmt.ratToDecimal resN resD 12
 118
 119end Numeric
 120end URCGenerators
 121end IndisputableMonolith