def
definition
def or abbrev
constantsToJSON
show as:
view Lean formalization →
formal statement (Lean)
213def constantsToJSON : String :=
proof body
Definition body.
214 let items := [" { \"name\": \"K_net (cone)\", \"value\": \"1\", \"source\": \"Intrinsic cone projection\", \"exact\": true }",
215 " { \"name\": \"K_net (eight-tick)\", \"value\": \"(9/7)^2 = 81/49\", \"source\": \"ε=1/8 covering\", \"exact\": true }",
216 " { \"name\": \"C_proj\", \"value\": \"2\", \"source\": \"Hermitian rank-one bound, J''(1)=1\", \"exact\": true }",
217 " { \"name\": \"C_eng\", \"value\": \"1\", \"source\": \"Standard normalization\", \"exact\": true }",
218 " { \"name\": \"C_disp\", \"value\": \"1\", \"source\": \"Dispersion bound\", \"exact\": true }",
219 " { \"name\": \"c_min (cone)\", \"value\": \"1/2\", \"source\": \"1/(1·2·1)\", \"exact\": true }",
220 " { \"name\": \"c_min (eight-tick)\", \"value\": \"49/162\", \"source\": \"1/((81/49)·2·1)\", \"exact\": true }",
221 " { \"name\": \"α (ILG)\", \"value\": \"(1-1/φ)/2\", \"source\": \"Self-similarity\", \"exact\": true }",
222 " { \"name\": \"φ\", \"value\": \"(1+√5)/2\", \"source\": \"x²=x+1 fixed point\", \"exact\": true }"]
223 "[\n" ++ String.intercalate ",\n" items ++ "\n]"
224
225/-- Generate a JSON array of example certificates. -/