3. Automation: discharging proof obligations🔗

Triptych separates three kinds of proof work:

1. Facts determined by the grammar and value clauses are generated and proved outright.

2. Repeated parser plumbing is handled by typed views, rule registries, and bounded tactics.

3. Format-specific semantic facts remain named premises.

Triptych discharges the first two categories; users supply the third because external code and domain semantics cannot be determined from the DSL.

1. 3.1. Generated proof interfaces
2. 3.2. Two parser registries
3. 3.3. Printer automation