cost_ceiling_report_json
plain-language theorem explainer
This definition generates a JSON string report for the cost ceiling certificate extracted from a given source string. Integrators of LNAL reports in URC adapter workflows invoke it to obtain serialized verification results. The body is a direct composition of certificate extraction from the source followed by JSON pretty-printing of the ok flag and error list.
Claim. For source string $s$, the map returns the pretty-printed JSON object containing boolean verification status and error list from the cost ceiling certificate of $s$.
background
The LNALReports module supplies JSON export functions for LNAL checks such as invariants and cost ceilings. CostCeilingCert is the structure that records whether net GIVE-REGIVE cost stays at most 4 per 8-tick window, storing an ok flag and error list. The upstream mkJson helper builds a Lean.Json object with fields for ok and errors.
proof idea
It is a one-line wrapper that applies CostCeilingCert.fromSource to the input string and then passes the resulting ok and errors fields to mkJson.
why it matters
This definition supplies the JSON serialization for cost ceiling reports inside the URC adapter layer. It operationalizes the cost constraint tied to the eight-tick octave. As a leaf definition with no downstream uses recorded, it closes the reporting interface for this check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.