Negative controls and the trust boundary
On this page · Permalink · Source line 330
A REJECTION HAS A PRECISE ROLE The current audit deliberately tested the following controls:
| Control | Why rejection matters |
|---|---|
| Illegal repeated wire | Legal gate constructors require distinct controls and target |
| Target-only cut reconstruction | A discrepancy can move to a data wire; completeness needs the entire coordinate family |
| False theorem | A false statement is not accepted merely because it has a theorem wrapper |
| Placeholder guard | The project rejects admitted or placeholder source constructs |
| False monomial degree | A two-occurrence monomial cannot satisfy the supplied length-at-most-one premise |
| False affine AND claim | The supplied degree-two proof has the wrong type for a degree-one target |
| False beta value | Complete safe detection for AND2 cannot have degree one |
| False betaStar bound | Optimization cannot erase the AND2 obstruction |
All eight controls were freshly rejected. They help check that the audit detects these specified errors. They are not additional positive mathematical results or an exhaustive attack on every possible checker defect. The separate positive four-corner theorem proves the semantic impossibility of an affine AND2 certificate; it is not the mechanism of that particular wrong-type negative test.
The bundled checker shares the Lean toolchain's trust boundary. It is not an independently implemented proof checker. The restored runtime archive was checked against the recorded combined hash. The runtime remains a separately supplied dependency.
Historical development failures, rejected negative controls, and successful current checks are retained as separate events in the evidence package.