cost_ceiling_report_json
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute the underlying cost ceiling verification logic.
- Does not validate or interpret the source string format.
- Does not handle exceptions raised during certificate creation.
formal statement (Lean)
98def cost_ceiling_report_json (src : String) : String :=
proof body
Definition body.
99 let cert := CostCeilingCert.fromSource src
100 mkJson cert.ok cert.errors
101