3.8. Tradeoff🔗

The two implementations are intentionally retained:

• The reference decoder favors semantic transparency. It materializes candidates, which makes induction and ordering arguments direct, but is allocation-heavy.

• The scanner favors execution. It performs the same ordered search lazily and has a certified deterministic path, but its continuation structure is less pleasant as the primary proof semantics.

Keeping the decoder as an archived model gives the scanner a simple independent specification. Generated applications import and execute the scanner; proof and benchmark modules may import Triptych.Archive when they need the reference model or cost profile.