Errata: Glimm-Jaffe Theorem 4.2.3 is the convergence theorem, not GKS-II, and there is no Proposition 4.2.3

[phasetr]

Found while doing the page-scoped citation verification for the #4984 header campaign
(wave 9, LGC Two*/Base*/Site*, PR #5006). One site of this class was inside that
wave's frozen 37-file set and is repaired there; every site listed below is outside
it and is filed here rather than absorbed, following the #4987 / #4989 / #4991 / #4993 /
#4998 / #5005 precedent.

Verification method: page-scoped extraction (pdftotext -f N -l N on
.self-local/refs/Glimm.Jaffe.P428.*.pdf), never the flat OCR text. In the chapter-4
region book page = PDF page − 16 (PDF 72 = book 56, PDF 73 = 57, PDF 74 = 58,
PDF 75 = 59). Anyone re-checking must re-measure the offset in the region they read.

Revision (PR #5006 round 2). Three corrections to this issue's own prose, from an
independent re-extraction: the GKS-I attribution below was wrong (it is Theorem 4.1.1,
not equation (4.1.10)); the site inventory was incomplete (docs/index.md:398 and
docs/index.md:1438 were missing); and the "correct at five sites" count understated
the correct uses by more than half. The six defect sites and the disposition are
unchanged.

What Glimm-Jaffe §4.1-§4.2 actually contains

• Theorem 4.1.1, book p. 57 (PDF 73): "Let H be ferromagnetic, let dμ_i(ξ_i) be
  symmetric under ξ_i → -ξ_i, and let (4.1.4) be satisfied. Then all moments are
  nonnegative: 0 ≤ ⟨ξ^A⟩ (4.1.9)." This is GKS-I.
• Lemma 4.1.2, book p. 57: 2^{|A|/2}(ξ^A ± χ^A) = (q + t)^A ± (q - t)^A is
  ferromagnetic in the duplicate variables q, t.
• Theorem 4.1.3, book p. 57 (PDF 73): "With the same assumption as the previous
  theorem, 0 ≤ ⟨q^A t^B⟩ (4.1.10), 0 ≤ ⟨ξ^A ξ^B⟩ − ⟨ξ^A⟩⟨ξ^B⟩ (4.1.11)."
  (4.1.11) is GKS-II; (4.1.10) is the duplicate-variable inequality in q, t that
  Glimm-Jaffe prove first and then use to derive (4.1.11) — it is not a second statement
  of GKS-I. For Ising spins σ² = 1, so σ^A σ^B = σ^{A∆B} and (4.1.11) is exactly the
  repository's symmetric-difference form.
• Proposition 4.2.1, book p. 58 (PDF 74): correlations are monotone increasing in
  the couplings J_A.
• Proposition 4.2.2, book p. 58: Ising couplings are ferromagnetic, correlations
  are at most 1.
• Theorem 4.2.3, book p. 59 (PDF 75): "Let 0 ≤ h in (4.2.2). As Λ ↑ ℝ^d, the
  correlation functions (4.2.1) of the Ising model converge." This is a convergence
  theorem. It is not an inequality and it is not about J-monotonicity.
• §4.3 begins immediately after Theorem 4.2.3 on p. 59. There is no Proposition 4.2.3 and
  no Proposition 4.2.4 (the latter is Errata: Glimm-Jaffe Proposition 4.2.4 does not exist, and Corollary 4.3.5's page is 63 not 62 #4993's subject).

A. GKS-II attributed to Theorem 4.2.3

Theorem 4.2.3 is convergence, not the second Griffiths inequality. The correct source is
Theorem 4.1.3, (4.1.11), p. 57.

• IsingModel/AmbientLattice/CorrelationInfinite/GKSSecondPrelude.lean:24 — module header,
  "Reference: Glimm-Jaffe, Quantum Physics §4.2 Theorem 4.2.3 (GKS-II for the
  infinite-volume limit)". The Friedli-Velenik Thm 3.49 pointer on the next line is not
  checked here.
• docs/index.md:382 — table row "GKS-II at ∞-vol (Thm 4.2.3)".
• docs/index.md:1147 — "GKS-II at infinite volume (Glimm-Jaffe §4.2 Thm 4.2.3)".
• docs/index.md:1284 — the §4.2 progress row lists correlationInfinite_gks_second
  (GKS-II) under "Thm 4.2.3 (thermodynamic limit)". Here the row label is right and the
  membership is the defect: exhaustion-independence belongs under 4.2.3, GKS-II does not.

Repaired in PR #5006 (in the frozen set, so not left to this issue):
IsingModel/Concrete/LatticeGraphCorrelation/TwoPointCorrelationInfinite.lean, whose
GKS-II docstring now cites "§4.1 Thm 4.1.3, p. 57, in its Ising symmetric-difference
form".

B. "Proposition 4.2.3" for J-monotonicity

There is no Proposition 4.2.3; 4.2.3 is a Theorem and is about convergence. The correct
source for J-monotonicity is Proposition 4.2.1, p. 58.

• IsingModel/Concrete/LatticeGraphCorrelation/LatticeMassHighTemperature/PosAndAntitone.lean:135
  — "(correlationInfinite_monotone_J, GJ Prop 4.2.3)".
• IsingModel/Concrete/LatticeGraphCorrelation/LatticeMassHighTemperature/PosAndAntitone.lean:137
  — "Reference: Glimm-Jaffe §17.1 pp. 304-306; §4.2 Prop 4.2.3 (J-monotonicity)". The
  §17.1 page range on that same line is Errata: 130 tracked lines cite Glimm-Jaffe §17.5 at pp. 304--306 (§17.5 is pp. 310--312; Lemma 17.5.2 is pp. 311--312), and no wave will reach them #4991's subject and is not re-derived here.

Full inventory of 4.2.3 in the tree

grep -rn '4\.2\.3' over IsingModel/, docs/index.md and README.md returns 20
lines: 6 defects (above), 2 under-qualified analogies, 12 correct uses. The
count matters because it is what forbids a blanket replacement.

site	class
AmbientLattice/CorrelationInfinite/GKSSecondPrelude.lean:24	defect (A)
.../LatticeMassHighTemperature/PosAndAntitone.lean:135,137	defect (B)
docs/index.md:382,1147,1284	defect (A)
.../FiniteVolumeCorrelationMonotonicityConvergent.lean:24	under-qualified analogy
docs/index.md:1438	under-qualified analogy
.../TwoPointCorrelationInfinite.lean:12,39	correct (in the wave-9 frozen set)
.../FiniteVolumeCorrelationMonotonicityConvergent.lean:14	correct
IsingModel/InfiniteVolume/Lattice.lean:15,21,28,75,129	correct
IsingModel/InfiniteVolume/MonotoneJ.lean:144,156,173	correct
docs/index.md:398	correct

The two under-qualified analogies.
FiniteVolumeCorrelationMonotonicityConvergent.lean:24 ("GJ §4.2 Thm 4.2.3 (J → ∞ along
ℕ)") and docs/index.md:1438 ("the direct GJ §4.2 Thm 4.2.3 specialization (J → ∞ along
ℕ)") both transpose the theorem from the volume direction (Λ ↑ ℝ^d) into a parameter
direction at fixed Λ. That transposition is real mathematics in this repository and the
theorem number is the right pointer for it, but neither line says it is a transposition,
whereas line 14 of the same file does ("taken here in a parameter direction at fixed Λ
rather than in the volume direction"). They are listed as a register weakness, not as
defects. docs/index.md:1438 additionally says "Prop 4.2.4 companion", which is #4993's
subject and is not re-derived here.

The correct uses. InfiniteVolume/Lattice.lean and InfiniteVolume/MonotoneJ.lean
cite Theorem 4.2.3, p. 59, for convergence statements — right on content and page.
docs/index.md:398 is the section heading "### §4.2: Thermodynamic limit of correlations
(Thm 4.2.3)" — right on content. TwoPointCorrelationInfinite.lean:12,39 attribute
exhaustion-independence to 4.2.3 as a corollary of the convergence theorem — right.

Suggested disposition

Site by site, not by blanket search-and-replace. Of the 20 lines carrying the string
4.2.3, 12 are correct and 2 more are correct-but-under-qualified, so a sweep would
break 14 lines to fix 6. #4993's own note about this failure mode applies here too. The
mathematics is fine everywhere; only the labels are wrong.

Reachability by the #4984 campaign

Not derived here and must not be assumed. Two of the .lean sites
(GKSSecondPrelude.lean, PosAndAntitone.lean) are in the Lean lane and may or may not
carry a ratchet charge in a later wave's frozen set; the four docs/index.md sites are in
the docs lane, which #4984 explicitly does not cover.

[phasetr]

Scoped into PR #5031 (docs(errata): PR2 of 2 — attribution corrections from #4984 campaign errata), draft, branch docs/4984-errata-pr2-attribution off main 6d63a472c8d75e245568f59c0f9a35f665c58306. Not yet implemented; this comment is scaffold-only scope confirmation.

[phasetr]

Resolved by #5031 (merged at main 1cd2ffd13298ba5674f44672f2ab5207b55968b8).

• The Prop 4.2.3 sites (2, nonexistent — 4.2.3 is a Theorem) are re-anchored on
  Proposition 4.2.1, p. 58, together with the Errata: Glimm-Jaffe Proposition 4.2.4 does not exist, and Corollary 4.3.5's page is 63 not 62 #4993/Part-A Prop 4.2.4 sweep (same
  J-monotonicity claim, same correct anchor).
• The GKS-II sites that named Thm 4.2.3 (a convergence theorem, not an inequality) are
  re-anchored on Theorem 4.1.3, (4.1.11), p. 57, matching the already-correct site in
  Concrete/.../TwoPointCorrelationInfinite.lean. docs/index.md:1284 (renumbered from the
  earlier :1281) now explicitly disambiguates: "correlationInfinite_gks_second is filed with
  [Thm 4.2.3] as the ∞-vol lift of GKS-II (§4.1 Thm 4.1.3, (4.1.11), p. 57); it is not part of
  Thm 4.2.3" — the dual-attribution row this issue flagged is fixed.
• GKS.lean's reference block still lists only Theorem 4.1.1 (GKS-I); gks_second's own module
  documents Thm 4.1.3 directly, so the citation is complete at the point of use.

Source: .self-local/reports/dev-implement-errata-pr2.md, PR #5031 body ("#5007" section).
No remaining open sub-scope. Closing as completed.