Triptych

3.1. Why the decoder came first🔗

The reference Triptych.decode function enumerates possible prefix matches, keeps the complete parses, and returns the first one in source order. Its intermediate candidate lists make the grammar semantics and ordering policy easy to inspect. They are also useful in roundtrip, ambiguity, and capture-coherence proofs.

That transparency has a runtime cost. Variable-width terminals can produce many prefixes, and alternatives, optionals, and repetitions can multiply those candidates. Most candidates are allocated only to be discarded later.

The decoder now lives under Triptych/Archive/ReferenceDecoder.lean. The runtime scanner implementation does not import it. Proof modules import it explicitly as an executable reference semantics for verification, diagnostics, and differential benchmarks.