# O-0176 witness pin

Pinned inputs:

- `lean/RHResearch/HeatBoundary.lean`
- `canon/witnesses/O-0176/HeatBoundary.lean`
- `canon/witnesses/O-0176/membership.json`
- `literature/2026-07-19-uniform-interior-certificate-barrier-primary-sources.md`
- `scratch/proof-system--o0176-field-redirecting-manuscript/dossiers.json`
- `scratch/proof-system--o0176-field-redirecting-manuscript/source_manifest.json`

The verifier:

1. requires the shared and pinned Lean files to be byte-identical;
2. compiles the metric, open-set, and arbitrary-interior
   accumulating-counterexample barriers and their quantitative
   specializations;
3. checks that both general theorems restrict common sufficiency to
   `Set.insert target (Set.range counterexample)`;
4. validates the exact M1--M4 schema;
5. validates seven primary-source program dossiers and two boundary
   controls against the manuscript route, including exact survivor
   lists and control rationales;
6. rejects any actual-paper membership verdict; and
7. requires every completion verdict to remain conditional on all
   stated admission clauses.

The manuscript route's independent verifier additionally pins fourteen
primary-source PDFs by SHA-256, checks displayed-statement anchors in
their extraction/OCR aids, enforces the outside-reader worksheet and
twenty-nine hostile attacks, rebuilds a warning-free PDF, and
cross-checks this canonical witness.

Rodgers--Tao's theorem supplies the analytic premise that every canonical
negative heat time is bad. The Lean witness verifies the full deduction
from an arbitrary named bad sequence and does not formalize that analytic
input.

Dependencies: Python 3 and the repository's frozen Lean/Mathlib
environment.

Run:

```bash
python3 canon/witnesses/O-0176/verify.py
```
