Spot-checkable artifacts (the PCP move)

Parent: recursive-harness

The most surprising softened-logic result, borrowed as a design principle. Classical proof-checking reads every line; the Probabilistically Checkable Proof (PCP) theorem shows proofs can be REWRITTEN into a robust format where any error contaminates a constant fraction of positions — so checking O(1) random spots catches a false proof with high probability. Verification collapses in cost not because the checker got smarter, but because the format was forced to amplify errors.

The move: constrain the artifact, not just the gate

The harness analogue: instead of only strengthening gates (more checks, more budget), the constitution can DEMAND delivery formats in which errors are loud and non-local:

• contracts/assertions woven through the code — an error violates nearby assertions, making locality globally visible;
• types everywhere — pervasive redundancy means a wrong value rarely type-checks along every path;
• tests interleaved with claims; invariant tables; checksums between pipeline stages;
• the ancient instance: double-entry bookkeeping — every transaction written twice so that corruption breaks a visible balance.

The principle: you cannot hide an error in a format that amplifies it.

The economics

This shifts cost from the VERIFIER (paid at every gate, recurring) to the FORMAT (paid once, at authoring). At fixed P×C the achievable α drops: cheap random spot-checks acquire global reach because the redundancy carries the error to wherever you look. It also feeds gate-subsumption (redundant structure = more static entailments between checks) and operationalizing-tolerances (spot-check pass-rate is a measurable gate with a computable α).

The harness inherits the accounting: a gate that relies on format-level redundancy is cheaper per call but requires the executor to sustain the redundancy — to maintain assertions, keep tests synchronized, preserve type coverage. This is not free: it is P×C debt incurred earlier, but compounded across all future spot-checks.

Honest caveat

Real PCP encodings are wildly impractical (polynomial blowups, algebraic encodings); the harness borrows the PRINCIPLE — error-amplifying redundancy — not the construction. And redundancy has its own cost: the executor must maintain it (more P×C at authoring), and stale redundancy (outdated comments/assertions) is negative signal. So the redundancy itself needs the build-cache invalidation discipline of gate-subsumption.

There is also a trap: redundancy can create false confidence. If assertions are weak (they only check obvious properties) or tests are sparse (they miss the edge case), then the harness reports high spot-check pass-rates while the actual α remains hidden. The format amplifies errors, yes — but only errors that interact with the redundancy. A failure mode outside the redundancy's scope is invisible.

One line

Don't just build better checkers — force artifacts into formats where errors cannot hide, and cheap checks become powerful.