[deanberris]

Follows #221, which is merged; this branch is rebased on it.

What this changes

No verdict moves. This adds four commands in a new module, Testimony.Logic.Declare, and declares every dispute in TestimonyArguments with them.

A dispute module written by hand repeated a fixed pattern around a small amount of real content. The commands take the content and generate the pattern.

declare_dispute

It takes the parties' packages, the unfold set, and the defeat, support and part-of tables as lists of pairs. It generates:

• the Dispute
• each party's strength, read from the package's own P_strength theorem where there is one, and otherwise computed and checked by the kernel
• the prepared clauses, or with pruned, the parts
• the three table theorems, each cell decided by horn_certify as before; with rows N, a few rows at a time, as sola fide's 17-party table needs
• the solver form
• the map

declare_verdict

It takes a witness and generates the Verdict and the theorem it proves, so the result is stated once instead of twice. The theorem's statement is unfolded from the claim.

• proves T : type keeps a statement written out, checked against the claim.
• using F names a solver form other than the dispute's own.
• Without proves, only the verdict is declared, for a theorem that does more than restate it.

declare_hearing

declare_hearing H := D only [...], or except [...], hears some of a dispute's parties and gives the hearing its solver form.

declare_rerated

It takes a register's defeat table under each standard and generates the re-rated strengths, the table theorem, the solver forms and the hearing under each standard. This is the pattern in Matthew, the Genesis 3:15 promise, and James's ratings.

What a converted module looks like

/-- The dispute over the procession. -/
declare_dispute processionDispute := partyNode using trinityDefs
  /-- **Who defeats whom**: one standoff, and nothing else. -/
  defeats [(.western, .eastern), (.eastern, .western)]
  /-- **Nothing supports anything.** -/
  supports []
  /-- **LST's case is part of both the others'.** -/
  partOf [(.lst, .western), (.lst, .eastern)]
  /-- The dispute drawn. -/
  map processionMap

/-- Why the West can be defended: with LST, it answers the East itself. -/
declare_verdict westernWithTheTexts for processionDispute :
    .credulous .western [.lst, .western]
  /-- **The Western position can be defended.** -/
  proves @[headline] western_defensible

Each table's statement is its list, so it reads as data on the page:

processionDispute_defeats : ∀ i j, processionDispute.defeats i j ↔ (i, j) ∈ [(.western, .eastern), (.eastern, .western)]

Under a standard, a table is written as the change it makes, for example matthewDispute.defeatsTable.erase (.drift, .matthew).

Converted modules

Seventeen modules lose 1,537 lines between them; the new library module is 669.

Module	Before	After
SolaFide/Dispute	1585	1354
SolaFide/James	1109	1000
SolaFide/Ratings	1081	969
SolaFide/JesusWords	796	677
SolaFide/Hearings	309	255
BornOfAVirgin/Dispute	708	605
BornOfAVirgin/Dispute/Septuagint	671	565
BornOfAVirgin/Dispute/Protoevangelium	442	382
BornOfAVirgin/Dispute/Matthew	342	263
BornOfAVirgin/Dispute/Wegner	324	247
BornOfAVirgin/Dispute/Genesis	321	241
BornOfAVirgin/Dispute/PromiseHearing	202	164
SolaScriptura/Dispute	372	262
SolaScriptura/Hearings	136	111
SpiritBaptism/Dispute	357	241
Trinity/Dispute	281	167
Articles/Howell2003	463	459

What it claims, and what it does not

It claims that the generated declarations are the ones the hand-written modules had:

• The table theorems are proved cell by cell, as before.
• Every dispute's AIF graph has the same node and edge counts as before.
• The 262 headline results are unchanged.
• The axiom audit and kernel replay pass for both packages.
• A wrong pair in a table fails the build: nothing is trusted because it was written.

One dispute is not declared this way. Howell's hearing seats every sola fide party inside its own, as .sola q, so its parties are not an enumeration. Its table is still a function, now proved from the generated sola fide table, and its verdict uses declare_verdict.

Statements that change:

• The AIF check draws ten hearings, not five. The Isaiah and Wegner hearings used to be built inline and unnamed, and declare_hearing names them.
• A grounded verdict's generated statement reads grounded D.defeats = Solver.toSet [...]. Where a theorem had {.x} or another hand-written form that other modules use, the theorem stays hand-written or keeps its statement through proves T : type.
• Names change: D.finite for the old …Finite, D.node_strength for …PartyNode_strength, and R_defeats for …_rerated_defeats. The benchmarks are updated to them.

Build time. I timed each converted dispute module against its old version, both elaborated in the same environment, three times each:

Module	Old (s)	New (s)
Trinity, Spirit baptism, sola scriptura, Genesis, Wegner, Protoevangelium, Matthew	3.5–5.2	about 0.2–0.4 slower each
Septuagint	5.7	6.1
James	8.7	9.1
sola fide	43.3	46.3

The small modules pay the commands' own fixed cost. Most of sola fide's extra 3 s, about 2 s, is the kernel checking once, over all 289 pairs of parties, that the solver form's function agrees with the written list. Profiling found two other costs, and both are removed. Scanning the list in every verdict check was the larger: kernel type-checking time rose from 84 s to 302 s, summed over threads. The other was a decide in each of 289 cells.

The A/B gate cannot compare the benchmarks that name dispute internals. Both sides of the A/B run this branch's benchmark file, and main lacks the new names. So those benchmarks are reported for this branch only. The by-hand timings above stand in for that comparison. Every benchmark elaborates and runs here (37 of 37).

For the reader

The "Weighing" pages and their siblings lose the boilerplate entries: the table functions, decidability instances, strength theorems and solver forms. Every result, verdict and table stays, in source order. Where a party's weakest link was described by a strength theorem that is gone, the description moves to the party's docstring.

docs/src/logic.md describes the commands, and CLAUDE.md lists the module.

Checks run

• lake build, lake lint, lake exe axiom-audit, scripts/kernel-replay.sh (library)
• python3 scripts/testimony_lint.py, clean. It now knows the names the commands declare: L6 for proves, L9 for declare_*. scripts/test_testimony_lint.py passes, with 4 new tests.
• the same in arguments/, and scripts/kernel-replay.sh TestimonyArguments bibgen argtex statusgen argdoc
• bibgen, statusgen, argdoc, argtex, each with --check; mdbook build docs; examples/ builds
• scripts/bench.sh --runs 1: all 37 benchmarks elaborate
• the generated pages compared declaration by declaration: only boilerplate removed

Sources

None.

🤖 Generated with Claude Code

https://claude.ai/code/session_01SkMSatro8D3AXSRBAmEcVM