escape

formal source

  49
  50private def boolToJson (b : Bool) : String := if b then "true" else "false"
  51
  52private def escape (s : String) : String :=
  53  -- Minimal escaping for JSON content used here
  54  s.replace "\"" "\\\""
  55
  56private def quote (s : String) : String := "\"" ++ escape s ++ "\""
  57
  58private def AuditItem.toJson (i : AuditItem) : String :=
  59  let fields := [
  60      "\"name\":" ++ quote i.name
  61    , "\"category\":" ++ quote i.category
  62    , "\"status\":" ++ quote i.status
  63    , "\"usesExternalInput\":" ++ boolToJson i.usesExternalInput
  64    ]
  65  let fields := match i.value with
  66    | some v => fields ++ ["\"value\":" ++ quote v]
  67    | none   => fields
  68  "{" ++ String.intercalate "," fields ++ "}"
  69
  70/--- Compute α^{-1} ≈ 4π·11 − (f_gap + δ_κ) using rationals.
  71  Use high-precision rationals: π ≈ 104348/33215 (|Δπ|≈3e−12), φ ≈ 161803399/100000000.
  72  Let f_gap = w8 * ln φ with w8 ≈ 2.488254397846. ln φ via ln(1 + 1/φ) alternating series. -/
  73def alphaInvValue : String :=
  74  IndisputableMonolith.URCGenerators.Numeric.alphaInvValueStr
  75
  76def auditItems : List AuditItem :=
  77  [ { name := "EightTickMinimality", category := "Timing", status := "Proven", usesExternalInput := false, value := some "1" }
  78  , { name := "Gap45_Delta_t_3_over_64", category := "Timing", status := "Proven", usesExternalInput := false, value := some "0.046875" }
  79  , { name := "UnitsInvariance", category := "Bridge", status := "Proven", usesExternalInput := false, value := some "1" }
  80  , { name := "KGate", category := "Bridge", status := "Proven", usesExternalInput := false, value := some "1" }
  81  , { name := "PlanckNormalization", category := "Identity", status := "Proven", usesExternalInput := false, value := some "0.31830988618" }
  82  , { name := "RSRealityMaster", category := "Bundle", status := "Proven", usesExternalInput := false, value := some "1" }