docs(errata): PR2 of 2 — attribution corrections from #4984 campaign errata

[phasetr]

Purpose

PR2 of 2 for the #4984 campaign errata effort (Codex final ruling in
.self-local/reports/dev-review-4984-post-triage-remainder.md: 2 PRs total,
<=20h combined budget). PR1 (10 issues) merged at main 6d63a472c8d75e245568f59c0f9a35f665c58306.
This PR is deliberately kept minimal given remaining budget: small attribution
corrections only, across the 4 issues below, plus a self-correction the review
process itself found (see below).

Scope

Refs #4989
Refs #4993
Refs #5007
Refs #5024

Change summary

Doc-string / comment / docs/index.md prose only across all 3 review rounds: 39 files
(38 .lean + docs/index.md), zero Lean code changed — every changed .lean file is
identical to main after stripping Lean comments (line --, nestable /- -/, /--, /-!,
string-literal aware), modulo blank-line bookkeeping inside comments. No declaration,
statement, proof, import or set_option is touched (dev-review round 3, task item 6: own
independent stripper, 38/38 hash-identical).

Page numbers were re-derived from the local PDFs in .self-local/refs/, not carried over from
the issues: GJ book = PDF − 16 in ch. 4 (PDF 73 heads 4.1 Griffiths Inequalities 57; PDF 79
heads 4.4 The FKG Inequality 63), FV book = PDF − 18 in ch. 3 (PDF 135 heads 3.7. Phase Diagram 117; PDF 162 heads 144 Chapter 3. The Ising Model).

#4989 / #4993 — GJ Corollary 4.3.5 is on book p. 63

PDF 79 (= book 63) carries the Corollary 4.3.5. statement, its full PROOF. and then
4.4 The FKG Inequality; nothing of 4.3.5 is on book p. 62. The 5 sites reading p. 62 are
corrected and one pp. 62-63 is tightened to p. 63; all 12 surviving Cor. 4.3.5 page citations
now read p. 63. Neighbouring corollaries were checked so that a blanket sweep could not hide:
book 61 = Corollary 4.3.3., book 62 = Corollary 4.3.4., both left alone.

#4993 / #5007 — GJ §4.2 has no "Proposition 4.2.4", and 4.2.3 is a Theorem

