docs(errata): #5032 PR-B — Simon-Lieb citation correction + related residue - #5034
Merged
Conversation
…on 1980 / Lieb 1980 The library's edge-peeling correlation bound (`correlation_inducedGraph_simon_lieb` and its infinite-volume, high-temperature and pseudo-mass consumers) was cited to "Friedli-Velenik Prop 9.31" and to "Glimm-Jaffe §5.1 pp. 74-75 / pp. 76-79". Neither anchor exists: Friedli-Velenik has no Proposition 9.31 (its Chapter 9 is "Models with Continuous Symmetry" and its highest numbered proposition there is 9.7), and Glimm-Jaffe §5.1 "Pure and Mixed Phases" spans pp. 72-74 and states the cluster property, not an edge-peeling bound; pp. 74-79 are §5.2/§5.3. The mathematics is unchanged and correct: it is the classical Simon-Lieb inequality in its random-current form, due to * B. Simon, Correlation inequalities and the decay of correlations in ferromagnets, Comm. Math. Phys. 77 (1980), 111-126; * E. H. Lieb, A refinement of Simon's correlation inequality, Comm. Math. Phys. 77 (1980), 127-135, which Glimm-Jaffe itself cites in §17.8 Remark 3, p. 317. Since neither paper's text is available among this repository's local references, they are cited by author/year/journal/volume/page-range only, with no internal theorem or page pinpoint claimed. Scope discipline: only the sites that use §5.1 to source the Simon-Lieb bound are re-anchored. Citations of §5.1's real content -- the cluster property at pp. 72-74/73-74, the order parameter and symmetry breaking, high-temperature susceptibility with Friedli-Velenik §3.7.3 -- are left untouched, and their counts are unchanged by this commit. Comment- and documentation-only; no declaration, statement or proof is touched.
… 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.
…ceiling Round-1 review follow-up for the Simon-Lieb citation errata. GJ §5.1 "Pure and Mixed Phases" spans pp. 72-74 (§5.2 starts p. 74) and contains eq. (5.1.3)-(5.1.5), the truncated pair correlation and cluster property -- no susceptibility bound and no edge-peeling inequality. * Cluster.lean, CorrelationDecay.lean, TheoremEtaLe1/MainTheorem.lean: §5.1 pp. 76-79 -> pp. 72-74 on genuine cluster-property content; this removes the last self-contradiction against the range these blocks now assert. The `pp. 76-79` / `pp. 72-79` class is now empty repo-wide. * Inequalities/HighTemp/Susceptibility.lean: every declaration states the `betaJD/(1-betaJD)` ceiling produced by iterating the Simon-Lieb peeling inequality (`correlation_sum_le_of_high_temp`), so all eight Reference lines now carry Simon 1980 / Lieb 1980 instead of a GJ §5.1 page pin. The module header keeps §5.1 pp. 72-74 scoped to the truncated two-point function that the susceptibility sums. * Inequalities/SimonLieb.lean: record the one repo-local statement of the bound, FFS eq. (12.27), Chapter 12. No page pin -- the local copy is a re-typeset whose index and running headers disagree (239 vs 237). * docs/index.md: mirror the Lean anchors for the rows whose modules lost their §5.1 anchor (1784, 1794, 1798, 1799, 2049, 2050), applying the Section-column rule already used for row 2099. Comment-only: all 16 touched .lean files are byte-identical after stripping comments. lake build 4944 jobs, zero warnings. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…third inequality
Round-2 review follow-up. The FFS sentence added by the previous commit read
... eq. (12.27) ..., Chapter 12, where it is derived from Griffiths' third
inequality and identified there as a special case of Simon-Lieb.
The coordinated passive makes eq. (12.27) the subject of both clauses, so it
asserts that FFS identifies (12.27) itself as a special case of Simon-Lieb.
FFS says something else (repo-local PDF, printed p. 237):
Indeed, by Griffiths' third inequality [271] (which is a special case of the
Simon-Lieb inequality [464, 372]) we have <s_z s_x> <= sum_z' (tanh J_zz')
<s_z' s_x> (12.27)
The parenthetical attaches to Griffiths' third inequality, not to (12.27). The
clause is reworded so the attribution follows the source.
The anchor is also tightened from "Chapter 12" to "§12.2": the passage sits on a
page whose running header reads "12.2 Lebowitz and Aizenman-Fröhlich
inequalities", and in body order it falls between the §12.2.2 and §12.2.3
headings. Unlike a page number, the section survives the index/running-header
disagreement of the local re-typeset.
Comment-only: all 16 .lean files touched by this branch remain byte-identical to
main after stripping comments. lake build 4944 jobs, zero warnings; audit_gate
--full and citation_audit both PASS.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Purpose
Correct the "Simon-Lieb inequality" citation, previously attributed in this repo 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, items 1/2/3/4/5b/6, merged as #5033
2270c5e6); PR-B closes outitems 5 and 7f plus a round-2 carry-over (Med-3), and is the final authorized scope item of
#5032.
Background (research conclusion)
9.31— 0 hits in theextracted FV text).
not any edge-peeling/Simon-Lieb result. GJ never states or numbers a "Simon-Lieb inequality"
anywhere in its own text.
correlations in ferromagnets," Comm. Math. Phys. 77, 111-126, and Lieb, E.H. (1980), "A
refinement of Simon's correlation inequality," Comm. Math. Phys. 77, 127-135 — cited by
author/year/journal/volume/pages only (neither paper's full text is in the repo's local
corpus, so no page/theorem pinpoint into them is claimed).
points readers to.
IsingModel/Inequalities/SimonLieb.lean,correlation_inducedGraph_simon_lieb, an edge-peeling correlation bound via therandom-current representation) was always mathematically correct; only the citation was wrong.
Item disposition
docs/index.mdrows + 24 Lean lines)9.31token count 31 → 0 tree-wide§5.1 pp. 76–798 → 0,§5.1 pp. 72–791 → 0 tree-wide; correct in-range§5.1 pp. 72–74retained/extended (25 → 30, all GJ-TOC-verified)docs/index.mdrows 1772/1773/1774/1775/1776/1777/1780/1781 pinning a staleAizenman (1982), Lemma 9.2/9.3, §9)§2 eq.(2.4)/Proposition 3.1 eq.(3.2)/Lemma 3.2 eq.(3.5)/Lemma 3.1), verified row-by-row 8/8 exact matchPlus one added anchor:
IsingModel/Inequalities/SimonLieb.leannow citesFernández–Fröhlich–Sokal (1992), eq. (12.27), §12.2as the one Simon-Lieb pinpoint that isindependently verifiable in the repo's local corpus (FFS states eq. (12.27) as a tanh-weighted
special case derived from Griffiths' third inequality, itself a special case of the Simon-Lieb
inequality — the repo's comment attributes this reading to FFS, not to the repo's own voice).
FFS anchor — pagination judgment call
The repo-local FFS PDF is a 2012 Ghostscript re-typeset (
Creator: dvips(k) 5.96,CreationDate: 2012-02-09) whose running header and its own index disagree by 2 pages for thesame passage (running header reads printed p. 237; the book's own index says "Simon-Lieb
inequality, 239"; printed p. 239 in this artifact carries no Simon-Lieb text). Neither number is
verifiable as a claim about the 1992 Springer printing from repo-local evidence alone. The PR
therefore cites by eq. (12.27), §12.2 instead of a page number — both identifiers were read
verbatim from the PDF and are printing-independent, whereas asserting either candidate page
number would have manufactured a new instance of the exact citation-accuracy defect this PR
exists to remove.
§12.2(rather than the more granular§12.2.2) was chosen because it is thesection identified by the page's own running header, the coarsest-but-still-true granularity
confirmable on the page carrying the equation.
Review history (3 rounds,
dev-review+ independent codex cross-review each round)3e9e0111) — CHANGES REQUESTED (3 High, 3 Med), full agreement with codex on all3 High findings: two edited doc blocks left a self-contradictory
§5.1 pp. 76–79pin(
Cluster.lean:34,CorrelationDecay.lean:84-87), and one classification false negative(
Susceptibility.lean:38-46names "Simon-Lieb iteration" in its doc header but had not beenre-anchored). Also flagged: the Lieb 1980 page range
127-135vs GJ's OCR127-136isdecidable in favor of
127-135via the FFS bibliography (clean, non-OCR text layer) — noescalation needed, kept as implemented.
81fbe297) — CHANGES REQUESTED (1 Med, blocking), full agreement with codex: theround-1 fixes were all verified correct and the
§5.1 pp. 76–79/pp. 72–79class wasconfirmed empty repo-wide, but the newly-added FFS sentence (R2-1) misattributed "special case
of Simon-Lieb" to eq. (12.27) itself rather than to Griffiths' third inequality (which is what
FFS actually says) — found independently by both reviewers reading the same ambiguous
coordinated-passive construction.
d01846c6, current HEAD) — APPROVE, full agreement with codex on everyquestion this round (R2-1 fix correct,
§12.2anchor correct, change is comment-only). Theone-clause reword was verified against the FFS primary source first-hand and is now
unambiguous. Codex's sole finding this round is a Low, non-blocking item on a line the PR does
not touch (
SimonLieb.lean:11, pre-existing onmain) — out of 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 authorized scope,recorded as a follow-up.
Gate evidence (independently re-run each round, not self-reported)
AC4 (comment-only change): both rounds, all 16 touched
.leanfiles byte-identical afternested-comment stripping (per-file
mainvsHEADcontent, SHA-256 compared); round 3additionally ran a fail-open self-test on the stripper (mutation of code, indentation, blank
lines all correctly detected as DIFF) to confirm the SAME×16 result is a real negative.
scripts/citation_audit.py: PASS every round — coverage OK, ratchet OK (37 cleared, 0new), 694 gating findings unchanged, 112 pre-existing advisory self-refs.
scripts/audit_gate.py --full: PASS every round — V1 (1922 files, noaxiom), V2 (nosorry/admit/native_decide), V3 (13 capstones ⊆ {propext, Classical.choice, Quot.sound}), V4 (no
Japanese, 1977 files).
lake build: exit 0, 4944 jobs, "Build completed successfully", zerowarning:/error:lines each round (doc-comment-only diff; no proof-term edits).
Anti-scope-creep token ledger (round 3, whole-tree,
.lean+.md, 1931 files both sides,main→ HEAD):9.31FV Prop§5.1 pp. 76–79§5.1 pp. 72–79§5.1(total)Simon 1980Lieb 198012.27/§12.2/Griffithsgit diff --name-status main...HEAD: 17 paths, allM(no add/delete/rename); all within theitem-5/item-7f/Med-3 site lists plus the two review-driven fixes. No file outside the diff
changed token counts.
Non-blocking follow-ups (recorded, not actioned in this PR — out of #5032's authorized scope)
§17.5 pp. 304–306mis-pin, ~104 sites tree-wide (docs/index.md~28 rows +HLSLatticeMassBridge.lean:19,PathLowerBound.lean:96,UpperBound.lean:108,JLowerBound.lean:200,SourcefreeConnectionLebowitzConvolutionDegenerateBound.lean:55, …) — GJ TOC says §17.5starts p. 310, not p. 304 (p. 304 is §17.1).
SummabilityCluster.lean:84,181still creditGJ §5.1 alone for the
βJD/(1−βJD)ceiling thatSusceptibility.leannow attributes toSimon/Lieb — nothing false asserted, but the scoping rule this PR applied elsewhere was not
extended here).
SimonLieb.lean:11"Six supporting lemmas" list-count mismatch (item 6 of the list isthe main result, not a supporting lemma) — pre-existing on
main, not introduced by this PR.RandomCurrent-family §5.1 classification (RandomCurrent.lean,RandomCurrent/Core.lean,Switching/Core.leanstill classify random-current preparation under GJ §5.1, which containsno random-current representation) — deferred sibling cluster, round-1's classification.
Test plan
rg -n "9\.31" IsingModel/ docs/index.md— 0 hits.rg -n "Simon-Lieb|Simon–Lieb" IsingModel/ docs/index.md— cites Simon 1980 / Lieb 1980 byname/year/journal/pages only, no page-pinpoint claims into those papers.
lake buildclean (doc-comment-only changes; no proof-term edits).rg -n "[ぁ-んァ-ン一-龯]" docs/index.md README.md— empty.Refs #5032
Refs #4984