From 9aaae49755b2f7c452ff3f016a2bb3ca61dcec0b Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 2 Nov 2026 07:11:49 +0000
Subject: [PATCH 1/4] Convert each party's position to clauses once per table

A certified defeat cell converted both parties' positions to clauses, so a
party in a row and a column of cells was converted once for every cell.
`prepare_clauses` converts each party's position once, writes the clauses
out, and has the kernel check, once per party, that they are what the
conversion gives; every cell reads them. `Horn.defeatsWith?` decides a cell
from given clauses, `Horn.defeatsBy?` is it with the clauses converted, and
`Horn.defeats_iff_of_prepared` takes each party's proof. Every whole-dispute
defeat table is ported: eleven in the arguments, two in the grits example,
and the library's fixture.

Five interleaved rounds, certified against prepared: the Septuagint's table
1.52 s to 0.93 s (-39%, p = 0.008), half of sola fide's 6.31 s to 5.53 s
(-12%, p = 0.016); preparing sola fide's parties costs 0.35 s, once. Ledger
round 10, with the measurement that set component pruning after a faster
checker; the citation checks' pins move by the new definitions.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BC49XsbtehCbmJMavF1K5Q
---
 CLAUDE.md                                     |  2 +-
 Testimony/Checks/Citations.lean               |  2 +-
 Testimony/Checks/Fixture.lean                 |  5 +-
 Testimony/Logic/Certificate.lean              | 97 ++++++++++++++++++-
 Testimony/Logic/Horn.lean                     | 54 ++++++++---
 .../BornOfAVirgin/Dispute.lean                |  5 +-
 .../BornOfAVirgin/Dispute/Genesis.lean        |  6 +-
 .../BornOfAVirgin/Dispute/Matthew.lean        |  6 +-
 .../Dispute/Protoevangelium.lean              |  6 +-
 .../BornOfAVirgin/Dispute/Septuagint.lean     |  7 +-
 .../BornOfAVirgin/Dispute/Wegner.lean         |  6 +-
 arguments/TestimonyArguments/Checks.lean      |  4 +-
 .../TestimonyArguments/SolaFide/Dispute.lean  |  8 +-
 .../TestimonyArguments/SolaFide/James.lean    |  5 +-
 .../SolaFide/JesusWords.lean                  |  5 +-
 .../SolaScriptura/Dispute.lean                |  5 +-
 .../SpiritBaptism/Dispute.lean                |  5 +-
 arguments/bench/Engine.lean                   | 17 ++++
 docs/src/logic.md                             | 12 ++-
 docs/src/performance.md                       | 27 ++++++
 examples/TestimonyExamples/Checks.lean        |  2 +-
 examples/TestimonyExamples/Grits/Dispute.lean | 11 ++-
 22 files changed, 252 insertions(+), 45 deletions(-)

diff --git a/CLAUDE.md b/CLAUDE.md
index 59f4ac5..9ebf1e1 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -141,7 +141,7 @@ back to `sorryAx` — that produces a *successful build*.
 | `Testimony/Bib/` | `Core` types, `Attr` registry attribute, `Works` entries, `Render`, `Registry` guards |
 | `Testimony/Provenance.lean` | `Reference`, `Source`, `Tradition`, `Confidence` |
 | `Testimony/Intertext.lean` | Typed relations between passages |
-| `Testimony/Logic/` | `Basic` formula, `Notation` (`p`/`notP`), `Entail` + countermodels + `Independent`, `Package` arguments + manifests, `Line` lines of reason, `Tactic` (`establish`, Horn-only, and `establish_by_search`/`refute_with`/`satisfied_by`/`leaves_open`/`granted`), `Framework` Dung semantics (grounded, preferred), `Dispute` packages as its nodes, defeat derived from entailment and cited confidence, `Horn` the decision procedure that computes a dispute's defeat table, `Certificate` the search that finds what the kernel checks of it (`horn_certify`), `Solver` the verified solver that computes its verdicts, `Witness` the checked reasons they are stated with, `Verdict` a verdict and its witness as one declaration, rendered from the witness, `Support` one position lending another a premise, `Map` a dispute drawn with its defeats, supports and the attacks support implies, `Because` why one package stands against another, at a checked crux, `Burden` the minimal sets of readings an opponent must reject, complete, `Dilemma` every reading of a rival's ambiguous claim, each answered, `Aif` every dispute as an AIF graph, checked against AIF's Definition 1.1 |
+| `Testimony/Logic/` | `Basic` formula, `Notation` (`p`/`notP`), `Entail` + countermodels + `Independent`, `Package` arguments + manifests, `Line` lines of reason, `Tactic` (`establish`, Horn-only, and `establish_by_search`/`refute_with`/`satisfied_by`/`leaves_open`/`granted`), `Framework` Dung semantics (grounded, preferred), `Dispute` packages as its nodes, defeat derived from entailment and cited confidence, `Horn` the decision procedure that computes a dispute's defeat table, `Certificate` the search that finds what the kernel checks of it (`horn_certify`), and each party's position converted once per table (`prepare_clauses`), `Solver` the verified solver that computes its verdicts, `Witness` the checked reasons they are stated with, `Verdict` a verdict and its witness as one declaration, rendered from the witness, `Support` one position lending another a premise, `Map` a dispute drawn with its defeats, supports and the attacks support implies, `Because` why one package stands against another, at a checked crux, `Burden` the minimal sets of readings an opponent must reject, complete, `Dilemma` every reading of a rival's ambiguous claim, each answered, `Aif` every dispute as an AIF graph, checked against AIF's Definition 1.1 |
 | `Testimony/Argument.lean` | Criteria, definitions, `Satisfies`, `People` |
 | `Testimony/Semantics/` | `Upper` (DOLCE's categories, each with its BFO counterpart), `Vocabulary`, `Grammar` (a claim's meaning as a term, over concepts, words and particulars), `Ontology` (a meaning taken apart and read under definitions), `Meaning` (`HasMeanings`, `HasJoins`), `Discourse` |
 | `Testimony/Ontology/` | Articles that derive what the vocabulary's words mean — definitions with sources, each shown at work — naming no argument (`Relations`; `Time`, an occurrence lasts one length of time; `Kinds`, each concept's category, or why it has none); `Search`, the generic queries; `Shared`, the definitions every join is read under |
