Errata: 13 merged citations put Glimm-Jaffe Cor. 4.3.5 on p. 62 (it is on p. 63), and carry zero ratchet charges so no wave will reach them

[phasetr]

Errata issue for already-merged prose. Thirteen tracked locations cite Glimm–Jaffe
§4.3 Corollary 4.3.5 (and its proof) at book page 62. Corollary 4.3.5, its statement
and its entire proof are on book page 63; page 62 carries Corollary 4.3.4. Two of the
thirteen are in the public tex/proof-guide.tex. The affected modules carry zero ratchet
charges, and the wave mechanism of #4984 only visits charged files, so no future wave will
ever reach them.

Found by dev-review round 2 of PR #4988 (wave 2/26) as finding R2-F4, and independently
re-verified here with a page-scoped extraction (the reviewer's list of 10 is extended to 13 + 1
by three further spellings the single-line 4.3.5/p.~62 patterns miss).

Ground truth: page-scoped extraction from the PDF

Verified against .self-local/refs/Glimm.Jaffe.P428.Quantum_Physics-A_Functional_Integral_Point_of_View.pdf
by extracting one page at a time, so a running head cannot be mistaken for a running foot
(the flat OCR text alone is ambiguous on exactly this point, and the two readings differ by a page):

PDF page	first lines	contains
77	4.3 ~4 Inequalities / 61	—
78	62 / 4 Correlation Inequalities and the Lee-Yang Theorem	Corollary 4.3.4.
79	63 / 4.4 The FKG Inequality	Corollary 4.3.5. and Dropping negative terms from the right (B2 odd) …
80	64 / 4 Correlation Inequalities and the Lee-Yang Theorem	—

Page 77 opening with 61 while carrying §4.3 material settles the head/foot question: the running
head sits at the top, and book page = PDF page − 16. So Corollary 4.3.5 and the whole of its
proof, including the quoted sentence "Dropping negative terms from the right", are on book p. 63.

The thirteen wrong locations

file	line	text
IsingModel/Inequalities/Lebowitz/Cor435.lean	7	"The intermediate inequality of GJ's proof of Corollary 4.3.5 (p. 62):"
IsingModel/Inequalities/Lebowitz/Cor435.lean	12	"Derivation (GJ p. 62, "Dropping negative terms from the right (B₂ odd) and"
IsingModel/Inequalities/Lebowitz/Cor435.lean	25	"* Glimm–Jaffe, Quantum Physics, 2nd ed., §4.3, Corollary 4.3.5, p. 62"
IsingModel/Inequalities/Lebowitz/Cor435.lean	53	"in the proof of Corollary 4.3.5, p. 62): for ferromagnetic h ≥ 0, a set"
IsingModel/Inequalities/GHS/NPoint.lean	40	"* Glimm–Jaffe, Quantum Physics, §4.3, Cor. 4.3.5, p. 62 -/"
IsingModel/Inequalities/GHS/NPoint.lean	42	"/-- Cor. 4.3.5 (Glimm–Jaffe, §4.3, p. 62): for h = 0 and n + 2"
IsingModel/Inequalities/GHS/Truncated3Contraction.lean	25	"No Lebowitz inductive bound (GJ Cor 4.3.5, pp. 61–62) is needed here: that"
IsingModel/AmbientLattice/SpontaneousMono.lean	138	"Reference: Glimm–Jaffe §4.3 Corollary 4.3.5, p. 62. -/"
docs/index.md	653	"… GJ §4.3 Cor 4.3.5, p. 62, axiom discharged (PR #3911)"
docs/index.md	1082	"Cor 4.3.5 at infinite volume (Glimm–Jaffe §4.3 Cor 4.3.5 p. 62) …"
docs/index.md	1255	"… (GJ Cor 4.3.5 intermediate bound, p. 62)"
tex/proof-guide.tex	4778	Glimm--Jaffe, 2nd ed., \S4.3 Cor.~4.3.5, p.~62.
tex/proof-guide.tex	25169	\S 4.3 Corollary 4.3.5, p.\ 62.

One further location is imprecise rather than false and should be reviewed with them:

file	line	text
IsingModel/Inequalities/GHS/NPoint.lean	24	"(Glimm–Jaffe, §4.3, pp. 62–63) bounds an (n+2)-point correlation:" — the bound and its derivation are wholly on p. 63; the range needlessly includes the page of Cor 4.3.4

The fix in every case is the page number alone: p. 63 (p.~63 / p.\ 63 in the TeX).

Do NOT change these — they are correct

Two sites cite Corollary 4.3.4 at p. 62, which the extraction confirms is right:

