generateJSONReport
plain-language theorem explainer
generateJSONReport produces a fixed JSON string that aggregates verification results for CPM constants derived from Recognition Science invariants. An auditor invoking the lake executable for constants audit would cite this definition to obtain the machine-readable summary. The definition is a direct string concatenation embedding the output of constantsToJSON together with hardcoded consistency statuses and theorem names.
Claim. The definition that yields the audit report string is the concatenation producing the JSON object with fields for title, version, status, the constants array from constantsToJSON, examples, consistency checks (cone_cmin and eight_tick_cmin both PASSED), coincidence probability bound less than $10^{-12}$, and the list of key theorems.
background
The CPM Constants Audit module supplies machine-checkable verification of constants derived from Recognition Science invariants, including consistency checks and probability bounds for coincidental agreement. Upstream, the RS Native Units module establishes base units with tick and voxel equal to 1, speed of light c=1, coherence quantum coh=φ^{-5}, action quantum ħ=φ^{-5}, and the φ-ladder phiRung n = φ^n. The module proves cone_cmin_consistent (c_min equals the inverse product of K_net, C_proj, C_eng), cone_cmin_numerical (c_min=1/2), all_examples_cproj_two_statement (every example certificate has C_proj=2), and coincidence_negligible (probability < 10^{-10}).
proof idea
The definition is a direct string concatenation that embeds the result of constantsToJSON and lists the passed outcomes of cone_cmin_consistent, eight_tick_cmin_consistent, all_examples_cproj_two_statement, and coincidence_negligible together with the coincidence bound.
why it matters
This definition supplies the export mechanism for the audit report invoked by the lake executable. It aggregates the verification theorems confirming CPM constants satisfy Recognition Science invariants, including the eight-tick octave and cone projections with C_proj=2. No open questions are addressed; the declaration is purely an output formatter with zero downstream uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.