docs(errata): #5032 PR-A — mechanical citation fixes (Aizenman/GJ/FFS pinpoints) by phasetr · Pull Request #5033 · phasetr/ising-model

phasetr · 2026-08-12T00:06:50Z

Purpose

PR-A of the errata campaign scoped in #5032 (dev-issue-manager scoping freeze,
2026-08-12, against main 1cd2ffd1): mechanical re-anchoring of doc-comment /
docs/index.md citations whose correct target was already established, with no
proof-term or statement changes. Items 5 and 7 (Simon–Lieb anchor, gated on a
dev-research dispatch) are explicitly out of scope and remain for PR-B.

Scope — 6 items fixed (55 sites / 20 files)

Aizenman "Lemma 4.1" → 5 content buckets — 37 lines / 12 files, per-site
classified (not a blanket rename) into Aizenman Lemma 3.2 (p. 7, eq. (3.5),
switching lemma), Lemma 3.1 (p. 7), Proposition 3.1 (eq. (3.2), p. 6),
Proposition 9.2 (p. 24, eqs. (9.5)–(9.7)), or §9 Lemma 9.2 (p. 25, eq. (9.11)) /
Lemma 9.3 (pp. 25-26), each verified against
~/junk/0-pdf-for-translation/Aizenman.1982.p48....pdf.
GJ Corollary 4.3.4 mis-paginated — 4 sites / 3 files corrected to book p. 62
(old p. 61 / pp. 68ff were both wrong; printed p. 62 running head verified
first-hand), including IsingModel/AmbientLattice/TruncatedFunctions/ThreePoint.lean:24.
GKS-II dual attribution — IsingModel/Inequalities/GKS.lean:10 now also
names GJ Theorem 4.1.3 / (4.1.11), p. 57, alongside the existing FV Theorem 3.49
citation (which already covered GKS-II; the defect was GJ's own GKS-II theorem
never being named).
FFS "Thm 9.35"/"Lemma 9.36" → displayed equations — 9 sites / 4 files
corrected to FFS eq. (9.35), ch. 9, p. 198 / eq. (9.36), p. 199 (verified against
.self-local/refs/Fernandez.Frohlich.Sokal.1992.p465.*.pdf pp. 198-199: both are
numbered displays, not theorems/lemmas).
5b. Misused FV (3.45) — 1 site,
SourcefreeConnectionLebowitzConvolutionBound.lean:72, pinpoint removed.
GKS-II i = j / GJ Prop 4.2.1 mislabeling — 2 sites
(GHS/TruncatedDefs.lean:172, FiniteVolumeCorrelationMonotonicity.lean:70-71),
migrated from Errata: Glimm-Jaffe Proposition 4.2.4 does not exist, and Corollary 4.3.5's page is 63 not 62 #4993's round-2 review.

