wave 12 of 16

[phasetr]

Refs #4984

Wave 12 of 16 — AmbientLattice/ Analyticity.lean umbrella + all AnalyticityLambda* children header rewrite

COMPLETE. Scope frozen against main @
93d92b7e77372814d1ac265bf24ba8764c942954 (wave 11 / PR #5016's merge commit); freeze detail:
#4984 (comment).

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

Analyticity.lean
AnalyticityLambdaBasicIdentities.lean
AnalyticityLambdaCapstones.lean
AnalyticityLambdaEpsilonIff.lean
AnalyticityLambdaJoint.lean
AnalyticityLambdaMagSuscep.lean
AnalyticityLambdaMayer.lean
AnalyticityLambdaMayerIdentity.lean
AnalyticityLambdaMayerPfeEdgeBounds.lean
AnalyticityLambdaMayerRecurrenceEpsilon.lean
AnalyticityLambdaPerDirection.lean
AnalyticityLambdaPfeSharpening.lean
AnalyticityLambdaPolymer.lean
AnalyticityLambdaPolymerBounds.lean
AnalyticityLambdaRegularity.lean
AnalyticityLambdaSandwich.lean
AnalyticityLambdaSection186.lean
AnalyticityLambdaTanhFerroIff.lean
AnalyticityLambdaVdPolymer.lean

git diff --name-only origin/main...docs/4984-w12-analyticity-headers equals exactly these 19
files plus scripts/audit/header_claim_baseline.tsv (the ratchet baseline) — no other path.

metric	value (final, re-verified against live --findings at head a2f9f8ea)
files	19
charges cleared	37 (19 NARROW_CHILD + 18 RELOCATION)
declarations	260 (re-derived independently by round-3 review from a fresh full read; the
scaffold's earlier 261 was off by one)
MISSING_MODULE_DOC	0 — 6th consecutive zero-authoring wave
ratchet	235 charges / 163 keys → 198 charges / 126 keys (exact charge count as
pre-registered; keys landed at 126, below the pre-registered ≤144 upper bound)

AmbientLattice/-specific checklist items — TOP BILLING (carried forward from wave 11, this wave is in the SAME tree)

Wave 11 (#5016) was the first campaign wave inside AmbientLattice/ and found 5 tree-specific
conventions with no analogue in the Concrete/LatticeGraphCorrelation/ waves 1–10. W12 is also in
AmbientLattice/, so these applied directly:

1. Vocabulary check runs inverted. Nothing in this tree is ℤ^d: files quantify over an
   arbitrary G : SimpleGraph V with {V : Type*} [DecidableEq V].
2. Every *AlongExhaustion description must state both branches of its dite.
3. Exhaustion is Monotone, never strictly increasing.
4. Λ may be overloaded within single files — Λ : Finset V vs Λ : Exhaustion V.
5. Expect stale citations from past deletion PRs in this tree.

Umbrella-specific note (new to W12, no wave-11 analogue)

Analyticity.lean carries 0 local declarations and 19 of the wave's 37 charges — it is a
pure umbrella whose entire content is claims about its 18 children. All 18 RELOCATION pointers
were verified against the live target module (existence + declaration count) across all four
review rounds, most recently in round 3's fresh independent re-derivation.

Review process — 4 rounds, final clean APPROVE both sides

This wave is a notable process-methodology case study within the campaign, alongside wave 9.

• Round 1 (.self-local/reports/dev-review-4984-w12-analyticity.md, head 491ff3d5):
  dev-review and independent Codex both CHANGES REQUESTED — 5 Med + 3 Low false header
  statements, and a genuine process failure: of 4 defects the implementer's own report claimed
  to have self-caught and repaired, 3 were never actually written into the tree — the report
  described the intended replacement text while the files still carried the original draft. This
  was caught only because the reviewer diffed the report's claims against the files themselves
  rather than trusting the report.
• Round 2 (.self-local/reports/dev-review-4984-w12-round2.md, head eafba79f): reviewed the
  round-1 fixes with a rigorous git show (blob of the pushed commit) + git log -S pickaxe
  verification protocol (never trusting the implementer's table) to confirm every one of the 8
  round-1 fixes was genuinely applied in the pushed commit object, not merely claimed — this
  protocol change prevented round 1's claimed-but-unapplied failure from recurring. The same round
  independently found 2 further genuine math errors (F1, F2): F1 in
  AnalyticityLambdaCapstones.lean is the more significant of the two — the round-1 fix (M2f)
  for a false "written out in each statement" universal itself introduced a new instance of the
  same defect class (a new false universal claiming 3 Mayer-filter statements were "phrased
  through mayerExpansionTerm" when the identifier occurs only in their names, not their
  statements). F2 was a separate false "nothing here treats a negative activity" claim across 3
  files, contradicted by the two-sided neighbourhood behaviour of AnalyticAt/ContinuousAt at
  the admissible boundary t = 0.
• Round 3 / final (.self-local/reports/dev-review-4984-w12-round3.md, head a2f9f8ea = PR
  HEAD): both F1 and F2 fixed in .self-local/reports/dev-implement-4984-w12-followup2.md.
  Round 3 is a fresh independent full re-derivation of all 19 headers' claims from the
  declarations by both reviewers (not a check of only the two named fixes) — dev-review
  APPROVE, independent Codex APPROVE, zero remaining findings on either side. Both reviewers
  confirmed the F1/F2 repairs did not relocate the error elsewhere, which is the specific failure
  mode this wave exhibited twice (the original M2f defect, then F1's reintroduction of it).

Campaign-methodology lessons this wave produced (recorded here and on the completion comment
on #4984):

1. Verification must check the actual pushed git commit (git show/git log -S), never trust
   a report's self-description of what it repaired — round 1's 3 claimed-but-unapplied fixes were
   real, and only round 2's pickaxe protocol caught and prevented recurrence of that failure mode.
2. A fix for defect class X can itself introduce a new instance of defect class X — F1 is
   exactly this: the fix for "false universal about statement phrasing" (M2f) shipped a new false
   universal about statement phrasing. Fixes need the same independent scrutiny as original
   content, not just self-testing.

Standing pre-review checklist (waves 1–11, unchanged)

Technical noun phrase resolved against a repo def; binder-level hypothesis scoping;
bare-cardinality idioms; same-file /-- ↔ /-! consistency; citations verified against
page-scoped PDF extraction, never flat OCR nor another repo copy; PR-body raw-HTML self-check; AC5
evidence inline with real numbers; blanket-disclaimer and anaphoric-reference precision; wave 6's
per-item scope-qualifier check on files carrying 2+ regime/layer tokens; wave 7's
exclusivity-claims-about-instance-binders check; wave 9's zero/nonzero mathematical
characterization check and no-negative-provenance-claims check; wave 10a/10b's
self-test-the-verification-instrument-adversarially-first methodology.

Acceptance criteria — final status

• AC1 (coverage) — PASS. Exactly the 19 frozen files; git diff --name-only shows no other
  path besides the ratchet baseline TSV.
• AC2 (ratchet) — PASS. --findings 0 charges on all 19 files; --check green at
  198 charges / 126 keys (from 235/163, −37 charges exact); --check-baseline-drift green
  (base = frozen main commit 93d92b7e); --self-test 184 tests OK, instrument unmodified.
• AC3 (header truth, 100%) — PASS. Every sentence of all 19 touched headers re-derived from
  declarations/proof terms by both reviewers independently across 3 review rounds; the umbrella's
  18 RELOCATION pointers each verified against the live target module (existence + declaration
  count); zero/nonzero characterization and no-negative-provenance checks clean; instance-binder
  exclusivity claims checked against actual binder lists; round 3 found zero remaining false
  claims.
• AC4 (zero Lean logic change) — PASS. Comment-stripped token stream, non-blank comment-stripped
  line list, and per-file import list byte-identical to the frozen main on all 19 files
  (independently re-verified by both round-2 and round-3 review); all non-blank diff lines fall
  inside comment spans.
• AC5 (gates, zero regressions) — PASS. lake build exit 0 zero warnings/errors (CI build
  7m6s green with warningAsError = true); import_dag_contract.py --check PASS, 0 baseline
  entries; audit_gate.py --full PASS (V1 1922 files, V2 1922 files, V3 13 capstones ⊆
  {propext, Classical.choice, Quot.sound}, V4 1977 tracked files); citation_audit.py PASS —
  findings 694, self-refs 112, ratchet 37 cleared, 0 new (no citation moved); grep -rn "sorry" IsingModel/ = 0; 0 Japanese in the 19 files; widest added line 93 codepoints (0 lines over 100).
• AC6 (review discipline) — PASS. dev-review + independent Codex reached a clean round with
  zero findings both sides at round 3 (.self-local/reports/dev-review-4984-w12-round3.md,
  Codex raw log .self-local/reports/codex-4984-w12-round3.log); full re-review after every fix
  across 3 rounds; per-file declaration subtotals reproduced by both reviewers independently.
• AC7 (falsification rule) — this wave needed 4 rounds (task-level count; 3 distinct review
  passes), tied with wave 9 for the most in the campaign so far. Per AC7, the next wave (W13)
  reverts to the largest declaration count smaller than 260, of the same work type (pure
  rewording), that has closed at ≤3 rounds under full attestation — recorded as a pending
  next-wave-sizing input, not actioned in this PR.
• AC8 (pre-review checklist) — PASS. Predicate noun phrases, binder-level hypothesis scoping
  (kernel telescope == source binder list for all 260 declarations), cardinality-idiom sweep,
  same-file /--↔/-! consistency, page-scoped citation verification, no raw HTML in this body,
  AC5 evidence filled with real numbers, all 5 AmbientLattice/-specific items above.

Errata filed, not fixed in-wave

#5019 (declaration-doc defects: provenance markers, unbalanced **, pFE/ε(t)/vdSum
shorthands) and #5020 (4 alpha-identical declaration pairs) — both out of this wave's frozen
scope, filed for future triage.

Docs/tex lane

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