5.1. Generalizing automation🔗

The current tactics remove parser decomposition and bookkeeping after format-specific semantic facts have been named. This track should broaden that reusable proof layer while keeping search bounded and leaving domain meaning explicit:

1. add terminating registry rules for more common parser combinators while keeping search limits explicit;

2. provide reusable semantic components for bounded integers, separators, and canonical numeric text;

3. extend derivation-based printer synthesis beyond the first signed-decimal shape; and

4. report missing registry facts and generated proof obligations directly at the failed goal.

Each extension should have a focused theorem-level test and at least one complete format proof. Success means fewer repeated proof steps and clearer failures, without changing the generated parser or allowing automation to manufacture semantic facts.