mkJson
plain-language theorem explainer
This definition constructs a JSON report string from a success boolean and error list for LNAL certificate outputs. It is invoked by the seven report generators in the same module covering compiler checks, cost ceilings, invariants, and related properties. The body directly builds a Json object with the two fields and applies pretty-printing.
Claim. A function that accepts a boolean success indicator and a list of error strings, then returns the pretty-printed JSON object whose 'ok' field holds the boolean and whose 'errors' field holds the array of strings.
background
The LNALReports module supplies JSON adapters for outputs from the LNAL compiler and its certificate generators. These reports cover invariants, opcode soundness, schedule neutrality, and SU3 masks. The module imports the LNAL compiler, JBudget, certificate modules, and Lean's Json library. The upstream map operation from RSNative.Core preserves measurement metadata under value transformations but is not invoked inside this definition.
proof idea
Direct definition that applies Lean.Json.obj to the pair of the ok boolean and the mapped error strings, then passes the result to Lean.Json.pretty.
why it matters
The definition supplies the common serialization step called by compiler_checks_report_json, cost_ceiling_report_json, lnal_invariants_report_json, and the four other report functions. It enables uniform machine-readable output for LNAL-derived checks that sit downstream of the forcing chain and J-uniqueness results. No open questions are attached to this helper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.