[deanberris]

The third item of the profiling plan, after #189 and #190.

Why

After round 6, simp was most of the elaboration time in the slowest modules, and most of that simp came from satisfied_by. Measured serially:

• 46 s of SolaFide.Dispute's elaboration;
• 24 s of SolaFide.Results'.

Its recipe unfolds the premise list and rewrites the semantics of every formula, which takes about a second for one sola fide case.

What changes

• Testimony.Logic.ModelCheck. A reading over an enumeration of claims is a table: True or False at each claim. tableOf reads that table off the definition at elaboration time, as a function to Bool. It also builds the proof that the table agrees with the reading, by cases, as a term rather than goal by goal. The kernel then evaluates every premise under the table with decide +kernel.
• models_iff_holdsB proves that this evaluation agrees with Foundation's semantics. satisfiable_of_table and independent_of_tables build on it.
• satisfied_by and leaves_open try the table first, and otherwise fall back to the old recipe. Their syntax is unchanged. I built once with the fallback disabled: no satisfied_by or leaves_open in the arguments or the examples falls back. The only fallback is the tactic module's own deliberate example, fun a => a = Pair.q.
• refute_with is unchanged, on purpose. The refutation check relies on refute_with unfolding every definition through the argument's unfold set. That is how it tells a genuine "not Horn" failure from a definition someone forgot to tag. A kernel check unfolds everything, tagged or not, so moving it would drop that guarantee silently.
• No new axiom. A first proof used tauto, which put Classical.choice under every model it checked. The generated pages print each theorem's axioms, and caught it. The proof is now constructive, so the theorems rest on propext and Quot.sound as before, and no generated page changes.
• Docs. The style guide now says to write a reading as a table, with the reason. The tactic docstrings, CLAUDE.md's layout table and ledger round 9 are updated. The citation check's pin moves from 2298 to 2304 definitions, the new module's.

Measured

scripts/bench-ab.sh origin/main, five interleaved rounds:

Benchmark	main	This PR	Change	p
satisfied_by: the Pauline case	1.11 s, 8 MiB	45 ms, 4 MiB	−96%	0.008
satisfied_by: Trent grants the subjective genitive	1.05 s, 8 MiB	46 ms, 4 MiB	−96%	0.008
leaves_open: parity leaves the canon open	204 ms, 4 MiB	15 ms, 2 MiB	−93%	0.008

By hand, two runs each, with only the tactic module's table alternative removed for the base:

• SolaFide.Dispute elaborates in 35.8 s, against 48.4 s;
• SolaFide.Results in 12.6 s, against 18.6 s.

The axiom audit now covers 9,670 declarations in the arguments, against 12,414. My reading is that the old recipe's simp proofs created auxiliary declarations. I haven't checked that declaration by declaration. Every theorem is still audited.

Round 7 is in #189 and round 8 in #190, so this is round 9. The ledger table and the pin in arguments/TestimonyArguments/Checks.lean will conflict trivially with whichever merges first.

Gates

All run locally on this head and all pass:

• lake build and lake build TestimonyTools;
• lake lint and lake exe axiom-audit, in all three packages;
• kernel replay, in all three packages;
• bibgen, argtex, statusgen and argdoc with --check, and exampletex --check;
• testimony_lint.py and mdbook build.

---

Generated by Claude Code