Why a check behaves unlike everything else a turn knows, what a wrong assertion costs, and when to build the thing twice instead
WP3 gave an unattended chain a floor: a share of defects nothing downstream can see any more, because what a turn can see decays at λ per handoff. This paper asks what a check does to that floor, and the answer rests on one property.
A check does not attenuate. Everything else a turn knows about its ancestors arrives discounted by λk−1; an executable check arrives at full strength, because it is re-run rather than remembered. Two things follow. A defect inside its coverage contributes nothing to the floor at any gap. And the final turn's mistakes, which in WP3 had nobody after them, now have somebody.
That would end the matter if checks were free and correct. They are neither, and the premise this paper was handed says how: it is at least as hard to verify as to design. A check that covers more asserts more, and the assertions added last are the ambitious ones. So the gate needs an unsoundness u and a difficulty tail γ, and the defects a wrong assertion creates are certified as passing by the very mechanism that made them.
Density is then (1−c)(1+βc)·M + u·cγ, which gives a stopping point rather than a target: specify up to c* = (M / γu)1/(γ−1) and no further. It also gives an uncomfortable corollary. M falls as λ rises, so improving the briefing lowers the optimal amount of specification. Context and verification are substitutes.
When a sound check cannot be written, build the thing twice and treat disagreement as the detector. That has a floor too, and it is not p². Knight and Leveson rejected the independence assumption at the 99% level for human programmers, and one model sampled twice has less reason to differ than two universities do. The crossing between the two strategies is the generalizable pattern, and which side of it you are on is a measurement nobody here has made.
The pattern this paper was handed runs: break the problem into two efforts, have two turns
build verification tools for those efforts, have two successors build to pass them, and let an
integrator glue the result together. That is four stages of widths 1, 2, 2, 1, which is six
turns, which is standard in WP2's catalogue with lane
wiring.
Nothing about the graph is new, and that is the useful part. Every number WP2 computes
for standard carries over unchanged: depth 3, peak width 2, sink ken 0.5, an
automorphism group of order 2. What is new is what the turns are for, and WP2's nine
roles cannot express it, because those are read off degree and degree cannot tell a
specification from an implementation. Under lane wiring all four middle turns are
relays, whichever of the two duties they carry.
So a turn has a role, which its in- and out-degree force, and a duty, which the assignment chooses. The two are orthogonal, and a run is not described until both are stated.
One decision does move the roles, and finding that out is the reason this table is generated
from roles.mjs rather than typed. Give the builder an edge from the setup turn, so
it can read the original problem beside its check, and four of the six roles change: the
specifiers become delegates and the builders become funnels. What
reads like a preference in §8 is a different graph.
standard.
Roles are derived; duties are chosen.| Turn | Duty | Role · lanes only | Role · builder also briefed | Makes |
|---|---|---|---|---|
setup | split | principal | principal | two briefs, one per effort |
wave A · 1 | specify | relay | delegate | an executable check for effort 1 |
wave A · 2 | specify | relay | delegate | an executable check for effort 2 |
wave B · 1 | build | relay | funnel | effort 1, against check 1 |
wave B · 2 | build | relay | funnel | effort 2, against check 2 |
cleanup | integrate | integrate | integrate | the artefact, with both checks still running |
Every input a turn receives about its ancestors is discounted by λk−1, which is what produced WP3's floor. An executable check is the exception, and the reason is mechanical rather than clever: it is re-run, not remembered. A check written at turn 2 is exactly as sharp at turn 6 as it was at turn 3, because turn 6 does not recall it. Turn 6 executes it.
Two consequences, and the second is the one WP3's model had no way to produce.
Fagan established the practice of counting defect removal as a rate rather than describing it, which is the move this whole model depends on. What is added here is the observation that the rate has a gap argument, and that for a check the gap argument is constant.
That claim is directly testable and is H10. It rides on H9's seeded-defect machinery with one turn added, so it costs twelve turns on top of a run already budgeted. It also carries its own null: a check nothing trips is flat at zero, and the loop ledger's 59 of 89 turns at the probe ceiling is what that looks like from the outside.
An assertion that states the wrong thing does more damage than no assertion at all. It turns a would-be-correct implementation into a defect, and it marks that defect as passing. The failure is invisible to the mechanism that created it, which is why it needs a parameter of its own rather than a caveat.
The premise this paper was handed says what shape that parameter has. It is at least as hard to verify as to design, so a check covering more asserts more, and the assertions you add last are the ambitious ones you are likeliest to get wrong. Two numbers, then: u, the share of defects a complete specification would itself introduce, and γ, how much harder the last assertions are than the first. A third, β, covers what happens to the parts nobody specified, since the pattern instructs the implementer to optimise for the check. That is Goodhart's law arranged deliberately rather than stumbled into, and Manheim and Garrabrant's taxonomy names this variety regressional.
The gate-created term is superlinear whenever γ > 1, which gives an interior optimum and two statements worth arguing with.
The first assertions are always worth writing. At γ > 1 the derivative at c = 0 is −M, so a little coverage always pays. The question was never whether to check.
The comparative statics are all interpretable, and one of them is unwelcome. A better check-writer, meaning a lower u, should specify more. A steeper difficulty tail moves the stopping point without moving it monotonically, because a very large γ concentrates all the difficulty in the final assertion and lets you specify nearly everything. And M falls as λ rises, which gives the result this paper would least like to be true.
| λ | Ungated density M | Stop specifying at | Density there | Against no gate |
|---|---|---|---|---|
| 0.20 | 0.5868 | 0.9781 | 0.2999 | 0.5868 |
| 0.40 | 0.538 | 0.8966 | 0.2968 | 0.538 |
| 0.60 | 0.4796 | 0.7994 | 0.2879 | 0.4796 |
| 0.80 | 0.4171 | 0.6952 | 0.2721 | 0.4171 |
| 0.95 | 0.3732 | 0.6221 | 0.2572 | 0.3732 |
Improving the briefing reduces the optimal amount of specification. Context and verification are substitutes rather than complements: fix the handoff and some of your tests stop paying for themselves, because the chain would have caught those defects anyway. WP3's conclusion was that wiring is the first lever; this is the bill for that, and it says a programme that improves λ should expect to write fewer checks, not more.
The bare version of the comparison is worth stating on its own, because it is the premise turned into an inequality. D(1) = u and D(0) = M, so specifying everything beats specifying nothing exactly when u < M: you have to be likelier to get an assertion right than the chain is to leave the defect anyway.
Build the thing twice, independently, and treat disagreement as the detector. This spends a whole second implementation rather than one specification turn, and it asks nothing of anyone's ability to state what correct means in advance.
Its floor is not p². Knight and Leveson had
twenty-seven versions written independently from one specification and rejected the assumption
of independent failure at the 99% level. Eckhardt and Lee
give the model that replaces it: inputs vary in
difficulty, versions fail independently given the difficulty, and therefore fail together on the
hard ones. Correlation enters as the variance of that difficulty, and
agreementFloor() implements that model rather than the independence one, because
the independence one is known to be false.
| ρ | Two versions | Three versions | One version |
|---|---|---|---|
| 0.00 | 0.23 | 0.1103 | 0.4796 |
| 0.15 | 0.2675 | 0.1646 | 0.4796 |
| 0.30 | 0.3049 | 0.2195 | 0.4796 |
| 0.50 | 0.3548 | 0.2933 | 0.4796 |
| 0.80 | 0.4297 | 0.4048 | 0.4796 |
| 1.00 | 0.4796 | 0.4796 | 0.4796 |
That result was obtained from people at different universities working from a written specification. One model sampled twice has less reason to differ than they did, so ρ here should be expected to sit high rather than low, and treating agreement as confirmation is the error this table exists to price.
Putting the three on one scale answers the question this paper was asked. Each independent attempt carries the density an unattended effort carries, so what survives build-twice is the share both get wrong together, and the three rows become comparable.
So the generalizable pattern is not the six-turn shape. It is a choice between three strategies, decided by whether you can write a sound check more reliably than you can do the work twice.
The quantity that decides between the first two deserves a name, and it is the one this theory most needs and least has: the verification discount, the cost of checking an answer over the cost of producing one. When it is well under 1, spend width on definitions. When it approaches 1, a check that costs as much as the work has no advantage over a second attempt, and the honest move is the one the premise implies.
The page runs graph/gate.mjs directly, so this widget and the gate that tests it
cannot disagree.
This section needs JavaScript. Tables 2 and 3 carry the same arithmetic without it.
Fixing the shape and the duties still does not fix the run. Three wiring decisions remain, and the first version of this pattern left all three implicit, which would have made two runs of it incomparable.
| The profile does not settle | Which changes what the run measures |
|---|---|
| does the builder see the problem statement, or only the check | ONLY THE CHECK is maximum independence and makes coverage the whole specification. BOTH lets the builder notice an unsound assertion, and changes four of the six derived roles: the specifiers become delegates and the builders become funnels |
| does the builder run the check, or only the integrator | the builder running it is a tighter loop and also self-certification against a possibly-wrong check, which is the unsoundness term with the blindfold on |
| do the two lanes see each other`s checks | lane wiring says no, which preserves the pairing WP2 prices at a 40% saving but forgoes the cross-check that would measure unsoundness for free |
The first is structural rather than stylistic, as §1 noted: it changes four of the six derived roles, so two runs differing only in that answer are not two runs of one design.
The second is the sharpest for what gets measured. A builder that runs its own check has a tight loop and is also certifying itself against a possibly-wrong check, which is the u term with the blindfold on. A held-out scorer is the only construction that measures u at all, and H11 requires one.
| What it is | What it decides | What stands behind it | |
|---|---|---|---|
| v verification discount | cost to check an answer over cost to produce one | v well under 1 favours specify-first; v near 1 favours build-twice, because a check that costs as much as the work has no advantage over a second attempt | nothing. It is the quantity this theory most needs and the one nobody here has measured |
| u unsoundness at full coverage | the share of defects a COMPLETE specification would itself introduce by asserting the wrong thing | where to stop specifying, against the ungated density the chain would have left anyway | nothing, though it is measurable the same way as g: write checks against a seeded artefact and count wrong assertions |
| rho error correlation | how much two independent attempts fail on the same inputs | the floor under build-twice, which is p at rho = 1 and p^2 at rho = 0 | nothing here, but the assumption of independence was rejected for human programmers and there is no reason to expect better from one model sampled twice |
H10 measures the first claim, that a check does not attenuate, for twelve turns on top of H9. H11 puts the three strategies against each other over the same tasks, paired, at eighteen turns per task, and yields ρ as a by-product of running the build-twice arm at all. Both are in the register, and neither can start before H8 gives λ, since M is a function of it.
Everything above assigns duties to turns, and it is worth asking why the duties need turns at all. A single agent with a large budget can delegate: it spawns subordinates, hands each a piece, and collects the results. On the face of it that buys the same division of labour with none of the handoff loss this programme spends its time measuring.
It buys a different thing. A subordinate spawned inside a turn is briefed by that turn, from the context that turn already holds, so the fan-out happens at λ = 1 and nothing is attenuated. That is the good news and the bad news together. Sharing the context also shares the misreading of it: if the parent has mistaken what the task requires, every subordinate inherits the mistake, and their agreement is not evidence. Two turns that cannot see each other's reasoning can be wrong in two different ways. One turn's delegates mostly cannot.
So the turn boundary is an independence boundary rather than a work boundary, and the two kinds of division are not competitors:
| Divide by issue | Divide by group | |
|---|---|---|
| Mechanism | subagents inside one turn | a turn boundary |
| Context | λ = 1 — the parent hands over what it holds | λ < 1 — the successor gets an artefact, not a mind |
| Error correlation | high; one reading of the task, fanned out | lower; that is the whole purchase |
| Buys | throughput and breadth, cheaply | a second opinion that had no way to inherit the first |
| Costs | nothing this model prices | the attenuation of §1, paid once per hop |
Read that way, the six-turn shape is not six units of work. It is one unit of work and five purchases of independence, and the strategy comparison of §6 is a claim about how many of those purchases are worth their attenuation. A run that split by issue would want its pieces inside one turn; a run that splits by group is buying exactly what a subagent cannot supply.
The bank has already measured the contrast in miniature, with checks in place of turns. tb-001 split its two efforts by subject — one check for the estimator, one for the coverage property — and both killed every mutant either killed: redundancy 1.00, no detection diversity for the second effort. tb-002 split by kind, placing the second check against the checker rather than against another part of the same subject, and redundancy fell to 0.429. Same task size, same two efforts, and the division rule accounts for the difference.
That is a suggestive analogy rather than a measurement of the claim, so the claim is
registered as H12 and the harness carries a second shape to test it.
lab/runner.mjs accepts --shape solo: one turn, told it may delegate
freely, with the run's whole budget rather than one turn's share. Against standard on
the same task at equal total spend, the outcome is the redundancy between the two checks each arm
writes, which the bank scores for nothing. H12 is refuted if solo's checks are no more redundant
than standard's — in which case a turn boundary buys no independence, and the graph half of this
programme is measuring something that does not exist.
One reporting consequence follows immediately and is implemented rather than noted. A one-turn run has no handoffs, so it never had the opportunity to leak; its isolation audit returns inapplicable, not clean. A regime that was never tested must not be recorded as one that held.