def
definition
constantsToJSON
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.CPM.ConstantsAudit on GitHub at line 213.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
210 s!"\{\"example\": \"{e.example}\", \"Cproj\": 2.0, \"reference\": \"{e.reference}\"}"
211
212/-- Generate a JSON array of all verified constants. -/
213def constantsToJSON : String :=
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. -/
226def examplesToJSON : String :=
227 let items := [" { \"example\": \"ToyModel\", \"Cproj\": 2.0, \"status\": \"verified\" }"]
228 "[\n" ++ String.intercalate ",\n" items ++ "\n]"
229
230/-- Generate a complete JSON audit report. -/
231def generateJSONReport : String :=
232 "{\n" ++
233 " \"title\": \"CPM Constants Audit Report\",\n" ++
234 " \"version\": \"1.0\",\n" ++
235 " \"status\": \"VERIFIED\",\n" ++
236 " \"constants\": " ++ constantsToJSON ++ ",\n" ++
237 " \"examples\": " ++ examplesToJSON ++ ",\n" ++
238 " \"consistency_checks\": {\n" ++
239 " \"cone_cmin\": \"PASSED\",\n" ++
240 " \"eight_tick_cmin\": \"PASSED\",\n" ++
241 " \"all_examples_cproj_two\": \"PASSED\"\n" ++
242 " },\n" ++
243 " \"coincidence_probability\": \"< 10^(-12)\",\n" ++