  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. -/

papers checked against this theorem

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