5.2. Faster executable parsers🔗

The generated parser.lean names decodeView, computeValue, parse, and their contracts. These definitions are executable, but the current engine is designed first as a transparent reference decoder: it enumerates possible splits and chooses the first complete parse. Its performance has not yet been characterized as an optimized parser.

The reference decoder exposes the bounds that make this search total:

Triptych.DecodeBudget.referenceDepth counts grammar productions, Triptych.DecodeBudget.repetitionDepth is the input length, and Triptych.DecodeBudget.terminalPrefixCandidates is input length plus one. These are exact search limits, not a runtime complexity theorem: separate choices can multiply into many backtracking branches.

The current parser_benchmark smoke test repeatedly parses complete-graph inputs at orders 8 and 16. It detects gross execution failures but has no timing threshold. This track should:

1. establish reproducible benchmarks and performance thresholds;

2. specialize deterministic grammar fragments to avoid unnecessary split enumeration; and

3. prove that the optimized backend agrees with the same readable specification and parser contracts.

The reference decoder can then remain a simple executable oracle, while applications use the optimized backend.