def
definition
def or abbrev
quote
show as:
view Lean formalization →
formal statement (Lean)
56private def quote (s : String) : String := "\"" ++ escape s ++ "\""
proof body
Definition body.
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. -/