def
definition
examplesToJSON
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.CPM.ConstantsAudit on GitHub at line 226.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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" ++
244 " \"key_theorems\": [\n" ++
245 " \"cone_cmin_consistent\",\n" ++
246 " \"eight_tick_cmin_consistent\",\n" ++
247 " \"cone_cmin_numerical\",\n" ++
248 " \"eight_tick_cmin_numerical\",\n" ++
249 " \"all_examples_cproj_two_statement\",\n" ++
250 " \"coincidence_negligible\"\n" ++
251 " ]\n" ++
252 "}"
253
254end ConstantsAudit
255end CPM
256end IndisputableMonolith