  41  if cert.ok then "OK: SU(3) braid mask (placeholder)"
  42  else s!"FAIL: {String.intercalate "; " cert.errors}"
  43
  44def previewNatArray (arr : Array Nat) (limit : Nat := 4) : String :=
  45  let previewVals := (arr.toList.take limit).map (fun n => toString n)
  46  let body := String.intercalate ", " previewVals
  47  if previewVals.isEmpty then "[]"
  48  else
  49    let ellipsis := if arr.size > previewVals.length then ", …" else ""
  50    "[" ++ body ++ ellipsis ++ "]"
  51
  52def jmonotone_report (src : String) : String :=
  53  let cert := JMonotoneCert.fromSource src
  54  if cert.ok then
  55    let preview := previewNatArray cert.deltaJ
  56    s!"OK: J-monotone per-window budget (ΔJ preview {preview})"
  57  else
  58    let base := if cert.errors.isEmpty then ["J-monotone violation"] else cert.errors
  59    let detail :=
  60      match cert.firstViolation? with
  61      | some idx =>
  62          let before := (cert.budgets.get? idx).getD 0
  63          let after := (cert.budgets.get? (idx + 1)).getD before
  64          s!" (window {idx / 8}, budget {before}→{after})"
  65      | none => ""
  66    s!"FAIL: {String.intercalate "; " base}{detail}"
  67
  68def units_kgate_report (src : String) : String :=
  69  let cert := UnitsKGateCert.fromSource src
  70  if cert.ok then "OK: Units quotient and K-gate audits"
  71  else s!"FAIL: {String.intercalate "; " cert.errors}"
  72
  73/-! Optional JSON artifact emission for per-source runs -/
  74

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.