Adjunct sweep (beyond items 1-6). While re-anchoring the random-current tree,
the same Aizenman-1982 misattribution class was found outside the enumerated items
and fixed in the same pass: 10 comment lines across 2 files pinning a bare §4,
Eqs. (4.3)–(4.10), Eqs. (4.8)–(4.10) or Eq. (4.12) — none of which exist
(Aizenman's §4 labels only (4.1) and (4.2)). Sites:
IsingModel/Inequalities/SourcefreeConnectionEdgeReachableLeg.lean:50,51,158,391,458
(5 lines; line 50 doubles as an item-1 Lemma 4.1 site) and
IsingModel/Inequalities/SourcefreeConnectionTruncatedFourPointMass.lean:65,80,85,124,273,314
(6 lines, including the Eq. (4.12) site at line 80 in the ## Scope (honest limitation) paragraph). All re-anchored to Lemma 3.2, p. 7, eq. (3.5) (the
switching lemma) or, for the random-walk representation, to Proposition 9.2, p. 24, eqs. (9.5)–(9.7). Reproduce with
git show main:PATH | rg -n --pcre2 '§ ?4(?![.0-9])|Eqs?\. \(4\.[0-9]+\)' on
IsingModel/Inequalities/SourcefreeConnection{EdgeReachableLeg,TruncatedFourPointMass}.lean.

Round-1 review fixes (Med-1/Med-2). One §4 residue survived the first sweep
because the string spans a line break in
SourcefreeConnectionEdgeEmptyLeg.lean:113-115 ((Aizenman 1982\n§4 / FFS Chapter 12; ...) — invisible to a single-line grep). docs/index.md:1780 carried
two Eqs. (4.3)–(4.10) ranges. Both fixed in bf4db83a; residue is now re-checked
with a line-break-insensitive (whitespace-joined) scanner, not single-line grep.

Verification

Check	Result
Line-break-insensitive residue scan (6 classes: `Lemma\s4\.\d`, bare `§\s4`, `Eqs?\.\s\(4\.\d+\)`, `\(4\.(3\|4\|…\|19)\)`, `Thm/Theorem\s9\.35`, `Lemma\s*9\.36`)	`main`: 37/11/8/15/8/4 hits; `HEAD`: 0/0/0/0/0/0
Fail-closed census: all 161 `Aizenman` mentions repo-wide, manually inspected	every pinpointed anchor resolves to §2/§3/§9 with a page number; no `§4`, `Lemma 4.1`, `(4.x)` survives, wrapped or not
AC4 comment-only (hand-written Lean tokenizer stripping `--`, nested `/- -/`, `/-- -/`, `/-! -/`, skipping string literals)	19/19 changed `.lean` files byte-identical `main` vs `HEAD` after stripping; `docs/index.md` is prose only
Anti-scope-creep gates: `9.31` (FV Prop 9.31) 31→31, `§5.1` 221→221, `3.45` 111→110 (only the item-5b site)	PASS, untouched except the one permitted site
Japanese-character audit (`rg "[ぁ-んァ-ン一-龯]" docs/index.md README.md`)	empty
`scripts/citation_audit.py`	PASS — coverage OK, ratchet OK (37 findings cleared, 0 new)
`scripts/audit_gate.py --full` (V1 no `axiom`, V2 no sorry/admit/native_decide, V3 13 capstones axiom-free, V4 no Japanese)	PASS
`lake build` (incremental, 4944 jobs)	green, 0 warnings, 0 errors
`lake env lean IsingModel/Inequalities/SourcefreeConnectionEdgeEmptyLeg.lean` (round-2, Codex)	succeeds, 15s

Independent review — 2 rounds, both APPROVE, Codex agreement both rounds

Round 1 (dev-review + Codex codex exec): found Med-1 (line-break-straddling
§4 residue in SourcefreeConnectionEdgeEmptyLeg.lean) and Med-2
(docs/index.md:1780 double Eqs. (4.3)–(4.10)). Both fixed in bf4db83a; see
"Round-1 review fixes" above.
Round 2 (.self-local/reports/dev-review-5032-pra-round2.md, reviewed SHA
bf4db83a): VERDICT: APPROVE. Independently re-verified every new anchor
against the primary sources (Aizenman 1982, GJ, FFS PDFs read directly — pages
4, 6, 7, 12-13, 22, 57, 60-62, 198-199), re-ran the residue scan and the AC4
comment-only diff, and re-ran the anti-scope-creep gates. One Low finding, on the
PR-body wording only (not a code issue): the adjunct-sweep description in an
earlier draft undercounted the site list; corrected to 10 lines/10 sites above,
with the full enumeration including EdgeReachableLeg.lean:51,458
(Eqs. (4.3)-(4.10)) and TruncatedFourPointMass.lean:80
(Eq. (4.12), Scope paragraph) that an earlier description omitted. Codex
independently re-ran a whitespace-normalized global scan (no residue), confirmed
all 19 changed files comment-only, and confirmed the anti-scope-creep gates —
full agreement, zero divergence, findings: none.

Deferred to PR-B (recorded here, not fixed in this PR)

Med-3 — 8 docs/index.md rows (lines 1772, 1773, 1774, 1775, 1776, 1777,
1780, 1781) pin a stale Aizenman (1982), Lemma 9.2/9.3, §9 reference: this
PR's Lean-header re-anchoring (item 1) moved the underlying modules' anchors to
§2 eq. (2.4) / Proposition 3.1 eq. (3.2) / Lemma 3.2 eq. (3.5) /
Lemma 3.1, so these 8 docs rows now describe those modules with an anchor
their sources no longer use. Pre-existing on main (count unchanged by this
PR — Med-2 only removed an equation range from one of the 8 rows). The
Lemma 9.2/9.3 anchor is correct on the separate ClusterConditioning*
rows, so PR-B must resolve this row-by-row (switching lemma vs. conditioning
lemma), not blanket-replace.
Low-3 — FFS "Ch. 12" / "Chapter 12" used as a descriptor for backbone-tail /
H_low / OZ-wall estimates the chapter does not actually contain (same false-
descriptor class as item 4). 41 total FFS (Ch.|Chapter) ?12 mentions in
IsingModel/; the suspect subset (not yet verified against the FFS PDF, which
needs extraction first) is
SourcefreeConnectionLebowitzConvolutionDegenerateBound.lean:47,143,222,
SourcefreeConnectionLebowitzConvolutionBound.lean:62-63,
SourcefreeConnectionEdgePivotal.lean:13,92,274,
SourcefreeConnectionRatioDerivative.lean:52,58,452. An exact count must be
re-derived in PR-B rather than carried over.
Items 5 (FV "Prop 9.31") and 7f (GJ §5.1 mislabeling for the Simon–Lieb anchor)
remain 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 original PR-B scope, gated on a prior dev-research dispatch
(neither GJ nor FV contains a "Simon–Lieb inequality"; the correct anchor is
primary literature — Simon, CMP 77 (1980) 111–126 / Lieb, CMP 77 (1980)
127–135).

Refs #5032
Refs #4984

… tree (#5032 item 1) Issue #5032 item 1: `Aizenman 1982 Lemma 4.1` does not exist. Re-extracted the primary paper (Commun. Math. Phys. 86, 1-48; `pdftotext -layout`, 49 pages, PDF page = book page) and confirmed first-hand: `Lemma 4.x` matches 0x, and section 4 ("A Heuristic Explanation of the Gaussian Structure ...", pp. 11-13) carries only eqs. (4.1) and (4.2) - so the sibling pointers `§4, Eqs. (4.3)-(4.10)`, `§4, Eqs. (4.8)-(4.10)` and `Eq. (4.12)` are equally nonexistent. Per-site classification (37 sites / 12 files; not a blanket rename), each site matched against what its own declaration claims: * Lemma 3.2, p. 7, eq. (3.5) - the switching lemma (source swap across the two-current doubled ensemble, conditioned on same-cluster connectivity), and the `weightSum * weightSum = tsum of fixed-M inner sums` regrouping that PR #5031 already anchored there. * Lemma 3.1, p. 7 - the fixed-flux binomial source swap: the summand definitions `doubledSourcefreeSummand` / `doubledPairSummand` and the `m |-> M - m` involution. `SourcefreeConnectionUnconditional.lean`'s per-current `W(M) = D(M)` is verbatim Aizenman's `A = B = {x,y}` instance (his eq. (3.8)). * Proposition 3.1, eq. (3.2), p. 6 - sites whose statement *is* `<s_x s_y>^2 = P^{empty,empty}[x <-> y]`, which is that display verbatim. * §9, Lemma 9.2, p. 25, eq. (9.11) and Lemma 9.3, pp. 25-26 - the `ClusterConditioningFiber*` (SL-D2) cluster: Lemma 9.2 is exactly "the correlation in the system obtained by setting the interaction to zero on all the bonds in B(w1)", i.e. the subgraph/reduced-interaction conditioning. Hedged with `cf.` because Aizenman's own use of it is via the Griffiths inequality, an inequality rather than a collapse. * §2, eq. (2.4), p. 4 - `SourcefreeConnectionCurrentDeriv.lean`, whose subject is the random-current weight `w(n) = prod_b (beta J_b)^{n_b}/n_b!` and its beta-scaling, not switching. Same-citation adjuncts, corrected to avoid leaving the files self-contradictory (a `Lemma 3.2, §3` anchor next to a `§4, Eqs. (4.x)` pointer): the nonexistent section-4 pinpoints in `SourcefreeConnectionEdgeReachableLeg.lean` and `SourcefreeConnectionTruncatedFourPointMass.lean`; the latter's P2-ii backbone reference now names Proposition 9.2, p. 24, eqs. (9.5)-(9.7), the random-walk representation. Also in these files (#5032 item 4): FFS `Thm 9.35` / `Lemma 9.36` are displayed equations, ch. 9, pp. 198-199 (verified on the local PDF: running heads `198 9. Models without magnetic field` and `9.2 Examples 199`), not theorems, not in ch. 12, and not the switching lemma - FFS contains no switching/backbone material at all. The labels are corrected and the switching role transferred to Aizenman Lemma 3.2, p. 7, eq. (3.5). Doc comments only; no declaration, statement, proof or import is touched. Refs #5032 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

… 2, 3, 5b, 6) Page numbers re-derived first-hand from `.self-local/refs/Glimm.Jaffe.P428.*.pdf` (book = PDF - 16 in ch. 4), not carried over from the issue. * item 2 - Corollary 4.3.4 is on book p. 62: PDF 78 opens with the running head `62 4 Correlation Inequalities and the Lee-Yang Theorem` and carries `Corollary 4.3.4.` plus its `PROOF.`; book p. 61 (PDF 77) carries `Corollary 4.3.3.`, and book p. 68 is inside §4.5 (Lee-Yang). Fixes `AmbientLattice/TruncatedFunctions/ThreePoint.lean` (`pp. 68ff`) and `Inequalities/Lebowitz/Cor434.lean` (`p. 61`). * item 3 - `Inequalities/GKS.lean`'s reference block named only Theorem 4.1.1, so the Glimm-Jaffe source of `gks_second` was never given. PDF 73 (book 57) has `Theorem 4.1.1` -> `(4.1.9) 0 <= <xi^A>` (GKS-I) and `Theorem 4.1.3` -> `(4.1.11) 0 <= <xi^A xi^B> - <xi^A><xi^B>` (GKS-II) on the same page; the GKS-II line is added and the existing (correct) Friedli-Velenik Thm 3.49 citation is kept. * item 5b - `SourcefreeConnectionLebowitzConvolutionBound.lean` called `lebowitz_four_zero_field` "the corrected form of GHS/FV eq. (3.45)". FV (3.45) is the high-temperature (tanh) representation of the partition function, and the result is the four-point Lebowitz inequality, not GHS. It is re-anchored on Glimm-Jaffe §4.3, Corollaries 4.3.2-4.3.3, pp. 60-61 - the anchor `Inequalities/Lebowitz/LebowitzFour.lean` itself carries (PDF 76 = book 60 heads `Corollary 4.3.2 (Lebowitz Inequalities)`). * item 6 - two live mislabels. `GHS/TruncatedDefs.lean`'s `truncated2_nonneg` claimed "non-negative by GKS-II", which is false on the `i = j` branch: that branch's proof is `gks_first` + `abs_correlation_le_one` + `nlinarith`, and GKS-II gives nothing there. The doc now splits the two branches and names Thm 4.1.3, (4.1.11), p. 57 and Thm 4.1.1, (4.1.9), p. 57 respectively. `Concrete/LatticeGraphCorrelation/FiniteVolumeCorrelationMonotonicity.lean` credited "GJ §4.2 Prop 4.2.1 (GKS-I)" for a nonnegativity statement, but Proposition 4.2.1 is coupling monotonicity; it is re-anchored on GKS-I with that distinction recorded. Doc comments only; no declaration, statement, proof or import is touched. Refs #5032 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…#5032 items 2, 3, 4) Four `docs/index.md` rows carried the same defects fixed on the Lean side: * `:657` - twice: the quoted Glimm-Jaffe display `2^{3/2}<t_i q_j q_k> <= 2^{3/2}<t_i><q_j q_k>` is attributed to "p. 61, verified verbatim" but sits inside the `PROOF.` of Corollary 4.3.4 on PDF 78 = book p. 62; and the trailing "GJ §4.3 Cor 4.3.4, p. 61". Both -> p. 62. * `:1188` - "Cor 4.3.4 pp. 68ff" -> p. 62 (book p. 68 is in §4.5, Lee-Yang). * `:1281` - the row bundled GKS-I and GKS-II under Thm 4.1.1, which states only `(4.1.9) 0 <= <xi^A>`; GKS-II is `(4.1.11)` under Thm 4.1.3, same book page 57. The row now names both. * `:1771` - "Chapter 12 (Theorem 9.35, Lemma 9.36)": `(9.35)` and `(9.36)` are displayed equations in FFS ch. 9 (book pp. 198-199, running heads `198 9. Models without magnetic field` and `9.2 Examples 199`), not theorems and not in ch. 12. The row now says so. `docs/index.md` prose only. The implementation record, with the primary-source extraction table, the per-site classification and the before/after gate measurements, is in `.self-local/reports/dev-implement-5032-pra.md`. Refs #5032 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…uation ranges (#5032) Round-1 review follow-up (two mechanical citation fixes). * `SourcefreeConnectionEdgeEmptyLeg.lean`: the inline proof citation of the Stage A product identity spanned a line break ("Aizenman 1982\n§4"), so the single-line sweep left it behind and the file contradicted its own header. Re-anchored to `Lemma 3.2, p. 7, eq. (3.5)` (the switching lemma), matching the header and the sibling `SourcefreeConnectionEdgeReachableLeg.lean`. * `docs/index.md`: dropped both `Eqs. (4.3)-(4.10)` fragments; Aizenman's §4 contains only eqs. (4.1)/(4.2). The first site keeps `Lemma 3.2, p. 7, eq. (3.5)`; the second keeps the bare `Lemma 9.2/9.3, §9` pointer. Comment/prose only; no proof term changes. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

… bricks Eight progress rows for the random-current / Ornstein-Zernike bricks still pinned "Aizenman (1982), Lemma 9.2/9.3" while the modules they describe were re-anchored elsewhere by PR #5033. The docs now mirror what each module's own reference block says: SourcefreeConnectionCurrentDeriv -> §2, eq. (2.4), p. 4 SourcefreeConnectionRatioDerivative -> Proposition 3.1, eq. (3.2), p. 6 SourcefreeConnectionExcessEdgeSum -> Lemma 3.2, p. 7, eq. (3.5) SourcefreeConnectionEdgePivotal -> Lemma 3.1, p. 7 SourcefreeConnectionEdgeReachableLeg -> Lemma 3.2, p. 7, eq. (3.5) None of the eight belongs to the §9 Lemma 9.2/9.3 bucket: the only modules still carrying that anchor are the ClusterConditioningFiber* files (SL-D2), which no row in this range cites. One row already carried "Aizenman 1982 Lemma 3.2, p. 7, eq. (3.5)" in its body while its trailing reference list still said 9.2/9.3; the two now agree.

…esidue (#5034) Correct the "Simon-Lieb inequality" citation, previously attributed to a nonexistent "FV Prop 9.31" and a mislabeled "GJ §5.1" — neither source contains this result. This is PR-B of #5032 (PR-A merged as #5033, `2270c5e6`), the final authorized scope item of #5032: item 5 (FV "Prop 9.31", 31 sites / 13 files), item 7f (GJ §5.1 mislabeling, 31 Lean lines / 11 files, 15 overlapping item 5), and Med-3 (8 `docs/index.md` rows carrying a stale post-PR-A "Aizenman 1982 Lemma 9.2/9.3" pin). Deliberately excluded: the ~104-site pre-existing `§17.5 pp. 304–306` mis-pin (a different section, separable, left for a future errata PR), the `SummabilityCluster.lean` in-range-object-anchor scoping question, a pre-existing "Six supporting lemmas" wording mismatch in `SimonLieb.lean:11` untouched by this diff, and the `RandomCurrent`-family §5.1 classification (a distinct, separable defect). Why: GJ §5.1 (pp. 72-74) is "Pure and Mixed Phases" — the truncated-correlation cluster property — and never states an edge-peeling/Simon-Lieb result; FV has no "Prop 9.31" at all (FV Ch. 9 tops out at Prop 9.7 and is unrelated). The correct attribution is Simon, B. (1980), Comm. Math. Phys. 77, 111-126, and Lieb, E.H. (1980), Comm. Math. Phys. 77, 127-135 — cited by author/year/journal/pages only, since neither paper's full text is in the repo's local corpus. GJ §17.8 Remark 3, p. 317 corroborates this as the source GJ itself points to. The Lean mathematics (`IsingModel/Inequalities/SimonLieb.lean`, `correlation_inducedGraph_simon_lieb`) was always correct; only the citation was wrong. What was considered and rejected: (1) the Lieb 1980 page range — GJ's own OCR bibliography reads `127-136` (a degraded scan), while the FFS 1992 bibliography (clean text layer) reads `127-135`; the clean source was preferred and corroborated independently in round 3. (2) An FFS eq. (12.27) sentence added in round 1 was rejected and reworded in round 2/3 after two independent reviewers (this repo's reviewer and codex) found it misattributed "special case of Simon-Lieb" to the equation itself rather than to Griffiths' third inequality, which is what FFS actually states. (3) A page-number pin for the FFS anchor was rejected in favor of `eq. (12.27), §12.2`: the repo-local FFS PDF is a 2012 Ghostscript re-typeset whose running header (237) and own index (239) disagree by two pages for the same passage, so no page number is verifiable against the 1992 Springer printing from repo-local evidence; the equation number and section are printing-independent and were read verbatim. Verified over 3 independent review rounds (this repo's reviewer + independent codex cross-review each round, full agreement on every blocking finding): round 1 found 3 High self-contradictions/false-negatives in the initial edit (fixed), round 2 found 1 blocking misattribution in the newly-added FFS sentence (fixed), round 3 APPROVE with all gates green — `lake build` (0 warnings/errors), `scripts/audit_gate.py --full` (V1-V4 pass), and `scripts/citation_audit.py` (37 cleared, 0 new) all re-run independently at HEAD. AC4 comment-only verified over all 16 touched `.lean` files (nested-comment-stripped, byte-identical to `main`, with a fail-open self-test on the stripper). Anti-scope-creep token ledger: `9.31` 31→0, `FV Prop` 12→0, `§5.1 pp. 76–79` 8→0, `Simon 1980`/`Lieb 1980` 0→46/0→46, 17 paths all `M` (no add/delete/rename), no file outside the diff changed. Refs #5032 Refs #4984 Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com> Co-authored-by: Codex <noreply@openai.com>

chore(pr): start PR-A errata mechanical fixes for #5032

ff08f67

phasetr mentioned this pull request Aug 12, 2026

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

Closed

phasetr and others added 4 commits August 12, 2026 09:45

phasetr marked this pull request as ready for review August 12, 2026 01:50

phasetr merged commit 2270c5e into main Aug 12, 2026
10 of 12 checks passed

phasetr deleted the docs/5032-errata-pra-mechanical branch August 12, 2026 01:54

phasetr mentioned this pull request Aug 12, 2026

docs(errata): #5032 PR-B — Simon-Lieb citation correction + related residue #5034

Merged

4 tasks

Navigation Menu

docs(errata): #5032 PR-A — mechanical citation fixes (Aizenman/GJ/FFS pinpoints) - #5033

docs(errata): #5032 PR-A — mechanical citation fixes (Aizenman/GJ/FFS pinpoints)#5033
phasetr merged 5 commits into
mainfrom
docs/5032-errata-pra-mechanical

phasetr commented Aug 12, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

phasetr commented Aug 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Purpose

Scope — 6 items fixed (55 sites / 20 files)

Verification

Independent review — 2 rounds, both APPROVE, Codex agreement both rounds

Deferred to PR-B (recorded here, not fixed in this PR)

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

phasetr commented Aug 12, 2026 •

edited

Loading