cost_ceiling_report_json
plain-language theorem explainer
This definition builds a JSON string from an input source by constructing a CostCeilingCert and feeding its status fields to a JSON formatter. LNAL certificate pipelines and URC validation tools invoke it to emit machine-readable cost reports. The body is a direct two-step composition of the certificate constructor and the pretty-printer.
Claim. The map sending a source string to the pretty-printed JSON object whose fields are the Boolean verification flag and error list of the cost-ceiling certificate extracted from that source, where the certificate asserts that net GIVE−REGIVE stays at most 4 per 8-tick window.
background
CostCeilingCert is the structure whose ok field records whether the net GIVE−REGIVE cost respects the bound of 4 units inside every 8-tick window; its errors field collects diagnostic strings. The helper mkJson assembles an arbitrary Boolean and string list into a Lean.Json object with keys "ok" and "errors" and returns its pretty-printed form.
The definition sits inside the URCAdapters.LNALReports module, whose purpose is to expose JSON adapters for LNAL compiler and certificate artifacts. It imports CostCeilingCert from the LNALCerts generator and the mkJson formatter defined earlier in the same file.
proof idea
One-line wrapper that applies CostCeilingCert.fromSource to the source string and immediately passes the resulting ok and errors fields to mkJson.
why it matters
The definition supplies the JSON serialization layer for the cost-ceiling certificate that enforces the eight-tick octave bound (T7) inside the forcing chain. It belongs to the URC adapter suite that converts internal LNAL certificates into consumable reports for downstream consent and verification steps. No used-by edges are recorded, indicating it functions as a terminal reporting utility rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.