jmonotone_report
plain-language theorem explainer
This definition supplies a string report on J-monotonicity for an input source string by delegating to a certificate check. LNAL compiler users and URC adapter developers would invoke it to obtain diagnostic output during budget verification. The body builds a JMonotoneCert, branches on its ok flag, and formats either a preview of deltaJ values or a violation window with before/after budgets.
Claim. A function that accepts a source string and returns a report string: OK with a preview of the delta-J array when the per-window J-cost sequence is monotone, or FAIL listing errors and the first violating window index together with its budget transition.
background
The LNALReports module generates human-readable diagnostics for LNAL compiler outputs and URC adapters. J-monotonicity is the requirement that successive J-cost values (governed by the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)) remain non-decreasing across fixed-size windows. The upstream before relation from TimeEmergence supplies the temporal ordering of ledger snapshots used inside the certificate, while get projects values from vantage triples and previewNatArray truncates array output for readability.
proof idea
One-line wrapper that calls JMonotoneCert.fromSource on the input string. It then matches on the resulting ok flag: true yields an OK string containing the previewNatArray rendering of cert.deltaJ; false assembles base error messages and appends a formatted window detail extracted from budgets at the firstViolation index.
why it matters
The definition closes the reporting layer for J-budget invariants inside URCAdapters.LNALReports, supporting verification of the J-uniqueness step (T5) and the eight-tick octave structure in the forcing chain. It produces the concrete strings consumed by higher-level consent and certificate modules even though no direct used_by edges are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.