wave 11 of 16

[phasetr]

Refs #4984

Wave 11 of 16 — AmbientLattice/ BetaDerivative* + MagnetizationInfinite* (incl. subdirectory) header rewrite

Scaffolding-only draft, now complete. Scope frozen against main @
972e7463f48f0ca687b5dde564c88adc37016623 (wave 10b / PR #5010's merge commit); freeze detail:
#4984 (comment)

Final scope (14 files, all under IsingModel/AmbientLattice/)

BetaDerivative.lean
BetaDerivativeFieldJ.lean
BetaDerivativeMagnetization.lean
BetaDerivativePartitionSusc.lean
MagnetizationInfinite/HSymmetryBounds.lean
MagnetizationInfinite/JZeroRegularity.lean
MagnetizationInfinite/TrivialSlices.lean
MagnetizationInfiniteEmptyTrivial.lean
MagnetizationInfiniteExhaustionHSymmetry.lean
MagnetizationInfiniteHZeroJZero.lean
MagnetizationInfiniteLambdaHSymmetry.lean
MagnetizationInfiniteMagTrivial.lean
MagnetizationInfiniteSusceptibility.lean
MagnetizationInfiniteSusceptibilityRegularity.lean

git diff --name-only origin/main...origin/docs/4984-w11-magnetizationinfinite-headers = exactly
the 14 files above plus scripts/audit/header_claim_baseline.tsv (the ratchet baseline) — no other
path.

metric	value
files	14
charges cleared	27 (10 NARROW_CHILD + 10 RELOCATION + 6 PAREN_COUNT + 1 POSSESSIVE_COUNT)
declarations	87
MISSING_MODULE_DOC	0 — 5th consecutive zero-authoring wave (pure rewording throughout)
ratchet	262 charges / 190 keys → 235 charges / 163 keys
review rounds	2 (round 1: Med-1 + Low-1/2/3 found and fixed; round 2: clean APPROVE both sides)

Per-family subtotals:

family	files	charges	declarations
BetaDerivative* (direct .lean)	4	6	23
MagnetizationInfinite/ (subdirectory)	3	7	11
MagnetizationInfinite* (direct .lean)	7	14	53
total	14	27	87

Review history

Round 1 (dev-review + independent Codex, head d3a8e8bf): 1 finding on each side, same
finding reached independently by different routes.

• Med-1 (MagnetizationInfiniteSusceptibility.lean:19-21) — the stagewise paragraph described
  only the covered branch of susceptibilityAlongExhaustion's dite, asserted the summand count
  strictly grows (an Exhaustion only guarantees Monotone, not strict growth), and asserted the
  family is unbounded above (no declaration in the module establishes this — same defect class as
  errata Errata: four prose defects in AmbientLattice declaration docs (malformed cardinality identity, J=0 mislabelled as infinite temperature, unproved susceptibility bound, nonexistent mathlib lemma cited) #5017's E3). Fixed: the paragraph now states both branches of the dite, derives
  "covered from some stage on, 0 before" from mono + exhaust, states the summand count is
  nondecreasing but need not increase, contrasts with correlationAlongExhaustion/
  magnetizationAlongExhaustion (hypothesis-free ≤ 1 bounds), and replaces the unboundedness
  assertion with the checkable statement that no declaration in the module bounds the family
  above.
• Low-1 (BetaDerivativePartitionSusc.lean:6) — title said "energy"; the declaration
  (freeEnergyAlongExhaustion → freeEnergyΛ → IsingModel.freeEnergy) is the free energy. Fixed
  to "free energy", within the file's 94-codepoint line-length convention.
• Low-2 — the cardinality-idiom sweep's reported "0 surviving" was scoped to the
  definite-article/both pattern (14 hits, 14 fixed); article-less and sentence-initial forms
  (3 instances) were independently re-verified true, not silently assumed.
• Low-3 — the implementer's citation_audit.py advisory count was corrected from 1 (a tail
  truncation artefact) to the true figure 30 NEW SELFREF rows, all in docs/index.md, none
  attributable to this PR (this branch changes no docs/index.md and adds/removes no tracked
  .lean file, so the target text and resolution set are byte-identical to main). Gating figures
  unaffected: findings 694, self-refs 112, "37 cleared, 0 new", PASS.

Round 2 (dev-review + independent Codex, head b3bf53b2): 2 files changed, +9/−5, entirely
inside /-! … -/ module headers (AC4-verified comments-only vs both main and round-1 head).
Verdict: clean APPROVE, both sides, zero new findings. Every sentence of the Med-1 replacement
was independently re-derived from the declarations (dite branches, Exhaustion.mono/.exhaust,
the two hypothesis-free sibling ≤ 1 lemmas, the module's actual declaration list) rather than
taken from the round-1 prose.

Notable finding: a genuine phantom-citation, traced to its source deletion

MagnetizationInfiniteSusceptibility.lean's pre-existing header cited a name,
susceptibilityInfinite_apply, that no longer exists in the repo. Traced to source: the
declaration was real and was deleted by main commit 1793e549
("refactor: remove 97 dead decoration lemmas + 2 unused imports (2026-07-17 tier2 cycle) (#4536)"),
which removed exactly the theorem susceptibilityInfinite_apply block and touched no other line of
the file — the header that cited the name was left untouched. lake build never reads comments, so
no gate in the repo could have caught the resulting staleness; it is undetectable by build and was
found only by header-vs-declaration-list cross-referencing during this wave's review.

Of the three _apply aliases that #4536 removed in one pass, only this one still carried a
surviving prose citation 24 days later (two occurrences: this file's header and
MagnetizationInfinite/HSymmetryBounds.lean). The other two left no residue. So the failure mode
is not "deletion PRs always strand citations" — it is that nothing in the repo's gates measures
whether they do; survivors are invisible until a header is read against the current declaration
set. This wave fixed both stale citations.

New-tree checklist items (for waves 12–16, if they touch AmbientLattice/)

This is the first campaign wave inside AmbientLattice/; the following are specific to this tree
and have no analogue in the Concrete/LatticeGraphCorrelation/ conventions waves 1–10 established:

1. Vocabulary check runs inverted. Nothing in this tree is ℤ^d: every file quantifies over an
   arbitrary G : SimpleGraph V with {V : Type*} [DecidableEq V]. Lattice vocabulary (ℤ^d,
   lattice, latticeGraph, cubic) is an error here, whereas in Concrete/ its absence was
   the error.
2. Every *AlongExhaustion description must state both branches of its dite. Med-1 above was
   exactly a header describing only the covered branch; make "states the uncovered branch too" an
   explicit pre-review item for this family.
3. Exhaustion is Monotone, never strictly increasing. "Grows"/"increases"/"the volumes
   expand" prose is false in general (a constant Finset.univ on a Fintype carrier is a valid
   exhaustion). Permitted forms: "nondecreasing", "covered from some stage on", "0 before that".
4. Λ is overloaded within single files — Λ : Finset V (with
   [Fintype (inducedGraph G Λ).edgeSet]) and Λ : Exhaustion V (with
   [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]) coexist; 3 of this wave's 14 files mix
   them. Any instance-binder claim must be stated per group, not blanket across the file.
5. Expect more stale citations from past deletion PRs in this tree, per the phantom-citation
   finding above; a cheap detector is to extract every backticked token from a produced header and
   resolve each against the live repo declaration set.

Acceptance criteria — final status

• AC1 (coverage) — PASS: exactly the 14 frozen files; git diff --name-only confirms no other
  path besides the ratchet baseline TSV.
• AC2 (ratchet) — PASS: --findings 0 charges on all 14 files; --check green,
  235 charges / 163 keys (from 262/190, −27 charges exact); --check-baseline-drift green
  (base 972e7463 via origin/main); --self-test OK, 184 tests, instrument unmodified.
• AC3 (header truth, 100%) — PASS after round-2 fix: every sentence of both touched headers
  re-derived from declarations/proof terms by both reviewers independently; zero/nonzero
  characterization and no-negative-provenance checks clean; instance-binder exclusivity claims
  checked against the actual binder lists (item 4 above).
• AC4 (zero Lean logic change) — PASS: comment-stripped token stream, non-blank comment-stripped
  line list, and per-file import list byte-identical to main on all 14 files (round 1) and to
  round-1 head on the 2 round-2-touched files; all non-blank diff lines fall inside comment spans.
• AC5 (gates, zero regressions) — PASS on final tree, nothing running concurrently:
  • lake build: exit 0, 4944 jobs, 1033 modules rebuilt, zero warnings, zero errors.
  • lake exe GKSTest: exit 0, "=== All tests passed ===".
  • audit_gate.py --full: exit 0 — V1 no axiom (1922 files), V2 no sorry/admit/native_decide
    (1922 files), V3 13 capstones PASS (axiom union = {Classical.choice, Quot.sound, propext}),
    V4 no Japanese (1977 tracked files).
  • citation_audit.py: exit 0 PASS, findings 694, self-refs 112, "37 cleared, 0 new"; 30
    non-gating NEW SELFREF advisories, all pre-existing in docs/index.md, none attributable to
    this PR (see Low-3 above).
  • import_dag_contract.py --check + tests: PASS, 0 baseline entries.
  • grep -rn "sorry" IsingModel/: 0.
  • header line width: max 94 codepoints across all touched files, 0 lines over 94.
  • all edited prose: English only, 0 Japanese codepoints in IsingModel/AmbientLattice/.
• AC6 (review discipline) — PASS: dev-review + independent Codex to a clean round 2 (zero
  findings both sides); full re-review after the round-1 fix; per-family D/D subtotals reported
  (table above); dev-issue-manager-style resolution verification folded into round-2 review's
  independent re-derivation of every claim.
• AC7 (falsification rule) — not triggered: closed at round 2 (≤3-round bound).
• AC8 (pre-review checklist) — PASS: predicate noun phrases, binder-level hypothesis scoping
  (kernel telescope == source binder list for all 87 declarations), cardinality-idiom sweep
  (measured, corrected in round 1 per Low-2), same-file /--↔/-! consistency, page-scoped
  citation verification, no raw HTML in this body, AC5 evidence filled with real numbers.

Errata filed (frozen /-- blocks, tracked separately, not blocking this PR)

Issue #5017 (OPEN) — four pre-existing prose defects in /-- declaration docs (not module
headers) discovered while reading this wave's 87 declarations. This wave's AC deliberately freezes
all /-- … -/ blocks (module-header-only rewrite), so these are recorded as errata rather than
fixed here. All four characterizations independently re-verified accurate by round-1 review.

Docs/tex lane

Untouched by this PR (docs/index.md and tex/proof-guide.tex remain a separate, later lane per
the design report; never bundled with this Lean-lane wave).