1. Introduction: one grammar, a coherent parser stack
Triptych compiles a flat string grammar -- decimal, duration, datetime, or IP address --
into a readable specification, a verified parser, and the Lean theorems that
connect them. The generated parser is ordinary code with a small public signature such as
String → Option Int64. The proof layer establishes that it recognizes exactly the
specified language and returns exactly the specified denotation.
The compiler also emits typed views and structural derivation trees. These are the bridge between generated parsing and later proof work: users reason about fields, options, and lists instead of a raw capture map.