test(audit-gate): assert per-directory scan coverage and re-derive the file-count floors (#4746 Item F1)

[phasetr]

Part of #4746 (Item F1). Test-only: scripts/test_audit_gate.py. No change to
scripts/audit_gate.py, no Lean rebuild.

Why now

CheckedFilesTest's blanket floors were calibrated a few dozen files below the
measured count, so every batch of the safe-to-delete lane had to lower them:
2003 / 1996 (#4749) -> 1993 / 1986 (#4751) -> 1984 / 1977 (#4754). That is the
ratchet describing the deletions instead of constraining them, and the standing
decision recorded in the file said the first batch that would actually trip a
floor must land F1 -- per-directory assertions -- rather than recalibrate again.

Re-measured independently on f8911169 (this PR's base) with
python3 -c "import audit_gate as ag; print(len(ag.iter_checked_files()), len(ag.iter_lib_files()), len(ag.iter_v4_files()[0]))":

counter	measured	old floor	deletions still allowed (assertGreater)
iter_checked_files()	1964	1957	6
iter_lib_files()	1957	1950	6
iter_v4_files()	1994	1977	16

The next ten-module batch trips two of the three floors, so this is that batch's
prerequisite.

What changed

F1-a — directory parity (no calibration). LIB_TOP_LEVEL_DIRS pins the 25
top-level IsingModel/ subdirectories, asserted twice: against a census of what
iter_checked_files() enumerates, and against an independent disk traversal
(LIB_DIR.iterdir() + rglob("*.lean")). The two are deliberately not the same
assertion -- deriving the expected set from the scan would be the
CAPSTONE_MIN_COUNT == len(read_capstones()) anti-pattern the suite already
refuses. Measured: 25 directories from the scan, 25 from disk, identical sets.
A filter such as if "Peierls" not in p.parts now fails by name at any
library size; when the lane empties a directory, scan and disk shrink
together, so no recalibration follows. Only a whole-top-level-directory deletion
(last one: #4703, IsingModel/LatticeSystemBridge) costs an edit, and that edit
is the point.

F1-b — coarse per-directory floors. Parity only requires one surviving file
per directory, so LIB_DIR_FLOORS adds a count floor for the eight directories
at 40+ files plus the loose bucket, at roughly 60-70 % of the measurement:

directory	measured	floor		directory	measured	floor
Concrete	843	600		Peierls	105	80
AmbientLattice	275	180		AmbientComplexAnalyticity	76	55
ClusterExpansion	205	150		Inequalities	71	50
TransferMatrix	109	80		Conditioning	48	35
				<top level> (loose)	39	25

assertGreaterEqual, unlike the strict blanket floors. Smaller directories get
no count floor: parity is the whole guard for them and a floor of "3" would be
noise.

F1-c — one-time re-derivation of the blanket floors. With directory loss now
asserted directly, the floors come from a budget instead of from the current
measurement: 200 further deleted modules (about 100 for the derived remainder of
the Item A lane, plus the excluded #4563 SpecialCases cluster, plus room for
cascade growth), rounded down to a multiple of ten.

constant	old	new	derivation
CHECKED_FILE_FLOOR	1957	1760	1964 - 200 -> 1760
LIB_FILE_FLOOR	1950	1750	1957 - 200 -> 1750
V4_FILE_FLOOR	1977	1790	1994 - 200 -> 1790

The floors are kept rather than deleted because they are the only assertions
that survive the two ways the exact git ls-files comparison can be made
vacuous: narrowing EXTRA_CHECKED_ROOTS and the suite's own ROOTS in one
commit, and a pathspec that matches nothing (set() - scanned is empty, so the
subset assertion passes trivially). Neither needs a tight floor. A new test
pins the floors' residual power as arithmetic: losing Concrete wholesale
(843 of 1964 files) must still take the count under CHECKED_FILE_FLOOR.

F1-d — mutation pairing. Two new mutations in MutationTest, per this
file's rule that every check is tested in the fixture and the mutation
direction, plus a LibraryCensusTest pinning the census helper on hand-built
paths (nested files, loose files, paths outside the library, missing bucket).

Verification

All commands run at d1f9ca7f.

• python3 scripts/test_audit_gate.py: 179 tests OK (skipped=1), 18.3 s
  -- 166 before, 18.6 s, so +13 tests at unchanged runtime.
• python3 scripts/audit_gate.py --self-test: OK (same 179).
• python3 scripts/audit_gate.py --full: PASS -- V1 1964, V2 1964,
  V3 13 capstones (axiom union {propext, Classical.choice, Quot.sound}),
  V4 1994. Run against the identical Lean tree of the base commit in the warm
  build tree, since V3 needs oleans; the change is Python-test-only and V1/V2/V4
  were additionally re-run on this branch's own tree with the same counts.
• rg -n "[Japanese ranges]" scripts/test_audit_gate.py: no match (V4 is green
  on the new file as part of the run above).

Injected-mutation check (that the new assertions really go red). Each
weakening was applied to scripts/audit_gate.py or to the pinned literal, the
new tests were run, and the file was restored (git diff clean afterwards):

injected weakening	result
iter_checked_files filtered on "TransferMatrix"	RED: test_the_scan_reaches_every_top_level_library_directory ("Items in the second set but not the first: 'TransferMatrix'") and test_every_large_directory_keeps_its_coarse_floor ("TransferMatrix is down to 0 scanned files (floor 80)"); disk-parity test stays green, as it must
Conditioning thinned to 3 files (45 removed)	RED: only test_every_large_directory_keeps_its_coarse_floor among the count assertions; directory parity and both blanket floors stay green -- exactly the gap F1-b exists to close
"Peierls" removed from LIB_TOP_LEVEL_DIRS	RED: both parity tests plus test_the_floor_table_names_only_buckets_that_exist
a non-existent name added to LIB_TOP_LEVEL_DIRS	RED: both parity tests, naming GhostDirectory

The two committed mutation tests are pinned by load_mutated, which raises if
its target text stops matching, so they cannot go vacuous.

Effect on the lane

Headroom after this PR: blanket 204 / 207 / 204 file deletions, Concrete 243,
and no count floor at all on the small directories (parity only). The remaining
Item A lane is about 100 modules, so no further recalibration is expected;
the next constant edit would be a deliberate top-level-directory deletion or a
shrink beyond the 200-module budget, which is a governance event by
construction.

Not included: the .self-local/issues/4746.md mirror entry for Item F1, which
is dev-pr-clerk's file and is being edited concurrently on another branch.

🤖 Generated with Claude Code