pow10

formal source

   7/-! Minimal numeric helpers for rational formatting (pure, computable). -/
   8namespace NumFmt
   9
  10def pow10 (d : Nat) : Nat := Nat.pow 10 d
  11
  12def padLeftZeros (s : String) (len : Nat) : String :=
  13  let deficit := if s.length ≥ len then 0 else len - s.length
  14  let rec mkZeros (n : Nat) (acc : String) : String :=
  15    match n with
  16    | 0 => acc
  17    | n+1 => mkZeros n ("0" ++ acc)
  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