[deanberris]

What

Testimony.Logic.Compose lets two arguments that share no claim be heard as one dispute, without deciding any of its cells again.

• Dispute.sum: both disputes' parties (ι ⊕ κ), over both arguments' claims kept apart (α ⊕ β), with both arguments' meaning postulates (instHasPostulatesSum).
• Dispute.sum_defeats: defeats x y ↔ Sum.LiftRel dα.defeats dβ.defeats x y, for every pair at once.
  • Within one argument, a defeat is what it was before. Renaming a claim changes nothing a valuation can see (models_rename). The other argument's postulates mention none of these claims, so models of the two sides combine (entails_inl_iff / entails_inr_iff). Ranks and strengths carry over unchanged (rankOf_inl, strength_inl).
  • Across the two arguments, there is no attack (not_attacks_inl_inr). All a party holds about the other argument's claims is that argument's postulates. Every party there holds the same postulates along with each claim it rests on, derives or concludes, so those postulates cannot entail the negation of any such claim.
• Dispute.sumFinite / Solver.Finite.sum: build the solver's table from the two tables already proved.

Everything is proved constructively and checked by the kernel: no native_decide, no raised heartbeats, and no theorem is weaker than before.

Not covered: arguments that share a claim, or whose meanings are linked by a postulate. Those are one argument, and their cells are still decided one by one.

Measured (ledger round 12)

Sola fide's 12 parties and Mark 7's 5, heard as one dispute: 17 parties, 289 cells. Five rounds each, each in its own process:

	before	after	p
60 cells, sola fide → Mark 7, searched in the kernel vs composed	10.6 s, 86 MiB	6.4 ms, 0 MiB	0.008
whole 289-cell table, composed	—	12.9 ms
grounded verdict over it (decide +kernel)	—	79 ms

• Why the per-cell baseline is searched: a certificate can't index the sum's claims, because it reads each claim as a bit at its constructor's index and a sum type has only two. The earlier prototype gave the two arguments one flat claim type, and there the 289 cells took 18.9 s prepared and 16 s pruned.
• Verdict: the grounded extension is each argument's own: Paul's word, by its two routes, plus the principle of Mark 7.
• Against main: in scripts/bench-ab.sh origin/main --runs 5, every existing benchmark matched (NO CHANGE).

Also

• Fixture: a two-meetings case (Testimony.Checks.TwoMeetings) exercises Dispute.sum. It sits outside the fixture's namespace, so the checks don't pick it up.
• Pin: the arguments' citation check moved from 2370 to 2380 library definitions. That is the 8 new definitions plus the fixture's 2.
• Docs: logic.md (Disputes), the performance.md ledger, and the layout row in CLAUDE.md.

Gates

All passed: library, tools, arguments and examples builds; lake lint; axiom audit; kernel replay of all three packages; bibgen/argtex/statusgen/argdoc/exampletex --check; testimony_lint.py; mdbook build.

---

Generated by Claude Code