[deanberris]

Built on #192, now merged. It is option 1 of the plan, pruning inside defeat cells with proofs, and the foundation for composing arguments. When several solas are joined into one dispute, whole positions share nothing, so most questions touch only a fraction of what a party holds.

What changes

• Components. A position falls into parts that share no claim. prepare_parts d for D writes out each party's clauses, and their components, found by union-find over the claims each clause mentions. It proves once for each party, checked by the kernel:
  • d.spec: the clauses are what conversion gives;
  • d.valid: the components partition them (Horn.Parts.valid). Each clause's claims lie in its component's mask, and no two masks meet.
• Pruned questions. Hint.prune sel inner asks only the components sel selects (Horn.askPruned), after one check that the question shares no claim with the rest. A question that touches every component is asked of the whole position, since pruning would drop nothing and only add its checks. Asked of a whole position, a pruned hint answers nothing, so the ordinary check stays a plain case split.
• Soundness. Horn.askPruned_sound proves the pruned answers are the whole position's, given its consistency, which every dispute node already proves (Dispute.consistent). Models of parts that share no claim combine. The proof is constructive and uses no axiom beyond propext and Quot.sound.
• Question oracles. To accept that, a defeat cell's theorems are now stated over any oracle that answers truly (Horn.AskSound, Horn.defeatsAsk?). defeatsWith? and defeatsBy? are instances of it, so every existing theorem and table stands unchanged.
• Proving a cell. Horn.defeats_iff_of_pruned proves a cell, and horn_certify finds the pruned hints (Horn.hintsPruned).
• Ported: sola fide's defeat table (both halves).

Measured

scripts/bench-ab.sh against #192's head, five interleaved rounds. The pruned tables exist only on this side, so they are compared with the prepared ones in the same run:

Table	Prepared	Pruned	Change	p	Peak memory
Sola fide, first half, 72 cells	5.95 s	5.38 s	−9.5%	0.008	60 → 36 MiB
Septuagint, 36 cells	1.05 s	1.26 s	+21%	0.15, not significant	12 → 4 MiB

So pruning pays on a large position and not on a small one, whose questions touch most of each party. Only sola fide's table is pruned; the smaller tables stay prepared. Ledger round 11 records both results, and docs/src/logic.md explains the method.

A regression CI caught, fixed

In the first version, a whole-position check recursed through a pruned hint's inner hint. That made the checker structural recursion over hints, which the kernel unfolds through brecOn on every question. CI's benchmark gate found the prepared Septuagint table 10% slower (p = 0.032).

The pruned hint now answers nothing when asked of a whole position. Seven interleaved rounds against #192's head then showed:

• the prepared Septuagint table +1.0% (p = 0.90);
• the certified one −3.5% (p = 0.26).

The first version had measured +4.7% and +8.2%.

Pins

The citation checks' pins in arguments/TestimonyArguments/Checks.lean move by exactly the new definitions: 2,338 → 2,370 and 1,633 → 1,634.

Gates

All run locally on this tree 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 merge from main brings in the squashed #192 and changes no file of this branch. No generated page changed.

🤖 Generated with Claude Code

https://claude.ai/code/session_01BC49XsbtehCbmJMavF1K5Q