Reproducibility protocol

For every executable supplement:

1. pin the source and all nonstandard dependencies;

2. distinguish an author’s original artifact from a local port;

3. state whether the run checks parsing, typing, reduction, testing, extraction, or a mechanized proof;

4. include one small expected-success and one expected-failure case;

5. record any axioms, admitted lemmas, unsafe flags, or unchecked termination, positivity, productivity, and universe conditions;

6. keep benchmark or implementation evidence separate from metatheory.