def
definition
cost_ceiling_report_json
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.URCAdapters.LNALReports on GitHub at line 98.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
95 let cert := ScheduleNeutralityCert.fromSource src
96 mkJson cert.ok cert.errors
97
98def cost_ceiling_report_json (src : String) : String :=
99 let cert := CostCeilingCert.fromSource src
100 mkJson cert.ok cert.errors
101
102def su3_mask_report_json (src : String) : String :=
103 let _ := SU3MaskCert.fromSource src
104 -- SU3 mask is step-preservation; treat as ok with empty errors
105 mkJson true []
106
107def jmonotone_report_json (src : String) : String :=
108 let cert := JMonotoneCert.fromSource src
109 let violationSnapshot :=
110 match cert.firstViolation? with
111 | some idx =>
112 let before := (cert.budgets.get? idx).getD 0
113 let after := (cert.budgets.get? (idx + 1)).getD before
114 Lean.Json.obj [
115 ("index", Lean.Json.num idx),
116 ("window", Lean.Json.num (idx / 8)),
117 ("budget_before", Lean.Json.num before),
118 ("budget_after", Lean.Json.num after)
119 ]
120 | none => Lean.Json.null
121 Lean.Json.pretty <| Lean.Json.obj [
122 ("ok", Lean.Json.ofBool cert.ok),
123 ("errors", Lean.Json.arr (cert.errors.map Lean.Json.str)),
124 ("init_budget", Lean.Json.num cert.initBudget),
125 ("budgets", Lean.Json.arr (cert.budgets.toList.map (fun n => Lean.Json.num n))),
126 ("delta_j", Lean.Json.arr (cert.deltaJ.toList.map (fun n => Lean.Json.num n))),
127 ("violations", Lean.Json.arr (cert.violations.map (fun n => Lean.Json.num n))),
128 ("violation_snapshot", violationSnapshot)