[deanberris]

Step 1 of the plan agreed after the relevance-pruning prototype: make each party's position a per-party artifact, rather than something every cell recomputes.

Why

A certified defeat cell converted both parties' positions to clauses. A party appears in a row and a column of its table, so a 12-party table converted each position 24 times. Measured in the kernel, conversion was about 14 ms of a sola fide cell.

What changes

• Horn.defeatsWith? decides a cell from given clauses. Horn.defeatsBy? is it with the clauses converted inside, so every existing theorem stands unchanged.
• Horn.defeats_iff_of_prepared proves a cell from each party's proof that its clauses are what conversion gives.
• prepare_clauses d for D (Testimony.Logic.Certificate) converts each party's position once, at elaboration time, and writes the clauses out. It also proves d.spec : ∀ i, clausesOf (D.node i).held = d i, which the kernel checks once per party: 0.35 s for sola fide's twelve.
• horn_certify finds a prepared cell's hints from the clauses themselves (Horn.hintsWith). defeatChecks and defeatsWith? no longer take the attacking package, which they never read.
• Every whole-dispute defeat table is ported: eleven in the arguments, two in the grits example, and the library's fixture. Hearing tables and Howell's article use other node functions or parameterised parties, so they are unchanged.
• The argument pages skip declarations with no source position. Those were generated by a command, as kernel machinery. Every generated page and PDF source is byte-identical to main's.

Measured

scripts/bench-ab.sh origin/main --filter table, five interleaved rounds, on the final code. The prepared benchmarks exist only on this side, so they are compared with the certified ones, as in rounds 3 and 8:

Table	Certified	Prepared	Change	p
Septuagint, 36 cells	1.61 s, 13 MiB	0.99 s, 11 MiB	−39%	0.008
Sola fide, first half, 72 cells	7.14 s, 70 MiB	5.44 s, 67 MiB	−24%	0.008

Every benchmark shared with main matched it ("NO CHANGE"). An earlier run, before hints were searched from the clauses, measured −39% and −12% (p = 0.016).

What this round also found

Ledger round 10 records two negative results, so nobody tries them again.

Pruning gave only 15% at this size. Each question was pruned to the components of a position it touches, found by union-find over the claims each clause mentions. That cut the clauses the kernel read to a third (6,671 of 19,800), but the time by only 15%.

A List.rec checker gained nothing in the tables. Cold micro-benchmarks suggested the kernel spends most of a model check in core's brecOn list functions and in Claim.ctorIdx: 7.6 ms against about 3 ms rewritten. So the checker was rewritten on List.rec, each function proved equal to core's, and the result was checked against this PR's head:

• A blowup. A lookup written as List.rec over Nat.rec made refutations exponential in the kernel: over 150 s for 32 synthetic formulas.
• Without that lookup, no gain. Neither table moved (prepared −5%, p = 0.15, and +2%), and one cell was 21% slower (p = 0.032).

Within a cell the kernel shares the work the cold measurement repeated. The rewrite was dropped, and clauses over constructor indices with it, since they rested on the same measurement.

Pins

The citation checks' definition counts move by exactly the new definitions:

• library fixture: 48 → 49;
• arguments: 2,319 → 2,325 and 1,622 → 1,633;
• examples: 76 → 78.

#190 and #191 each also move the first arguments pin and add a ledger row. Whichever merges later meets a trivial conflict in both.

Gates

All run locally and all pass:

• library: lake build, lake build TestimonyTools, lake lint, lake exe axiom-audit, scripts/kernel-replay.sh;
• arguments: build, lint, axiom audit, kernel replay, and bibgen/argtex/statusgen/argdoc --check;
• examples: build, lint, axiom audit, kernel replay, exampletex --check;
• testimony_lint.py and mdbook build.

The last commit changes only the ledger's prose; testimony_lint.py and mdbook build pass on it.

🤖 Generated with Claude Code

https://claude.ai/code/session_01BC49XsbtehCbmJMavF1K5Q