[deanberris]

The second item of the profiling plan after #189: the support and part-of tables were the last tables in a dispute the kernel still decided by searching.

What changes

• supportsBy? and partOfBy? (Testimony.Logic.Support) ask each question with a hint, as Horn.defeatsBy? does: a model or a refutation, checked by the kernel (Horn.clausesSatisfiableBy?), through Horn.satisfiableAppend?. Each party's clauses are converted once a cell. Before this, the part-of table converted a party's premises afresh for every premise it asked about.
• supports_iff_of_certified and partOf_iff_of_certified take the same hypothesis as the certified defeat tables: some index that tells atoms apart, and some hints that decide the cell. The soundness proofs go through checksBy, which hands questions their hints in order. Its lemmas show every check was asked of a premise with a valid hint, and every premise was asked about.
• supports? and partOf? are now supportsBy?/partOfBy? with no hints, the way defeats? is. Their theorems are unchanged in statement.
• horn_certify dispatches on both, with Horn.supportHints and Horn.partHints, which share entailsQuestion with the checker.
• Every dispute's support and part-of tables are now certified: seven in the arguments, and the grits example.
• docs/src/logic.md shows the certified proof.

Measured

scripts/bench-ab.sh origin/main --filter "144 cells", five interleaved rounds. The certified benchmarks exist only on this side, so they are compared with the searched ones, as in round 3:

Sola fide, 144 cells	Searched	Certified	Change	p
Part of	8.01 s, 131 MiB	5.00 s, 102 MiB	−38%	0.008
Supports	3.37 s, 17 MiB	1.99 s, 13 MiB	−41%	0.008

The searched forms, now the no-hint case, match main (supports +1.2%, p = 1.0; part of −0.9%, p = 0.55). Timed by hand, two runs each: SolaFide.Dispute elaborates in 41.5 s, against 47.6 s with its two tables searched. Recorded as ledger round 8 in docs/src/performance.md.

Merged with main after #189

#189 merged first. The merge resolves two conflicts:

• Ledger: rounds 7 and 8 now both appear, in order, each with its paragraph.
• Citation check's pin in arguments/TestimonyArguments/Checks.lean: now 2,326 definitions. That is main's 2,319 plus the 7 auxiliary definitions this PR's proofs add; no entries changed.

Gates

All run locally on the merged head 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.

No generated file changed: the docstrings that say how each table is computed name the engine as the certified defeat tables' docstrings already do.

---

Generated by Claude Code