jmonotone_report_json
plain-language theorem explainer
This definition produces a JSON report summarizing J-monotone certification results for an input source string. LNAL compiler integrators and URC adapter developers cite it to export certification snapshots for external review. The body derives a JMonotoneCert via fromSource, builds a violation snapshot from the first index when present, and assembles a pretty-printed object with status, sequences, and deltas.
Claim. The function maps a source string $s$ to a JSON string by first obtaining the J-monotone certificate from $s$, constructing a snapshot object from the first violation index (with preceding and following budgets) or null, then serializing an object with certification flag, error list, initial budget, budget sequence, delta-J sequence, violation indices, and the snapshot.
background
The URCAdapters.LNALReports module supplies JSON export utilities for LNAL compiler outputs. JMonotoneCert aggregates results from JBudget checks, exposing fields for success flag, error strings, initial budget, budget list, delta-J list, and violation indices. Upstream, the before relation from TimeEmergence orders snapshots by tick index. The map operation from RSNative.Core preserves measurement structure under value transformation. toList converts lepton mass ratios to a canonical triple, and get projects vantage triples to inside, act, or outside components.
proof idea
The definition calls fromSource to instantiate the certificate. It matches on firstViolation? to produce a JSON object holding index, window, and adjacent budgets or else null. It then builds the root object with ofBool for ok, mapped string array for errors, num for initBudget, mapped num arrays for budgets and deltaJ, num array for violations, and the snapshot, finally applying pretty.
why it matters
This supplies the serialization step for J-monotone reports in the LNAL pipeline, complementing sibling definitions such as lnal_invariants_report_json. It enables external auditing of J-cost monotonicity, consistent with J-uniqueness (T5) and the Recognition Composition Law in the forcing chain. No downstream theorems are recorded, leaving the report as an interface layer rather than a proved invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.