Adds a fully inspectable, explicitly non-empirical verifier-optimization protocol unit: separated auditor-visible artifact and hidden adjudication witnesses; generated Lean type checks binding JSON labels to named witnesses; a configured typed structural linter with a declared vacuity blind spot; schema-valid exhaustive certificates; exact prefix-mean selection contrasts; and a selection-blind, citation-bounded auditor interface. The full nine-check gate passes locally, from a clean clone, and in hosted CI. This release does not report a model-behavior pilot, prevalence estimate, auditor result, or cross-domain transfer.