3. From reference decoder to verified scanner🔗

Triptych has two parsing implementations with different jobs. The archived reference decoder is small and proof-oriented. The scanner is the runtime engine used by every generated parser. The switch did not replace one trusted implementation with another: Triptych proves that the scanner returns exactly the reference result, then proves that the generated parser has the same public contract as before.

1. 3.1. Why the decoder came first
2. 3.2. The scanner
3. 3.3. A concrete Decimal trace
4. 3.4. Correctness of the switch
5. 3.5. One scan per generated parser
6. 3.6. Formal search-cost evidence
7. 3.7. Dependent continuation
8. 3.8. Tradeoff
9. 3.9. Measured evidence