  64    with π ≈ 104348/33215, φ ≈ 161803399/100000000,
  65    w8 = 2.488254397846 ≈ 2488254397846 / 10^12,
  66    δ_κ = −103/(102·π^5). Emits 12-decimal string. -/
  67def alphaInvValueStr : String :=
  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

papers checked against this theorem

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