docs(mirror): record #4746 Item A batch 3 (#4751) and the ratchet-slack decision point

[phasetr]

Summary

Records #4746 Item A batch 3 (PR #4751, main 051aa857) in the local issue mirror.
.self-local/issues/4746.md only; no Lean source, no docs/, no tex/, no
scripts/ file is touched, so no library gate can move.

What the entry records

• The ten deleted modules (724 lines / 39 declarations), the ten dropped import lines,
  and the Moved: doc-block corrections in eight surviving siblings.
• Condition (ii): the eight survival-count retractions in docs/index.md and
  tex/proof-guide.tex, plus the eight stale survival-location module names the
  follow-up commit corrected, and the three that were deliberately left alone.
• Condition (i): --lean was not reported in the PR body, so the tier-1 audit ran it
  against a green pre-deletion build — no consumer seen by Lean was missed on a
  safe-to-delete verdict.
• Gates re-run on the merged main: lake build 5,015 jobs / 0 warning / 0 error
  (5,025 before, difference exactly ten), citation_audit.py PASS with 960 gating
  findings and ratchet 0/0, dead_candidate_scan.py --self-test 100 OK,
  test_audit_gate.py 166 OK, lake exe GKSTest pass, #print axioms std-3 only.
• The one PR-body number that was wrong (grep -rn "sorry" IsingModel/ claimed 4 prose
  hits, actual 2) and its correction in the squash message.

Two findings carried into the mirror

The recorded Item A denominator no longer reconciles. Subtracting batches 1-3 from
the recorded 64 leaves 39, but a full-tree sweep on the merged main reports 205
fully-dead modules excluding Lemma_17_5_2 (231 on the pre-merge main), and
recomputing the same quantity from the tier-2 report's own stored verdicts gives 178
against a recorded 75. The rule behind the recorded figure is not recoverable from the
stored data, so the denominator should be re-derived and written down before batch 4 is
scoped.

F1 is now due rather than deferrable. Measured slack after batch 3 is 36 / 36 / 46
against CHECKED_FILE_FLOOR / LIB_FILE_FLOOR / the new V4_FILE_FLOOR; one more
ten-module batch takes it to 26 / 26 / 36 and two more exhaust the named floors.

Also carries a cascade warning: 30 declarations became reference-0 as a consequence of
batch 3, six of them abstract GJ §18 statements in
IsingModel/ClusterExpansion/MayerCore/Terms.lean, which a later batch must not sweep.

Part of the mirror upkeep for #4746.

🤖 Generated with Claude Code