• IsingModel/Inequalities/GHS/NPoint.lean:18 — "Cor. 4.3.4 (Glimm–Jaffe, §4.3, p. 62) states the truncated 3-point …"
• IsingModel/ContinuousSpin/Phi4.lean:186 — "Reference: Glimm–Jaffe, Corollary 4.3.4, p. 62. -/"

A blanket p. 62 → p. 63 sweep would break both. Any fix must be keyed on the corollary number.

Provenance, and why no gate and no wave can reach them

• git log -S pins every one of them to a single commit,
  8fa5d522061d9bb9701c5ca5420c946260d5dba1 = PR feat(gj-4.3): GJ Cor 4.3.5 inductive Lebowitz bound — discharge the lebowitz_inductive axiom — #3906 #3911 (feat(gj-4.3): GJ Cor 4.3.5 inductive Lebowitz bound — discharge the lebowitz_inductive axiom — #3906), merged 2026-06-12. They are
  legacy prose, not campaign output.
• header_inventory_claim_ratchet.py --findings charges 0 on all four affected Lean modules,
  and scripts/audit/header_claim_baseline.tsv has 0 rows for them. Batch-migrate the remaining stale header charges to intension-only prose (PR-3+ wave campaign, 16 waves: all merged; Lean lane at zero, docs lane D1 open/unscoped) #4984's wave population is
  the charged one, so no wave will open these files.
• citation_audit.py resolves repo identifiers, not literature page numbers, so nothing
  mechanical in this repository would ever flag a wrong book page. lake build never reads /-!
  or /-- prose. Every check of this class is manual.

The repo currently disagrees with itself

PR #4988 (wave 2/26) corrected IsingModel/Concrete/LatticeGraphCorrelation/UniformMagCorrelationTrivialCor4_3_5.lean
(lines 7, 17, 36) to p. 63. That file's frozen scope is why the thirteen above were left alone.
Until they are fixed, main asserts both pages for the same corollary — and docs/index.md:1082 is
the progress-table row for correlationInfinite_cor_4_3_5_h0, the direct parent of the two theorems
just corrected.

Why PR #4988 did not just fix them

PR #4988's file set is frozen (#4984: "editing any of them requires amending this list first, with
the reason"). Silently widening a wave's scope to absorb an unrelated find would destroy the
pre-registration guarantee that makes the ratchet numbers meaningful. The find is therefore filed
rather than absorbed — the same disposition #4987 took for wave 1's analogous out-of-scope errata.

Disposition to decide (not self-authorized)

1. One standalone errata PR for the fourteen sites (prose-only; the four Lean modules carry zero
   ratchet charges, so the pre-registered expectation is --check unchanged, which the PR body
   should state explicitly so a zero delta is not read as a no-op). tex/proof-guide.tex is public,
   so lean-tex-build applies and the TeX must still compile.
2. Amend a later wave's frozen file set to include them, with this issue as the recorded reason.
   Note this only covers the four Lean modules; docs/index.md and tex/proof-guide.tex are outside
   any wave's population either way.
3. Explicitly accept the discrepancy and close.

Recommended alongside any of the above

Round 2 of PR #4988 adopted, for waves 3–26, the rule that a newly asserted citation must be verified
against a page-scoped PDF extraction, never the flat OCR text and never another repo copy —
comparing repo copies degenerates into comparing thirteen copies of the same error, which is exactly
what happened here. A bounded audit of the remaining Glimm–Jaffe page citations against page-scoped
extractions is the proportionate follow-up; PR #3911's own citations are now known to be wrong in
every instance it introduced.

References

• Campaign: Batch-migrate the remaining stale header charges to intension-only prose (PR-3+ wave campaign, 16 waves: all merged; Lean lane at zero, docs lane D1 open/unscoped) #4984 (PR-3+ wave campaign); parent Refactoring re-audit: canonicalize the current code while preserving source-book coverage #4924; sibling errata issue Errata: six merged headers expand vd as "van-den-Berg" instead of "vertex-disjoint", and carry zero ratchet charges so no wave will reach them #4987.
• Wave 2 = PR docs(headers): wave 2/26 — LGC Uniform* family (#4984) #4988; finding R2-F4 in .self-local/reports/dev-review-4984-w10-round2.md;
  re-verification and the three additional locations in
  .self-local/reports/dev-implement-4984-w10-followup2.md.
• Origin of the error: PR feat(gj-4.3): GJ Cor 4.3.5 inductive Lebowitz bound — discharge the lebowitz_inductive axiom — #3906 #3911, commit 8fa5d522.

[phasetr]

Moot: the target file (tex/proof-guide.tex) that this errata was against has been removed entirely by PR #4995 (issue #4994). The citation/label defect this issue tracked no longer exists because the document carrying it is gone. Closing as not planned rather than completed, per the disposition note in PR #4995's body.