su3_mask_report_json
plain-language theorem explainer
The SU3 mask report JSON function maps an input source string to a report string. LNAL report generators cite it when producing standardized outputs for mask certifications. The body constructs the certificate object then delegates to the JSON builder with a success flag and empty error list.
Claim. The map sending a source string $src$ to the JSON string obtained by forming the SU3 mask certificate from $src$ and invoking the JSON constructor on the success indicator together with the empty error list.
background
The definition sits inside the LNAL reports adapter module. It relies on the SU3 mask certificate constructor and the mkJson helper also defined in the same file. Upstream the cellular automata step operation applies a local rule to each neighborhood of a tape, supplying the step-preservation property referenced in the comment. The module imports six supporting files that supply the certificate and ledger primitives used by the report suite.
proof idea
Definition, not theorem. The body binds the certificate constructed from the source (discarding the result), notes that the mask encodes step preservation, and returns the result of mkJson applied to true and the empty list.
why it matters
It belongs to the family of report generators that includes lnal invariants report json and compiler checks report json. The definition supplies a uniform JSON interface for SU3 mask claims that rest on step preservation, feeding the larger LNAL certification pipeline inside the Recognition Science adapters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.