SU3MaskCert
plain-language theorem explainer
SU3MaskCert packages a certificate asserting that the SU(3) braid invariant is preserved under each wrapped LNAL transition. Compiler soundness teams cite it when confirming color symmetry across VM steps. The implementation reduces directly to the upstream preservation lemma via a one-line simpa application.
Claim. Let $LState$ be the wrapped LNAL state and $lStep$ the wrapped transition function. The structure $SU3MaskCert$ asserts that for every program $P$ and state $s$, if the SU(3) invariant holds at $s$ then it holds at $lStep(P,s)$.
background
LNAL invariants certificates bundle VM preservation and token unit bounds. The upstream $LState$ wraps the base LNAL state with a monotone window counter that increments on eight-tick boundaries for per-window J-budget tracking. The $lStep$ function executes the legacy small-step while updating the window index and optionally enabling v2 certificates. The local module setting treats these certificates as modular checks on invariant preservation.
proof idea
The verified property is witnessed by the theorem verified_any. It introduces the program and state, assumes the invariant, and applies simpa to reduce immediately to the upstream lemma lStep_preserves_su3.
why it matters
This certificate is consumed by su3_mask_report and su3_mask_report_json to emit human-readable and JSON status for the SU(3) mask check. It forms one component of the LNAL invariants bundle that supports step-wise VM preservation in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.