IndisputableMonolith.URCGenerators.Numeric

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace URCGenerators
   5namespace Numeric
   6
   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
  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
  52  let (num, den) : (Int × Nat) :=
  53    if k ≥ 0 then
  54      let kk : Nat := Int.toNat k
  55      (powInt φ_num kk, powNat φ_den kk)
  56    else
  57      let kk : Nat := Int.toNat (-k)
  58      -- invert: (φ_den^kk) / (φ_num^kk)
  59      ((powNat φ_den kk : Nat) |> fun n => (n : Int), (powInt φ_num kk).natAbs)
  60  NumFmt.ratToDecimal num den digits
  61
  62/-- φ-only curvature pipeline evaluator (deterministic, computable):
  63    α^{-1} ≈ 4π·11 − (w8·ln φ + δ_κ),
  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
  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
 122