GJ §4.2 contains exactly Proposition 4.2.1 (book 58), Proposition 4.2.2 (book 58) and
Theorem 4.2.3 (book 59); the string 4.2.4 occurs 0× in the book. The J-monotonicity and
h-monotonicity citations Prop 4.2.4 (11 sites), Proposition 4.2.4 (9 sites) and
Prop 4.2.3 (2 sites) are re-anchored on Prop 4.2.1, p. 58 ("Let H be ferromagnetic. Then
⟨ξ^B⟩, considered as a function of the couplings J_A in H, is monotone increasing"). For the
h-direction the comment now points at GJ's own remark on book p. 58 (a positive external field
keeps the Ising measure ferromagnetic) together with the proof of Thm 4.2.3 on book p. 59 ("a
nonzero value J_A = h occurs for A = {a_i}"), i.e. h is a singleton coupling in GJ's
formalism, so Prop 4.2.1 does cover it. After this PR, 4.2.4 matches 0× in the repo.

#5007 — GKS-II is Theorem 4.1.3, (4.1.11), p. 57

Book p. 57 (PDF 73) has Theorem 4.1.1 → (4.1.9) 0 ≤ ⟨ξ^A⟩ (GKS-I only) and Theorem 4.1.3 →
(4.1.10) 0 ≤ ⟨q^A t^B⟩, (4.1.11) 0 ≤ ⟨ξ^Aξ^B⟩ − ⟨ξ^A⟩⟨ξ^B⟩ (GKS-II). The GKS-II citations
that named Thm 4.2.3 (a convergence theorem) are re-anchored on Thm 4.1.3, (4.1.11), p. 57,
matching the already-correct site in Concrete/.../TwoPointCorrelationInfinite.lean. The added
clause records that in the Ising case σ² = 1 turns (4.1.11) into the symmetric-difference form
⟨σ^A⟩⟨σ^B⟩ ≤ ⟨σ^{A△B}⟩ the repo uses.

#5024 — the random-current tree is anchored on FV §3.10.6, not §3.7 / (3.45)

FV (3.45) is the high-temperature (tanh) representation of the partition function: book p. 117,
§3.7.3, "The expression (3.45) is called the high-temperature representation of the partition
function", and FV §3.7 is "Phase Diagram". The random-current weight ∏_e (βJ)^{n_e}/n_e! and the
source set ∂_Λ n are in §3.10.6 "Random-cluster and random-current representations", book
pp. 143-145 (book 144 displays Z⁺ = 2^{|Λ|} Σ_{∂n=∅} ∏ β^{n_e}/n_e!; w(n) is defined in the
proof on book 145). Every Current.weight citation in IsingModel/RandomCurrent/** and
IsingModel/Inequalities/ClusterConditioning* is re-anchored ((3.45) / §3.7 now match 0× in
both trees; §3.10.6 appears at 110 sites repo-wide).

Two nonexistent pointers are removed in the same pass:

• GJ "Theorem 5.1.2" — matches 0× in the book (GJ §5.1 is "Pure and Mixed Phases", (5.1.2)
  is a displayed equation); dropped rather than replaced.
• "FV Theorem 9.35" (6 sites) — FV ch. 9 is "Models with Continuous Symmetry" and its numbering
  stops around 9.14; the switching lemma is FV Lemma 3.55, p. 144 ("Lemma 3.55 (Switching
  Lemma). Let Λ ⋐ Z^d, A ⊂ Λ, i ∈ Λ …").

The surviving (3.45) citations in ClusterExpansion/** and **/HighTemperature* are genuine
tanh(βJ)^{|X|} / evenSubgraphs high-temperature sums and were deliberately not swept.

Round-1 review fix (.self-local/reports/dev-review-errata-pr2-round1.md)

• High-1 (blocker, introduced by this branch). Three sites had swapped the nonexistent
  GJ §5.1 Thm 5.1.2 / FV Thm 9.35 for another nonexistent pointer, Aizenman 1982 Lemma 4.1.
  Aizenman 1982 has no Lemma 4.1 (§4 is the heuristic Gaussian-structure section; the only "(4.1)"
  is an unrelated Wick-identity equation), per .self-local/refs/Aizenman-1982-sec4-conditioning-extract.md:15-18.
  Each site is re-anchored on what it actually claims:
  RandomCurrent/Switching/Core.lean:9 → Aizenman 1982 Lemma 3.2, p. 7, eq. (3.5) (the
  switching lemma); Switching/SwitchingIdentities.lean:32,67 → FV Lemma 3.56, p. 145 /
  Aizenman 1982 Lemma 3.1, p. 7 (the fixed-total m ↦ n − m source-swap, not the switching
  lemma itself).
• Med-2. The §3.7 → §3.10.6 sweep is completed across the SL-D₁ cluster: 43 sites in the 7
  Inequalities/ClusterConditioning* modules plus docs/index.md:1793-1795.
• Med-3 / Med-4. In Inequalities/GHS/Truncated3Contraction.lean, GJ Cor 4.3.4 is on book
  p. 62 (not 61), and the GHS/GKS-II pair was crediting Cor 4.3.3 with
  ⟨σ_iσ_j⟩⟨σ_k⟩ ≤ ⟨σ_iσ_jσ_k⟩ — impossible, since Cor 4.3.3 assumes h_i ≡ 0 and |A|, |B|
  both even while here |B| = 1. Both defects are fixed at all five sites in that file and in the
  docs/index.md row that mirrors it.
• Med-5. docs/index.md:375 credited GKS-II to Thm 4.1.1 while :382 credited it to
  Thm 4.1.3 — same table, 7 rows apart. Line 375 now reads Thm 4.1.3, (4.1.11).

Self-correction: round-2/round-3 fix, commit dde4f087

Round 2 review (.self-local/reports/dev-review-errata-pr2-round2.md, High-A) found that the
round-1 fix above had, at 8 sites it re-anchored plus 5 same-file companion lines, itself
introduced or left Aizenman 1982 Lemma 4.1 — the very nonexistent citation this branch's own
evidence base rules out — making Switching/Core.lean internally inconsistent (a Lemma 3.2
module header next to sibling declarations still citing the nonexistent Lemma 4.1). Round 3
review independently re-verified every citation this branch authors against the primary
Aizenman 1982 PDF (not just the in-repo extract) and confirms the fix is correct
(.self-local/reports/dev-review-errata-pr2-round3.md §§0–4).

Commit dde4f087 re-anchors 13 of those branch-introduced Lemma 4.1 sites to
Aizenman 1982 Lemma 3.2, p. 7, eq. (3.5) (Switching/Core.lean:27,57,95,
Switching/GlobalSwitching.lean:23,46, Switching/GlobalSwitchingLimit.lean:29,170,290,
Switching/SourceFilters.lean:58, Switching/SupportGraph.lean:115,235,
Switching/PairFinset.lean:38, Inequalities/CurrentConnectivityRepresentation.lean:49,94),
drops 1 more nonexistent pinpoint at Inequalities/ClusterConditioningPivotal.lean:33,53
(cluster conditioning is Aizenman §9, not §3 — no safe lemma number exists there), and rewords
docs/index.md:1794,1795 to drop the same nonexistent pointer. It also fixes
Inequalities/GHS/GHSInequality.lean:35 (Corollary 4.3.4, p. 61 → p. 62), aligning
Inequalities/GHS/ internally. In total, 14 of the branch's own defective sites are fixed
(13 re-anchored + 1 pinpoint dropped); 28 remain, all pre-existing (not branch-authored),
deferred to #5032 (dev-review-errata-pr2-round3.md, "Med-2").

Residual defects deferred (out of this PR's scope)

Pre-existing defects, not introduced by this branch, inventoried with file:line evidence in
#5032:

• Aizenman 1982 Lemma 4.1: 28 sites remain after this branch's own 14-site fix above
  (dev-review-errata-pr2-round3.md, Med-2), all on lines this branch never authored.
• FV Prop 9.31 (no such proposition in FV): round-2/round-3 review's corrected inventory is
  7 docs/index.md rows + ~24 Lean lines (not the 9-site docs-only count errata: residual mis-attributions left out of PR #5031 (Aizenman "Lemma 4.1", GJ Cor 4.3.4 page, GKS-II rows, FFS "Thm 9.35", FV "Prop 9.31") #5032 originally
  recorded); 2 of the 9 original docs sites were fixed by this branch's own round-1/round-2 sweep,
  leaving 7 docs rows plus the Lean sites open. errata: residual mis-attributions left out of PR #5031 (Aizenman "Lemma 4.1", GJ Cor 4.3.4 page, GKS-II rows, FFS "Thm 9.35", FV "Prop 9.31") #5032's item 5 did not list the Lean sites at all,
  including 4 lines in RandomCurrent/Peeling.lean:12,230,254,466, a file this branch itself
  edited (round-3 review Med-1) — errata: residual mis-attributions left out of PR #5031 (Aizenman "Lemma 4.1", GJ Cor 4.3.4 page, GKS-II rows, FFS "Thm 9.35", FV "Prop 9.31") #5032 is extended with the full Lean inventory in this same
  clerk pass (see the issue for the corrected list).
• Lebowitz/Cor434.lean:23 + docs/index.md:657,1188 (Cor 4.3.4 page) — unchanged.
• docs/index.md:1281 (Thm 4.1.1 credited with both GKS-I and GKS-II) — unchanged.
• FFS "Thm 9.35" mislabel — unchanged; the local FFS PDF is still unextracted.
• New defect class found while verifying, not yet in any issue (round-3 review §9): GJ §5.1
  is used repo-wide as the anchor for the random-current / Simon–Lieb work stream, but GJ §5.1 is
  "Pure and Mixed Phases", book p. 72 — unrelated to random currents or switching. The correct GJ
  anchor for Simon–Lieb was not located. Out of scope for this PR; needs an issue-manager decision
  on where to track it.

Test plan

• lake build — PASS (4944 jobs, full run, commit dde4f087). The lakefile sets
  warningAsError = true plus weak.linter.mathlibStandardSet = true, so a successful build is
  itself the zero-warning guarantee. No added line exceeds 100 characters.
• lake env lean on every file touched by the round-2/round-3 fix — PASS, zero
  warning:/error: (round-3 review, independently re-run).
• Comment/prose-only proof — PASS: all 38 changed .lean files hash-identical to main after
  comment stripping, independently re-derived twice (implementer + round-3 review, own stripper).
• python3 scripts/citation_audit.py — PASS, ratchet: OK -- 37 finding(s) cleared, 0 new,
  coverage OK.
• python3 scripts/audit_gate.py --full — PASS (V1 no axiom, V2 no sorry/admit/native_decide,
  V3 13 capstones axiom-clean, V4 no Japanese in 1977 tracked files).
• Independent cross-review: 3 rounds (.self-local/reports/dev-review-errata-pr2-round{1,2,3}.md),
  round 3 verdict APPROVE the diff (round-3 review, .self-local/reports/dev-review-errata-pr2-round3.md).