ratToDecimal

formal source

  18  mkZeros deficit s
  19
  20/-- Render a rational q = n / m to a fixed d-decimal string. -/
  21def ratToDecimal (n : Int) (m : Nat) (d : Nat) : String :=
  22  let sign := if n < 0 then "-" else ""
  23  let nAbs : Nat := Int.natAbs n
  24  if m = 0 then sign ++ "NaN" else
  25  let scale := pow10 d
  26  let scaled : Nat := (nAbs * scale) / m
  27  let ip : Nat := scaled / scale
  28  let fp : Nat := scaled % scale
  29  let fpStr := padLeftZeros (toString fp) d
  30  sign ++ toString ip ++ (if d = 0 then "" else "." ++ fpStr)
  31
  32end NumFmt
  33
  34/-- Compute φ^k as a fixed-decimal string using a high-precision rational φ.
  35    Supports negative exponents by inversion. Deterministic and computable. -/
  36def phiPowValueStr (k : Int) (digits : Nat := 12) : String :=
  37  -- φ as a rational
  38  -- Use Source.txt canonical value φ ≈ 1.6180339887498948 with 16 fractional digits
  39  -- to reduce rounding error in comparator checks on φ^Δr ratios.
  40  let φ_num : Int := 16180339887498948
  41  let φ_den : Nat := 10000000000000000
  42  -- integer power helper for Int and Nat
  43  let rec powInt (a : Int) (n : Nat) : Int :=
  44    match n with
  45    | 0 => 1
  46    | n+1 => (powInt a n) * a
  47  let rec powNat (a : Nat) (n : Nat) : Nat :=
  48    match n with
  49    | 0 => 1
  50    | n+1 => (powNat a n) * a
  51  -- assemble numerator/denominator for φ^k