diff --git a/Testimony/Checks/Citations.lean b/Testimony/Checks/Citations.lean
index 195091b..70ef471 100644
--- a/Testimony/Checks/Citations.lean
+++ b/Testimony/Checks/Citations.lean
@@ -84,7 +84,7 @@ syntax (name := checkCitationsCmd) "#check_citations" " under " ident : command
 elab_rules : command
   | `(#check_citations under $root) => checkCitations [root.getId]
 
-/-- info: every entry is a tagged definition, and every key names one: 48 definitions, 15 entries -/
+/-- info: every entry is a tagged definition, and every key names one: 49 definitions, 15 entries -/
 #guard_msgs in
 #check_citations under Testimony.Checks.Fixture
 
diff --git a/Testimony/Checks/Fixture.lean b/Testimony/Checks/Fixture.lean
index 5e4057c..ecaf67e 100644
--- a/Testimony/Checks/Fixture.lean
+++ b/Testimony/Checks/Fixture.lean
@@ -216,10 +216,13 @@ theorem node_strength : ∀ i, (node i).strength = strength i
   | .minutes => by decide
   | .clock => by decide
 
+prepare_clauses disputeClauses for dispute
+
 /-- Who defeats whom, computed and checked by the kernel. -/
 theorem dispute_defeats : ∀ i j, dispute.defeats i j ↔ defeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (node_strength i) (node_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (node_strength i) (node_strength j)
+    (disputeClauses.spec i) (disputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute, in the form the solver and the AIF check read. -/
diff --git a/Testimony/Logic/Certificate.lean b/Testimony/Logic/Certificate.lean
index 339fbc4..a370800 100644
--- a/Testimony/Logic/Certificate.lean
+++ b/Testimony/Logic/Certificate.lean
@@ -182,6 +182,8 @@ def searchFor (index lhs : Expr) : MetaM Expr := do
   let args := lhs.getAppArgs
   if lhs.isAppOfArity ``Horn.defeatsBy? 9 then
     mkAppOptM ``Horn.hintsFor #[args[0]!, args[1]!, args[2]!, index, args[5]!, args[6]!]
+  else if lhs.isAppOfArity ``Horn.defeatsWith? 10 then
+    mkAppOptM ``Horn.hintsFor #[args[0]!, args[1]!, none, index, args[6]!, args[7]!]
   else if lhs.isAppOfArity ``Dissent.findingsBy? 6 then
     mkAppOptM ``Horn.findingsHints #[args[0]!, args[1]!, args[2]!, index, args[5]!]
   else if lhs.isAppOfArity ``Horn.satisfiableAppend? 6 then
@@ -190,8 +192,8 @@ def searchFor (index lhs : Expr) : MetaM Expr := do
       throwError "horn_certify: expected the clauses of a list, got{indentExpr base}"
     mkAppOptM ``Horn.hintsAppend #[args[0]!, args[1]!, index, base.appArg!, args[5]!]
   else
-    throwError "horn_certify: expected `Horn.defeatsBy? …`, `Dissent.findingsBy? …` or \
-      `Horn.satisfiableAppend? …`, got{indentExpr lhs}"
+    throwError "horn_certify: expected `Horn.defeatsBy? …`, `Horn.defeatsWith? …`, \
+      `Dissent.findingsBy? …` or `Horn.satisfiableAppend? …`, got{indentExpr lhs}"
 
 /-- Prove `∃ index, Function.Injective index ∧ ∃ hints, decision index hints … = v`,
 for a defeat cell or a dissent's findings, or `∃ index hints, … = v` for a
@@ -228,4 +230,95 @@ elab (name := hornCertify) "horn_certify" : tactic => do
   goal.assign <| mkApp4 (.const ``Exists.intro us) indexTy p index body
   replaceMainGoal []
 
+/-! ### Each party's clauses, once
+
+A defeat table asks every cell about two parties' positions as clauses, and
+converting a position is most of what a cell costs the kernel. `prepare_clauses`
+converts each party's position once, at elaboration time, writes the result as a
+literal, and proves for each party that the literal is what the conversion
+gives: the kernel evaluates the conversion once per party, and every cell reads
+the literal. -/
+
+/-- A list of clauses as a term, each atom the constructor at its index. -/
+def clausesExpr (α : Expr) (ctors : Array Name) (cs : List (List ℕ × List ℕ)) :
+    MetaM Expr := do
+  let atom (k : ℕ) : MetaM Expr := do
+    let some c := ctors[k]? | throwError "prepare_clauses: no constructor {k}"
+    return mkConst c
+  let clauseTy := mkApp (mkConst ``Horn.Clause) α
+  let mut out : Array Expr := #[]
+  for (body, heads) in cs do
+    let b ← body.mapM atom
+    let h ← heads.mapM atom
+    out := out.push (mkApp3 (mkConst ``Horn.Clause.mk) α (← mkListLit α b) (← mkListLit α h))
+  mkListLit clauseTy out.toList
+
+/-- `prepare_clauses name for d`: define `name : ι → Option (List (Clause α))`,
+each party's position as clauses, written out, and prove `name_spec : ∀ i,
+clausesOf (d.node i).held = name i`, which the kernel checks once per party. -/
+elab "prepare_clauses " name:ident " for " d:term : command => Command.liftTermElabM do
+  let d ← Term.elabTerm d none
+  Term.synthesizeSyntheticMVarsNoPostponing
+  let d ← instantiateMVars d
+  let dTy ← whnfR (← inferType d)
+  let #[α, inst, ι] := dTy.getAppArgs | throwError "prepare_clauses: not a dispute"
+  let enumCtors (ty : Expr) : MetaM (Name × Array Name) := do
+    let .const n [] := ty | throwError "prepare_clauses: {ty} is not an enumeration"
+    let some (.inductInfo i) := (← getEnv).find? n | throwError "prepare_clauses: {n}?"
+    return (n, i.ctors.toArray)
+  let (ιName, parties) ← enumCtors ι
+  let (_, atoms) ← enumCtors α
+  let αName := α.constName!
+  let optTy := mkApp (mkConst ``Option [Level.zero]) (mkApp (mkConst ``List [Level.zero])
+    (mkApp (mkConst ``Horn.Clause) α))
+  let mut lits : Array Expr := #[]
+  for c in parties do
+    let held := mkApp3 (mkConst ``ArgumentPackage.held) α inst
+      (mkApp (mkApp4 (mkConst ``Dispute.node) α inst ι d) (mkConst c))
+    let cl := mkApp2 (mkConst ``Horn.clausesOf) α held
+    -- Evaluated as constructor indices, a type the evaluator knows.
+    let idx := mkConst (αName ++ `ctorIdx)
+    let toIdx ← withLocalDeclD `c (mkApp (mkConst ``Horn.Clause) α) fun c => do
+      let body ← mkAppM ``List.map #[idx, ← mkAppM ``Horn.Clause.body #[c]]
+      let heads ← mkAppM ``List.map #[idx, ← mkAppM ``Horn.Clause.heads #[c]]
+      mkLambdaFVars #[c] (← mkAppM ``Prod.mk #[body, heads])
+    let mapClauses ← mkAppM ``List.map #[toIdx]
+    let asIdx ← mkAppM ``Option.map #[mapClauses, cl]
+    let v ← unsafe evalExpr (Option (List (List ℕ × List ℕ)))
+      (← inferType asIdx) asIdx
+    let lit ← match v with
+      | some cs => pure (mkApp2 (mkConst ``Option.some [Level.zero])
+          (mkApp (mkConst ``List [Level.zero]) (mkApp (mkConst ``Horn.Clause) α))
+          (← clausesExpr α atoms cs))
+      | none => pure (mkApp (mkConst ``Option.none [Level.zero])
+          (mkApp (mkConst ``List [Level.zero]) (mkApp (mkConst ``Horn.Clause) α)))
+    lits := lits.push lit
+  let defName := (← getCurrNamespace) ++ name.getId
+  let casesOn (motive : Expr) (minors : Array Expr) (i : Expr) (lvl : Level) : Expr :=
+    mkAppN (mkConst (ιName ++ `casesOn) [lvl]) (#[motive, i] ++ minors)
+  let body := Expr.lam `i ι (casesOn (.lam `_ ι optTy .default) lits (.bvar 0) Level.one) .default
+  addAndCompile <| .defnDecl {
+    name := defName, levelParams := [], type := .forallE `i ι optTy .default, value := body,
+    hints := .abbrev, safety := .safe }
+  addDocStringCore defName s!"Each party's position in `{d}`, as clauses, written out once \
+    so that every cell of its defeat table reads them rather than converting the position \
+    again. Generated by `prepare_clauses`; `{defName ++ `spec}` proves it."
+  -- For each party, the conversion reduces to its literal: `Eq.refl`, checked by the kernel.
+  let specTy ← withLocalDeclD `i ι fun i => do
+    let held := mkApp3 (mkConst ``ArgumentPackage.held) α inst
+      (mkApp (mkApp4 (mkConst ``Dispute.node) α inst ι d) i)
+    mkForallFVars #[i] (← mkEq (mkApp2 (mkConst ``Horn.clausesOf) α held)
+      (mkApp (mkConst defName) i))
+  let motive ← withLocalDeclD `i ι fun i => do
+    let held := mkApp3 (mkConst ``ArgumentPackage.held) α inst
+      (mkApp (mkApp4 (mkConst ``Dispute.node) α inst ι d) i)
+    mkLambdaFVars #[i] (← mkEq (mkApp2 (mkConst ``Horn.clausesOf) α held)
+      (mkApp (mkConst defName) i))
+  let proofs ← lits.mapM fun lit => mkEqRefl lit
+  let specVal := Expr.lam `i ι (casesOn motive proofs (.bvar 0) Level.zero) .default
+  addDecl <| .thmDecl {
+    name := defName ++ `spec, levelParams := [], type := specTy, value := specVal }
+  addDocStringCore (defName ++ `spec) s!"Each party's clauses in `{defName}` are what \
+    converting its position gives, checked by the kernel once for each party."
+
 end Testimony.Logic.Certificate
diff --git a/Testimony/Logic/Horn.lean b/Testimony/Logic/Horn.lean
index ade29c4..216354c 100644
--- a/Testimony/Logic/Horn.lean
+++ b/Testimony/Logic/Horn.lean
@@ -887,11 +887,10 @@ def stepRebuts? (index : α → ℕ) (hb ha : Hint) (ca cb : Option (List (Claus
     else none
 
 /-- Every way `a` could defeat `b`: the rebuttal, each premise of `b`, and each
-claim `b`'s steps deliver, each with its hint. -/
-def defeatChecks (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage α) (s t : ℕ) :
-    List (Option Bool) :=
-  let ca := clausesOf a.held
-  let cb := clausesOf b.held
+claim `b`'s steps deliver, each with its hint, given the clauses of what each
+holds, `ca` and `cb`. -/
+def defeatChecks (index : α → ℕ) (hints : List Hint) (ca cb : Option (List (Clause α)))
+    (a b : ArgumentPackage α) (s t : ℕ) : List (Option Bool) :=
   let n := b.premises.length
   (rebuts? index (hintAt hints 0) b ca s t ::
     b.premises.zipIdx.map fun (φ, i) => undermines? index (hintAt hints (i + 1)) b ca s φ) ++
@@ -899,17 +898,25 @@ def defeatChecks (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage
       stepRebuts? index (hintAt hints (n + 1 + 2 * i)) (hintAt hints (n + 2 + 2 * i)) ca cb s t
         q.2
 
-/-- Whether `a`, of strength `s`, defeats `b`, of strength `t`, from hints:
-`some true` if any way succeeds, `some false` if every way is shown to fail,
-`none` if some check was on a formula without clauses, or its hint did not
-check, and none succeeded. The checks are made once. -/
-def defeatsBy? (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage α) (s t : ℕ) :
-    Option Bool :=
-  let checks := defeatChecks index hints a b s t
+/-- Whether `a`, of strength `s`, defeats `b`, of strength `t`, from hints, given
+the clauses of what each holds: `some true` if any way succeeds, `some false` if
+every way is shown to fail, `none` if some check was on a formula without
+clauses, or its hint did not check, and none succeeded. The checks are made
+once. A table converts each party's position once, not once for every cell it
+appears in (`defeats_iff_of_prepared`). -/
+def defeatsWith? (index : α → ℕ) (hints : List Hint) (ca cb : Option (List (Clause α)))
+    (a b : ArgumentPackage α) (s t : ℕ) : Option Bool :=
+  let checks := defeatChecks index hints ca cb a b s t
   if checks.any (· == some true) then some true
   else if checks.all (· == some false) then some false
   else none
 
+/-- Whether `a`, of strength `s`, defeats `b`, of strength `t`, from hints, each
+position converted to clauses here. -/
+def defeatsBy? (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage α) (s t : ℕ) :
+    Option Bool :=
+  defeatsWith? index hints (clausesOf a.held) (clausesOf b.held) a b s t
+
 /-- Whether `a`, of strength `s`, defeats `b`, of strength `t`, every question
 searched: `defeatsBy?` with no hints. -/
 def defeats? (a b : ArgumentPackage α) (s t : ℕ) : Option Bool :=
@@ -1028,8 +1035,9 @@ theorem defeats_of_defeatsBy? {index : α → ℕ} {hints : List Hint} {a b : Ar
     {s t : ℕ} (hidx : Function.Injective index ∨ hints = []) (hs : a.strength = s)
     (ht : b.strength = t) (h : defeatsBy? index hints a b s t = some true) : Defeats a b := by
   subst hs ht
-  dsimp only [defeatsBy?] at h
-  generalize hc : defeatChecks index hints a b a.strength b.strength = checks at h
+  dsimp only [defeatsBy?, defeatsWith?] at h
+  generalize hc : defeatChecks index hints (clausesOf a.held) (clausesOf b.held) a b a.strength
+    b.strength = checks at h
   split at h
   · rename_i hany
     obtain ⟨x, hx, hxt⟩ := List.any_eq_true.mp hany
@@ -1055,8 +1063,9 @@ theorem not_defeats_of_defeatsBy? {index : α → ℕ} {hints : List Hint}
     {a b : ArgumentPackage α} {s t : ℕ} (hs : a.strength = s) (ht : b.strength = t)
     (h : defeatsBy? index hints a b s t = some false) : ¬ Defeats a b := by
   subst hs ht
-  dsimp only [defeatsBy?] at h
-  generalize hc : defeatChecks index hints a b a.strength b.strength = checks at h
+  dsimp only [defeatsBy?, defeatsWith?] at h
+  generalize hc : defeatChecks index hints (clausesOf a.held) (clausesOf b.held) a b a.strength
+    b.strength = checks at h
   split at h
   · simp at h
   · split at h
@@ -1138,6 +1147,19 @@ theorem defeats_iff_of_certified {a b : ArgumentPackage α} {s t : ℕ} {P : Pro
   · simp only [hP, decide_false] at h
     exact iff_of_false (not_defeats_of_defeatsBy? hs ht h) hP
 
+/-- **A cell of a defeat table, from hints the kernel checks and each position's
+clauses given.** The clauses are proved once for each party
+(`prepare_clauses`), so a table converts each position once rather than in every
+cell. -/
+theorem defeats_iff_of_prepared {a b : ArgumentPackage α} {s t : ℕ} {P : Prop} [Decidable P]
+    {ca cb : Option (List (Clause α))} (hs : a.strength = s) (ht : b.strength = t)
+    (hca : clausesOf a.held = ca) (hcb : clausesOf b.held = cb)
+    (h : ∃ (index : α → ℕ), Function.Injective index ∧
+      ∃ hints : List Hint, defeatsWith? index hints ca cb a b s t = some (decide P)) :
+    Defeats a b ↔ P := by
+  subst hca hcb
+  exact defeats_iff_of_certified hs ht h
+
 end Attacks
 
 end Testimony.Logic.Horn
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean
index 0ae0287..42a1b9a 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean
@@ -513,6 +513,8 @@ theorem partyNode_strength : ∀ i, (partyNode i).strength = partyStrength i
   | .motyer => motyerReply_strength
   | .micah => micahParity_strength
 
+prepare_clauses isaiahDisputeClauses for isaiahDispute
+
 /-- **Who defeats whom**, all thirty-six pairs: the critic and the scriptural
 reading defeat each other; each reply defeats the critic; the critic defeats
 Berry and Motyer back, but neither of Postell's counterexamples; nothing
@@ -523,7 +525,8 @@ checked by the kernel; the table is what the computation is checked
 against. -/
 theorem isaiahDispute_defeats : ∀ i j, isaiahDispute.defeats i j ↔ partyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (partyNode_strength i) (partyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (partyNode_strength i) (partyNode_strength j)
+    (isaiahDisputeClauses.spec i) (isaiahDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean
index 181535c..9a2d616 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean
@@ -212,14 +212,16 @@ theorem genesisPartyNode_strength : ∀ i, (genesisPartyNode i).strength = 0
   | .posterity => posterityCase_strength
   | .idiom => idiomCase_strength
 
+prepare_clauses genesisDisputeClauses for genesisDispute
+
 /-- **Who defeats whom**, all nine pairs: Luther and Leupold defeat each other,
 Luther and Lewis defeat each other, and nothing else. Every cell is computed
 from what the parties hold by `Horn.defeats?` and checked by the kernel. -/
 theorem genesisDispute_defeats :
     ∀ i j, genesisDispute.defeats i j ↔ genesisPartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (genesisPartyNode_strength i)
-    (genesisPartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (genesisPartyNode_strength i) (genesisPartyNode_strength j)
+    (genesisDisputeClauses.spec i) (genesisDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Matthew.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Matthew.lean
index b8d6828..a6ce54e 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Matthew.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Matthew.lean
@@ -159,14 +159,16 @@ theorem matthewPartyNode_strength : ∀ i, (matthewPartyNode i).strength = 0
   | .matthew => matthewCase_strength
   | .drift => driftObjection_strength
 
+prepare_clauses matthewDisputeClauses for matthewDispute
+
 /-- **Who defeats whom**, all four pairs: Matthew's reading and Wegner defeat
 each other, and nothing else. Every cell is computed from what the parties hold
 by `Horn.defeats?` and checked by the kernel. -/
 theorem matthewDispute_defeats :
     ∀ i j, matthewDispute.defeats i j ↔ matthewPartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (matthewPartyNode_strength i)
-    (matthewPartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (matthewPartyNode_strength i) (matthewPartyNode_strength j)
+    (matthewDisputeClauses.spec i) (matthewDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Protoevangelium.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Protoevangelium.lean
index c2c8227..55c451a 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Protoevangelium.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Protoevangelium.lean
@@ -371,14 +371,16 @@ theorem promisePartyNode_strength : ∀ i, (promisePartyNode i).strength = 0
   | .syntax => syntaxCase_strength
   | .scene => sceneCase_strength
 
+prepare_clauses promiseDisputeClauses for promiseDispute
+
 /-- **Who defeats whom**, all sixteen pairs: Westermann defeats the fulfilment,
 the syntax and the scene, and each defeats him back; and nothing else. Every cell is computed
 from what the parties hold by `Horn.defeats?` and checked by the kernel. -/
 theorem promiseDispute_defeats :
     ∀ i j, promiseDispute.defeats i j ↔ promisePartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (promisePartyNode_strength i)
-    (promisePartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (promisePartyNode_strength i) (promisePartyNode_strength j)
+    (promiseDisputeClauses.spec i) (promiseDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean
index 57780f4..b7541d6 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean
@@ -542,6 +542,8 @@ theorem septuagintPartyNode_strength :
   | .dinah => dinahCase_strength
   | .miller => millerCase_strength
 
+prepare_clauses septuagintDisputeClauses for septuagintDispute
+
 /-- **Who defeats whom**, all thirty-six pairs: Wegner defeats the witness,
 Rico and Gentry and the laws, and each defeats him back; so does Miller, and
 each defeats him back; the status reading defeats Wegner and Miller, and
@@ -550,8 +552,9 @@ parties hold by `Horn.defeats?` and checked by the kernel. -/
 theorem septuagintDispute_defeats :
     ∀ i j, septuagintDispute.defeats i j ↔ septuagintPartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (septuagintPartyNode_strength i)
-    (septuagintPartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (septuagintPartyNode_strength i)
+    (septuagintPartyNode_strength j)
+    (septuagintDisputeClauses.spec i) (septuagintDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean
index f71e7b2..e467876 100644
--- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean
+++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean
@@ -198,6 +198,8 @@ theorem wegnerPartyNode_strength : ∀ i, (wegnerPartyNode i).strength = 0
   | .sign => signArgument_strength
   | .reply => ordinarySignReply_strength
 
+prepare_clauses wegnerDisputeClauses for wegnerDispute
+
 /-- **Who defeats whom**, all nine pairs: the fathers and Wegner defeat each
 other, the fathers and the reply defeat each other, and nothing else. Every
 cell is computed from the parties' premises by `Horn.defeats?` and checked by
@@ -205,8 +207,8 @@ the kernel. -/
 theorem wegnerDispute_defeats :
     ∀ i j, wegnerDispute.defeats i j ↔ wegnerPartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (wegnerPartyNode_strength i)
-    (wegnerPartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (wegnerPartyNode_strength i) (wegnerPartyNode_strength j)
+    (wegnerDisputeClauses.spec i) (wegnerDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/Checks.lean b/arguments/TestimonyArguments/Checks.lean
index 3d4c82f..78d3fae 100644
--- a/arguments/TestimonyArguments/Checks.lean
+++ b/arguments/TestimonyArguments/Checks.lean
@@ -101,13 +101,13 @@ The canonical witness
 #check_refutations under TestimonyArguments using unfoldSets
 
 /--
-info: every entry is a tagged definition, and every key names one: 2298 definitions, 176 entries
+info: every entry is a tagged definition, and every key names one: 2302 definitions, 176 entries
 -/
 #guard_msgs in
 #check_citations under Testimony
 
 /--
-info: every entry is a tagged definition, and every key names one: 1622 definitions, 176 entries
+info: every entry is a tagged definition, and every key names one: 1633 definitions, 176 entries
 -/
 #guard_msgs in
 #check_citations under TestimonyArguments
diff --git a/arguments/TestimonyArguments/SolaFide/Dispute.lean b/arguments/TestimonyArguments/SolaFide/Dispute.lean
index b896256..913a9bf 100644
--- a/arguments/TestimonyArguments/SolaFide/Dispute.lean
+++ b/arguments/TestimonyArguments/SolaFide/Dispute.lean
@@ -927,13 +927,16 @@ theorem partyNode_strength : ∀ i, (partyNode i).strength = partyStrength i
   | .trentOnPaulsWord => tridentineOnPaulsWord_strength
   | .romansOnTheWord => romansFourOnTheWord_strength
 
+prepare_clauses solaFideDisputeClauses for solaFideDispute
+
 /-- The first six rows of the table, computed from the parties' premises and
 checked by the kernel. The table is split in two only so that each declaration
 stays within the heartbeat budget. -/
 private theorem solaFideDispute_defeats_first (i : Party)
     (hi : i ∈ [.pauline, .dominical, .apostolic, .trent, .apocalyptic, .sanders])
     (j : Party) : solaFideDispute.defeats i j ↔ partyDefeats i j := by
-  refine Horn.defeats_iff_of_certified (partyNode_strength i) (partyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (partyNode_strength i) (partyNode_strength j)
+    (solaFideDisputeClauses.spec i) (solaFideDisputeClauses.spec j) ?_
   simp only [List.mem_cons, List.not_mem_nil, or_false] at hi
   rcases hi with rfl | rfl | rfl | rfl | rfl | rfl <;> cases j <;> horn_certify
 
@@ -941,7 +944,8 @@ private theorem solaFideDispute_defeats_first (i : Party)
 private theorem solaFideDispute_defeats_second (i : Party)
     (hi : i ∈ [.critics, .jervell, .gospel, .lexical, .trentOnPaulsWord, .romansOnTheWord])
     (j : Party) : solaFideDispute.defeats i j ↔ partyDefeats i j := by
-  refine Horn.defeats_iff_of_certified (partyNode_strength i) (partyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (partyNode_strength i) (partyNode_strength j)
+    (solaFideDisputeClauses.spec i) (solaFideDisputeClauses.spec j) ?_
   simp only [List.mem_cons, List.not_mem_nil, or_false] at hi
   rcases hi with rfl | rfl | rfl | rfl | rfl | rfl <;> cases j <;> horn_certify
 
diff --git a/arguments/TestimonyArguments/SolaFide/James.lean b/arguments/TestimonyArguments/SolaFide/James.lean
index 72ab1f4..0a67d60 100644
--- a/arguments/TestimonyArguments/SolaFide/James.lean
+++ b/arguments/TestimonyArguments/SolaFide/James.lean
@@ -799,6 +799,8 @@ theorem jamesPartyNode_strength : ∀ i, (jamesPartyNode i).strength = jamesPart
   | .renewalOnTheWord => renewalOnTheWord_strength
   | .westminsterOnReward => westminsterOnReward_strength
 
+prepare_clauses jamesDisputeClauses for jamesDispute
+
 /-- **Who defeats whom**, all 144 pairs. James's word defeats Trent's reading of
 it, and the reading's reply fails; it defeats the renewal reading too, whose
 reply fails for the same reason — it rests on Paul's word as renewal, rated
@@ -822,7 +824,8 @@ by the kernel. -/
 theorem jamesDispute_defeats :
     ∀ i j, jamesDispute.defeats i j ↔ jamesPartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (jamesPartyNode_strength i) (jamesPartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (jamesPartyNode_strength i) (jamesPartyNode_strength j)
+    (jamesDisputeClauses.spec i) (jamesDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/SolaFide/JesusWords.lean b/arguments/TestimonyArguments/SolaFide/JesusWords.lean
index 2746786..d5372f7 100644
--- a/arguments/TestimonyArguments/SolaFide/JesusWords.lean
+++ b/arguments/TestimonyArguments/SolaFide/JesusWords.lean
@@ -550,6 +550,8 @@ theorem wordsPartyNode_strength : ∀ i, (wordsPartyNode i).strength = wordsPart
   | .matthew19Way => matthew19WayCase_strength
   | .matthew19Legal => matthew19LegalCase_strength
 
+prepare_clauses jesusWordsDisputeClauses for jesusWordsDispute
+
 /-- **Who defeats whom**, all 49 pairs: four standoffs, and nothing else. Luke
 7:50 and Trent defeat each other, and so do Luke 18 and Trent, over Trent's
 definition of justification; each Matthean reading defeats its rival, and is
@@ -558,7 +560,8 @@ defeated back. Every cell is computed from the parties' premises by
 theorem jesusWordsDispute_defeats :
     ∀ i j, jesusWordsDispute.defeats i j ↔ wordsPartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (wordsPartyNode_strength i) (wordsPartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (wordsPartyNode_strength i) (wordsPartyNode_strength j)
+    (jesusWordsDisputeClauses.spec i) (jesusWordsDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/SolaScriptura/Dispute.lean b/arguments/TestimonyArguments/SolaScriptura/Dispute.lean
index 77cedaf..24276af 100644
--- a/arguments/TestimonyArguments/SolaScriptura/Dispute.lean
+++ b/arguments/TestimonyArguments/SolaScriptura/Dispute.lean
@@ -179,6 +179,8 @@ theorem mark7PartyNode_strength : ∀ i, (mark7PartyNode i).strength = mark7Part
   | .trentAsMensCommandments => tridentineAsMensCommandments_strength
   | .trentAsApostolicWord => tridentineAsApostolicWord_strength
 
+prepare_clauses mark7DisputeClauses for mark7Dispute
+
 /-- **Who defeats whom**, all 25 pairs. Mark 7's principle defeats Trent read as
 commandments of men, and that reading's reply fails against it. Mark 7's case
 and Trent defeat each other, as Trent states it and read either way. Nothing
@@ -189,7 +191,8 @@ by the kernel — the defeats, and the absences of defeat, alike. -/
 theorem mark7Dispute_defeats :
     ∀ i j, mark7Dispute.defeats i j ↔ mark7PartyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (mark7PartyNode_strength i) (mark7PartyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (mark7PartyNode_strength i) (mark7PartyNode_strength j)
+    (mark7DisputeClauses.spec i) (mark7DisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean b/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean
index 0ad8ee3..3f7e437 100644
--- a/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean
+++ b/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean
@@ -154,6 +154,8 @@ theorem viewNode_strength : ∀ i, (viewNode i).strength = viewStrength i
   | .holiness => holinessCase_strength
   | .sacramental => sacramentalCase_strength
 
+prepare_clauses spiritBaptismDisputeClauses for spiritBaptismDispute
+
 /-- **Who defeats whom**, all 16 pairs: four standoffs, and nothing else. The
 conversion view and each subsequence view defeat each other — "no second to
 seek" against "a second to seek" — and the Pentecostal view also denies the
@@ -163,7 +165,8 @@ subsequence view defeat each other on the same point. Every cell is computed by
 theorem spiritBaptismDispute_defeats :
     ∀ i j, spiritBaptismDispute.defeats i j ↔ viewDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (viewNode_strength i) (viewNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (viewNode_strength i) (viewNode_strength j)
+    (spiritBaptismDisputeClauses.spec i) (spiritBaptismDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
diff --git a/arguments/bench/Engine.lean b/arguments/bench/Engine.lean
index 3fcb072..ec95176 100644
--- a/arguments/bench/Engine.lean
+++ b/arguments/bench/Engine.lean
@@ -166,6 +166,14 @@ example : ∀ i j, septuagintDispute.defeats i j ↔ septuagintPartyDefeats i j
     (septuagintPartyNode_strength j) ?_
   cases i <;> cases j <;> horn_certify
 
+#bench "table, prepared: Septuagint, 36 cells" in
+example : ∀ i j, septuagintDispute.defeats i j ↔ septuagintPartyDefeats i j := by
+  intro i j
+  refine Horn.defeats_iff_of_prepared (septuagintPartyNode_strength i)
+    (septuagintPartyNode_strength j) (septuagintDisputeClauses.spec i)
+    (septuagintDisputeClauses.spec j) ?_
+  cases i <;> cases j <;> horn_certify
+
 #bench "verdict: Septuagint, grounded in stages" in
 example : Verdict septuagintDispute where
   finite := septuagintFinite
@@ -241,6 +249,15 @@ example (i : Party)
   simp only [List.mem_cons, List.not_mem_nil, or_false] at hi
   rcases hi with rfl | rfl | rfl | rfl | rfl | rfl <;> cases j <;> horn_certify
 
+#bench (runs := 1) "table, prepared: sola fide, first half, 72 cells" in
+example (i : Party)
+    (hi : i ∈ [.pauline, .dominical, .apostolic, .trent, .apocalyptic, .sanders])
+    (j : Party) : solaFideDispute.defeats i j ↔ partyDefeats i j := by
+  refine Horn.defeats_iff_of_prepared (partyNode_strength i) (partyNode_strength j)
+    (solaFideDisputeClauses.spec i) (solaFideDisputeClauses.spec j) ?_
+  simp only [List.mem_cons, List.not_mem_nil, or_false] at hi
+  rcases hi with rfl | rfl | rfl | rfl | rfl | rfl <;> cases j <;> horn_certify
+
 #bench "strengths: James hearing under evidence, 12 parties" in
 example :
     ∀ i, ((jamesRegister.rerated .evidence).node i).strength = ratedStrength .evidence i := by
diff --git a/docs/src/logic.md b/docs/src/logic.md
index 4043a9e..0951df4 100644
--- a/docs/src/logic.md
+++ b/docs/src/logic.md
@@ -572,9 +572,12 @@ dispute's relation equal to the table. Every cell is computed from the
 premises and checked by the kernel — the defeats and the absences alike:
 
 ```lean
+prepare_clauses isaiahDisputeClauses for isaiahDispute
+
 theorem isaiahDispute_defeats : ∀ i j, isaiahDispute.defeats i j ↔ partyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (partyNode_strength i) (partyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (partyNode_strength i) (partyNode_strength j)
+    (isaiahDisputeClauses.spec i) (isaiahDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 ```
 
@@ -613,6 +616,13 @@ can only make the proof fail, and `Horn.defeats_iff_of_certified` states exactly
 what `Horn.defeats_iff_of_defeats?` does. `decide +kernel` on `Horn.defeats?`
 still proves any cell, searching.
 
+Every cell asks its questions of two parties' positions as clauses, and a party
+appears in a row and a column of cells. `prepare_clauses` converts each party's
+position once, writes the clauses out, and proves for each party that they are
+what the conversion gives (`isaiahDisputeClauses.spec`); every cell then reads
+them, and `Horn.defeats_iff_of_prepared` takes the proofs, so the kernel converts
+each position once per table rather than once per cell.
+
 A single defeat worth naming is one line, from the same computation:
 
 ```lean
diff --git a/docs/src/performance.md b/docs/src/performance.md
index 83aad5a..d985bec 100644
--- a/docs/src/performance.md
+++ b/docs/src/performance.md
@@ -76,6 +76,33 @@ The slowest modules of the arguments' build: `SolaFide.Ratings` (150 s),
 | 4 | Certify assessments and consistency; in a hearing, weigh a step's rank only once it is attacked (#183) | the hearings and assessments | 3.08 s, 97 MiB | 0.48 s, 16 MiB | 0.008 | kept |
 | 5 | Compare a citation by its key and locus, a key checked to name one entry | a hearing's rerated strengths | 2.54 s, 83 MiB | 0.86 s, 25 MiB | 0.008 | kept |
 | 6 | Replay a refutation on bitmasks (#180) | the certified defeat tables | 7.21 s, 94 MiB | 5.99 s, 70 MiB | 0.008 | kept |
+| 10 | Convert each party's position to clauses once per table, not once per cell | the certified defeat tables | 1.52 s, 14 MiB | 0.93 s, 12 MiB | 0.008 | kept |
+
+Round 10, measured on one side of a `scripts/bench-ab.sh` run against `main`,
+five interleaved rounds, as rounds 3 and 8 were: each defeat table is
+benchmarked certified, as before, and prepared. A certified cell converted both
+parties' positions to clauses, so a party appearing in a row and a column of
+cells was converted once for every cell. `prepare_clauses` converts each
+party's position once, at elaboration time, writes the clauses out, and has the
+kernel check, once for each party, that they are what the conversion gives;
+every cell then reads them (`Horn.defeatsWith?`,
+`Horn.defeats_iff_of_prepared`). The Septuagint's table fell from 1.52 s to
+0.93 s (−39%, p = 0.008), and half of sola fide's from 6.31 s to 5.53 s (−12%,
+p = 0.016); preparing sola fide's twelve parties costs 0.35 s, once. Every
+benchmark shared with `main` matched it, but for the searched Septuagint table,
+which this change does not touch, 8% faster (p = 0.032): noise, most likely.
+
+Before this, the round's real target was measured and set aside. Pruning each
+question to the components of a position it touches, found by union-find over
+the claims each clause mentions, asked the kernel about a third of the clauses
+(6,671 of 19,800 in half of sola fide's table) but saved only 15% of the time.
+Most of a question's cost is not in the clauses it reads but in how the kernel
+reads them: a model check of Paul's 33 clauses took 7.6 ms, of which the
+library's list functions, compiled through `brecOn`, and each claim's
+constructor index, computed by a case split over the claim type's hundred-odd
+constructors, are most. Written on `List.rec` and over indices, the same check
+took about 3 ms. That is the next round; pruning, which makes the cost follow
+the part of a position a question touches rather than the whole, follows it.
 
 Round 6, `scripts/bench-ab.sh` against `main`, five interleaved rounds. A
 certified refutation was replayed over lists of settled atoms, each membership
diff --git a/examples/TestimonyExamples/Checks.lean b/examples/TestimonyExamples/Checks.lean
index 1a82bc0..6e077c1 100644
--- a/examples/TestimonyExamples/Checks.lean
+++ b/examples/TestimonyExamples/Checks.lean
@@ -52,7 +52,7 @@ The grits
 #guard_msgs in
 #check_refutations under TestimonyExamples using unfoldSets
 
-/-- info: every entry is a tagged definition, and every key names one: 76 definitions, 17 entries -/
+/-- info: every entry is a tagged definition, and every key names one: 78 definitions, 17 entries -/
 #guard_msgs in
 #check_citations under TestimonyExamples
 
diff --git a/examples/TestimonyExamples/Grits/Dispute.lean b/examples/TestimonyExamples/Grits/Dispute.lean
index d4342bc..4cb4c5c 100644
--- a/examples/TestimonyExamples/Grits/Dispute.lean
+++ b/examples/TestimonyExamples/Grits/Dispute.lean
@@ -163,6 +163,8 @@ theorem sideNode_strength : ∀ i, (sideNode i).strength = sideStrength i
   | .direct => direct_strength
   | .cross => cross_strength
 
+prepare_clauses gritsDisputeClauses for gritsDispute
+
 /-- **Who defeats whom**, all four pairs. The cross-examination defeats the
 testimony: it denies the five-minute breakfast and the five minutes, and it is
 the stronger. The testimony's denials of the twenty minutes are attacks, and
@@ -170,7 +172,8 @@ fail: its weakest link is weaker than the cross-examination's. Every cell is
 computed by `Horn.defeats?` and checked by the kernel. -/
 theorem gritsDispute_defeats : ∀ i j, gritsDispute.defeats i j ↔ sideDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (sideNode_strength i) (sideNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (sideNode_strength i) (sideNode_strength j)
+    (gritsDisputeClauses.spec i) (gritsDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/
@@ -277,14 +280,16 @@ theorem atTheFastCookNode_strength : ∀ i, (atTheFastCookNode i).strength = fas
   | .direct => direct_strength
   | .cross => crossAtTheFastCook_strength
 
+prepare_clauses atTheFastCookDisputeClauses for atTheFastCookDispute
+
 /-- **Who defeated whom at the fast cook**, all four pairs: a standoff. With both
 weakest links `disputed`, each side's attacks on the other are defeats. Every
 cell is computed by `Horn.defeats?` and checked by the kernel. -/
 theorem atTheFastCookDispute_defeats :
     ∀ i j, atTheFastCookDispute.defeats i j ↔ fastCookDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (atTheFastCookNode_strength i)
-    (atTheFastCookNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (atTheFastCookNode_strength i) (atTheFastCookNode_strength j)
+    (atTheFastCookDisputeClauses.spec i) (atTheFastCookDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute at the fast cook, in the form the verdict solver computes with. -/

From d81045ea0ef43fd401b6949687cbd6f8dd1cf350 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 2 Nov 2026 07:56:05 +0000
Subject: [PATCH 2/4] Prepared cells: search hints from the clauses; generated
 declarations off the pages

`Horn.defeatChecks` and `Horn.defeatsWith?` no longer take the attacking
package, which a cell with given clauses never reads; `horn_certify` finds a
prepared cell's hints from the clauses themselves (`Horn.hintsWith`). The
argument pages skip a declaration with no place in the source: it was
generated by a command, `prepare_clauses`, as machinery for the kernel, not
written for a reader, and every generated page stays as it was.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BC49XsbtehCbmJMavF1K5Q
---
 Testimony/Logic/Certificate.lean         | 21 +++++++++++++++++++--
 Testimony/Logic/Horn.lean                | 14 +++++++-------
 Testimony/Tools/Pages.lean               |  6 +++++-
 arguments/TestimonyArguments/Checks.lean |  2 +-
 4 files changed, 32 insertions(+), 11 deletions(-)

diff --git a/Testimony/Logic/Certificate.lean b/Testimony/Logic/Certificate.lean
index a370800..b563cad 100644
--- a/Testimony/Logic/Certificate.lean
+++ b/Testimony/Logic/Certificate.lean
@@ -115,6 +115,23 @@ question `Horn.satisfiable_of_certified` asks. -/
 def hintsAppend (index : α → ℕ) (Γ Δ : List (Formula α)) : List Hint :=
   [hintOnAll index (base Γ) Δ]
 
+/-- The base of a list of clauses, already converted: what propagation settled
+from them, and the clauses that fired. -/
+def baseOfClauses (cs : List (Clause α)) : Base α :=
+  let (s, trace) := chainTrace cs (cs.length + 1) ⟨[], []⟩ []
+  ⟨cs, s, trace⟩
+
+/-- **The hints for a cell whose positions are given as clauses**
+(`Horn.defeatsWith?`), in the order `Horn.defeatChecks` asks its questions, as
+`hintsFor` finds them from the packages. -/
+@[nospecialize]
+def hintsWith (index : α → ℕ) (ca cb : Option (List (Clause α))) (b : ArgumentPackage α) :
+    List Hint :=
+  let ba := ca.map baseOfClauses
+  let bb := cb.map baseOfClauses
+  (hintOn index ba b.conclusion :: b.premises.map (hintOn index ba)) ++
+    (stepsOf b.premises).flatMap fun q => [hintOn index bb (∼q.2), hintOn index ba q.2]
+
 variable [HasPostulates α]
 
 /-- **The hints for a dissent's findings**, in the order `Dissent.findingsBy?`
@@ -182,8 +199,8 @@ def searchFor (index lhs : Expr) : MetaM Expr := do
   let args := lhs.getAppArgs
   if lhs.isAppOfArity ``Horn.defeatsBy? 9 then
     mkAppOptM ``Horn.hintsFor #[args[0]!, args[1]!, args[2]!, index, args[5]!, args[6]!]
-  else if lhs.isAppOfArity ``Horn.defeatsWith? 10 then
-    mkAppOptM ``Horn.hintsFor #[args[0]!, args[1]!, none, index, args[6]!, args[7]!]
+  else if lhs.isAppOfArity ``Horn.defeatsWith? 9 then
+    mkAppOptM ``Horn.hintsWith #[args[0]!, args[1]!, index, args[4]!, args[5]!, args[6]!]
   else if lhs.isAppOfArity ``Dissent.findingsBy? 6 then
     mkAppOptM ``Horn.findingsHints #[args[0]!, args[1]!, args[2]!, index, args[5]!]
   else if lhs.isAppOfArity ``Horn.satisfiableAppend? 6 then
diff --git a/Testimony/Logic/Horn.lean b/Testimony/Logic/Horn.lean
index 216354c..778e85e 100644
--- a/Testimony/Logic/Horn.lean
+++ b/Testimony/Logic/Horn.lean
@@ -890,7 +890,7 @@ def stepRebuts? (index : α → ℕ) (hb ha : Hint) (ca cb : Option (List (Claus
 claim `b`'s steps deliver, each with its hint, given the clauses of what each
 holds, `ca` and `cb`. -/
 def defeatChecks (index : α → ℕ) (hints : List Hint) (ca cb : Option (List (Clause α)))
-    (a b : ArgumentPackage α) (s t : ℕ) : List (Option Bool) :=
+    (b : ArgumentPackage α) (s t : ℕ) : List (Option Bool) :=
   let n := b.premises.length
   (rebuts? index (hintAt hints 0) b ca s t ::
     b.premises.zipIdx.map fun (φ, i) => undermines? index (hintAt hints (i + 1)) b ca s φ) ++
@@ -905,8 +905,8 @@ clauses, or its hint did not check, and none succeeded. The checks are made
 once. A table converts each party's position once, not once for every cell it
 appears in (`defeats_iff_of_prepared`). -/
 def defeatsWith? (index : α → ℕ) (hints : List Hint) (ca cb : Option (List (Clause α)))
-    (a b : ArgumentPackage α) (s t : ℕ) : Option Bool :=
-  let checks := defeatChecks index hints ca cb a b s t
+    (b : ArgumentPackage α) (s t : ℕ) : Option Bool :=
+  let checks := defeatChecks index hints ca cb b s t
   if checks.any (· == some true) then some true
   else if checks.all (· == some false) then some false
   else none
@@ -915,7 +915,7 @@ def defeatsWith? (index : α → ℕ) (hints : List Hint) (ca cb : Option (List
 position converted to clauses here. -/
 def defeatsBy? (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage α) (s t : ℕ) :
     Option Bool :=
-  defeatsWith? index hints (clausesOf a.held) (clausesOf b.held) a b s t
+  defeatsWith? index hints (clausesOf a.held) (clausesOf b.held) b s t
 
 /-- Whether `a`, of strength `s`, defeats `b`, of strength `t`, every question
 searched: `defeatsBy?` with no hints. -/
@@ -1036,7 +1036,7 @@ theorem defeats_of_defeatsBy? {index : α → ℕ} {hints : List Hint} {a b : Ar
     (ht : b.strength = t) (h : defeatsBy? index hints a b s t = some true) : Defeats a b := by
   subst hs ht
   dsimp only [defeatsBy?, defeatsWith?] at h
-  generalize hc : defeatChecks index hints (clausesOf a.held) (clausesOf b.held) a b a.strength
+  generalize hc : defeatChecks index hints (clausesOf a.held) (clausesOf b.held) b a.strength
     b.strength = checks at h
   split at h
   · rename_i hany
@@ -1064,7 +1064,7 @@ theorem not_defeats_of_defeatsBy? {index : α → ℕ} {hints : List Hint}
     (h : defeatsBy? index hints a b s t = some false) : ¬ Defeats a b := by
   subst hs ht
   dsimp only [defeatsBy?, defeatsWith?] at h
-  generalize hc : defeatChecks index hints (clausesOf a.held) (clausesOf b.held) a b a.strength
+  generalize hc : defeatChecks index hints (clausesOf a.held) (clausesOf b.held) b a.strength
     b.strength = checks at h
   split at h
   · simp at h
@@ -1155,7 +1155,7 @@ theorem defeats_iff_of_prepared {a b : ArgumentPackage α} {s t : ℕ} {P : Prop
     {ca cb : Option (List (Clause α))} (hs : a.strength = s) (ht : b.strength = t)
     (hca : clausesOf a.held = ca) (hcb : clausesOf b.held = cb)
     (h : ∃ (index : α → ℕ), Function.Injective index ∧
-      ∃ hints : List Hint, defeatsWith? index hints ca cb a b s t = some (decide P)) :
+      ∃ hints : List Hint, defeatsWith? index hints ca cb b s t = some (decide P)) :
     Defeats a b ↔ P := by
   subst hca hcb
   exact defeats_iff_of_certified hs ht h
diff --git a/Testimony/Tools/Pages.lean b/Testimony/Tools/Pages.lean
index 2701950..1cffe61 100644
--- a/Testimony/Tools/Pages.lean
+++ b/Testimony/Tools/Pages.lean
@@ -253,7 +253,11 @@ def deriveArgumentBodies (tableName : Ident) (root : Name) : CommandElabM Unit :
       | _ =>
         let some modIdx := env.getModuleIdxFor? n | continue
         let some k := modOrder[env.header.moduleNames[modIdx.toNat]!]? | continue
-        let line := (← findDeclarationRanges? n).map (·.range.pos.line) |>.getD 0
+        -- A declaration with no place in the source was generated by a command
+        -- (`prepare_clauses`'s clauses), machinery for the kernel, not
+        -- something written for a reader.
+        let some ranges ← findDeclarationRanges? n | continue
+        let line := ranges.range.pos.line
         let dname := n.getString!
         let headOf (e : Expr) : Option Name :=
           match e.getAppFn with
diff --git a/arguments/TestimonyArguments/Checks.lean b/arguments/TestimonyArguments/Checks.lean
index 83cda2d..6b4e445 100644
--- a/arguments/TestimonyArguments/Checks.lean
+++ b/arguments/TestimonyArguments/Checks.lean
@@ -101,7 +101,7 @@ The canonical witness
 #check_refutations under TestimonyArguments using unfoldSets
 
 /--
-info: every entry is a tagged definition, and every key names one: 2323 definitions, 176 entries
+info: every entry is a tagged definition, and every key names one: 2325 definitions, 176 entries
 -/
 #guard_msgs in
 #check_citations under Testimony

From 148318c76a61a6bc3cdbe71e52bd4b6b08dcee04 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 2 Nov 2026 08:08:29 +0000
Subject: [PATCH 3/4] Ledger: round 10 measured on the final head

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BC49XsbtehCbmJMavF1K5Q
---
 docs/src/performance.md | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/docs/src/performance.md b/docs/src/performance.md
index 9aed628..e3fa97f 100644
--- a/docs/src/performance.md
+++ b/docs/src/performance.md
@@ -77,7 +77,7 @@ The slowest modules of the arguments' build: `SolaFide.Ratings` (150 s),
 | 5 | Compare a citation by its key and locus, a key checked to name one entry | a hearing's rerated strengths | 2.54 s, 83 MiB | 0.86 s, 25 MiB | 0.008 | kept |
 | 6 | Replay a refutation on bitmasks (#180) | the certified defeat tables | 7.21 s, 94 MiB | 5.99 s, 70 MiB | 0.008 | kept |
 | 7 | Find exclusions through shared keys, not every pair | the sola fide joins | 45.4 s, 3.43 GiB | 10.6 s, 1.06 GiB | 0.008 | kept |
-| 10 | Convert each party's position to clauses once per table, not once per cell | the certified defeat tables | 1.52 s, 14 MiB | 0.93 s, 12 MiB | 0.008 | kept |
+| 10 | Convert each party's position to clauses once per table, not once per cell | the certified defeat tables | 1.61 s, 13 MiB | 0.99 s, 11 MiB | 0.008 | kept |
 
 Round 10, measured on one side of a `scripts/bench-ab.sh` run against `main`,
 five interleaved rounds, as rounds 3 and 8 were: each defeat table is
@@ -87,11 +87,12 @@ cells was converted once for every cell. `prepare_clauses` converts each
 party's position once, at elaboration time, writes the clauses out, and has the
 kernel check, once for each party, that they are what the conversion gives;
 every cell then reads them (`Horn.defeatsWith?`,
-`Horn.defeats_iff_of_prepared`). The Septuagint's table fell from 1.52 s to
-0.93 s (−39%, p = 0.008), and half of sola fide's from 6.31 s to 5.53 s (−12%,
-p = 0.016); preparing sola fide's twelve parties costs 0.35 s, once. Every
-benchmark shared with `main` matched it, but for the searched Septuagint table,
-which this change does not touch, 8% faster (p = 0.032): noise, most likely.
+`Horn.defeats_iff_of_prepared`). The Septuagint's table fell from 1.61 s to
+0.99 s (−39%, p = 0.008), and half of sola fide's from 7.14 s to 5.44 s (−24%,
+p = 0.008); preparing sola fide's twelve parties costs 0.35 s, once. Every
+benchmark shared with `main` matched it. An earlier run, before the hints were
+searched from the clauses rather than the packages, measured −39% and −12%
+(p = 0.016).
 
 Before this, the round's real target was measured and set aside. Pruning each
 question to the components of a position it touches, found by union-find over

From b69f2f86777eb7ccafa725dd8f687f9eaec25260 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 2 Nov 2026 09:37:43 +0000
Subject: [PATCH 4/4] Ledger: round 10 records the List.rec checker, measured
 and dropped

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BC49XsbtehCbmJMavF1K5Q
---
 docs/src/performance.md | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/docs/src/performance.md b/docs/src/performance.md
index e3fa97f..a597d29 100644
--- a/docs/src/performance.md
+++ b/docs/src/performance.md
@@ -103,8 +103,19 @@ reads them: a model check of Paul's 33 clauses took 7.6 ms, of which the
 library's list functions, compiled through `brecOn`, and each claim's
 constructor index, computed by a case split over the claim type's hundred-odd
 constructors, are most. Written on `List.rec` and over indices, the same check
-took about 3 ms. That is the next round; pruning, which makes the cost follow
-the part of a position a question touches rather than the whole, follows it.
+took about 3 ms, cold.
+
+That did not carry over to the tables, and is recorded so that nobody tries it
+again. The checker's model check, clause checks and replay were rewritten on
+`List.rec`, each function proved equal to its core counterpart. A lookup written
+that way, `List.rec` over `Nat.rec`, made each refutation's replay exponential
+in the kernel, from 0.13 s to over 150 s as a synthetic position grew from 24 to
+32 formulas; without it, against this round's head, five interleaved rounds,
+neither table moved (the prepared ones −5%, p = 0.15, and +2%, p = 0.84) and
+one certified cell was 21% slower (p = 0.032). Within a cell the kernel shares
+the work the cold measurement repeated, so the list functions are not where a
+table's time goes. The rewrite was dropped, and clauses over indices with it,
+which the same measurement had suggested.
 
 Round 7, `scripts/bench-ab.sh` against `main`, five interleaved rounds. A
 profile of `Meanings.SolaFide` put 51 of its 64 seconds in one proof: that the