schedule_neutrality_report_json
plain-language theorem explainer
schedule_neutrality_report_json produces a JSON string that summarizes schedule neutrality verification for a given source. It builds a ScheduleNeutralityCert from the source and formats its ok flag plus error list via mkJson. The definition is a direct composition serving as a reporting adapter in the LNAL certification pipeline.
Claim. Let $f(src)$ be the string obtained by forming the schedule neutrality certificate $c$ from source $src$ and then serializing the pair $(c.ok, c.errors)$ into a pretty-printed JSON object with keys ``ok'' and ``errors''.
background
The LNALReports module supplies conversion utilities that turn internal certificates into JSON reports for external consumption. ScheduleNeutralityCert is the structure that aggregates schedule-related neutrality checks; it carries a boolean ok field and a list of error strings. The sibling mkJson definition builds a Lean.Json object containing exactly those two fields and renders it via pretty printing. Sibling reports in the same module cover compiler invariants, opcode soundness, and cost ceilings.
proof idea
One-line wrapper that applies ScheduleNeutralityCert.fromSource to the input string and then delegates to mkJson on the resulting ok flag and errors list.
why it matters
The definition supplies the JSON output layer for ScheduleNeutralityCert objects produced by the URCGenerators.LNALCerts module. It completes the reporting path for schedule neutrality within the LNAL adapter suite, allowing automated pipelines to consume verification status without direct Lean access. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.