[deanberris]

Part of #176. The first of three changes from profiling Meanings.SolaFide and SolaFide.Dispute.

Why

Meanings.SolaFide took 64 s, and 51 s of it was one proof: that the pinned exclusions are exactly what the meanings contain. The kernel checked it by testing all 6,105 pairs of the argument's 111 claims for a clash.

Two first guesses were wrong; both are recorded in the ledger so nobody tries them again:

• That the kernel re-closed each meaning for every pair. A literal table of closed meanings, and one of their coherence, each checked once, changed nothing: 44 s.
• That closing the meanings was the cost. It takes 0.4 s for all 111 claims.

The cost was the clash check itself. It compares whole facts and terms a field at a time, about 100 µs a comparison, some 400,000 comparisons in all.

What this does

Two coherent meanings can clash only where they touch. Seen as a graph, claims meet through their keys:

• a literal meets its negation in one fact;
• a definition's rule (only, functional) relates two facts about one thing;
• a nogood is completed by the other meaning's literal.

The changes:

• Ontology.Key, keysOf, shares_of_clash: a meaning's keys, and the proof that two coherent meanings that clash share one.
• HasMeanings.exclusionsUnder: each meaning is closed once (shapedUnder), then the claims are taken from the last to the first, against an index from keys to the later claims holding them. Each claim is checked only against the claims it shares a key with.
• The definition is kept as exclusionsByPairs. exclusionsUnder_eq proves the two are the same list, pair for pair and in order. So every pin stands unchanged, and no argument, statement or generated file changes.

The entailments were tried the same way, indexed by each claim's first literal. They gained only 9.7 s → 8.3 s, because their check already stops at the first literal missing. The loop over pairs is their cost, and the index doesn't remove it, so they're left as they are and recorded in the ledger.

A regression CI caught, fixed

The first push closed each later claim's meaning again for every claim before it, inside the walk. The kernel shares those repeated terms, so the proof was not slowed. But #check_ontology runs the same function compiled, once per definition, and paid for every closing. CI's benchmark gate found it 5.1% slower than main (p = 0.008). The second push closes each meaning once, before the walk, and the proof of equality carries over.

Measured

scripts/bench-ab.sh origin/main, five interleaved rounds, on the current head. Result: IMPROVED, nothing worse.

Benchmark	main	This PR	Change	p	Peak memory
Sola fide exclusions, 111 claims (new)	45.4 s	10.6 s	−77%	0.008	3.43 → 1.06 GiB
Checks: ontology	3.16 s	1.69 s	−47%	0.008	24 → 24 MiB
The other three checks	—	—	within noise	≥ 0.22	unchanged

Measured by hand on the first push, clean, on the same machine:

	Before	This PR
Meanings.SolaFide	64 s	24 s (31 s in the parallel build)
Arguments, lake build	225 s, 13.8 GiB peak	204 s, 10.9 GiB peak
Arguments, kernel replay	9.3 GiB peak	6.9 GiB peak, 226 s

The exclusions proof was the largest single holder of memory in both the build and the replay.

The round is recorded as round 7 in docs/src/performance.md. The semantics chapter says how the exclusions are found.

Also

A pin: #check_citations in the arguments now scans 2,319 definitions.

Checks

All pass on the current head:

• lake build, including TestimonyTools, the arguments and the examples
• lake lint and lake exe axiom-audit, in all three packages
• scripts/kernel-replay.sh, in all three packages
• scripts/testimony_lint.py
• bibgen, argtex, statusgen and argdoc with --check, and exampletex --check
• mdbook build docs

---

Generated by Claude Code