Found while doing the page-scoped citation verification for the #4984 header
campaign (wave 4, LGC Finite*). Both items are outside that wave's frozen
17-file scope, so they are filed here rather than absorbed, following the
#4987 / #4989 / #4991 precedent.
Verification method for everything below: page-scoped extraction
(pdftotext -f N -l N on .self-local/refs/Glimm.Jaffe.P428.*.pdf), never the
flat OCR text. The page offset is not constant across the book: in the
chapter-4 region book page = PDF page − 16 (PDF 71 = book 55 = the chapter
opening, PDF 73 = 57, 74 = 58, 75 = 59, 76 = 60, 77 = 61, 78 = 62, 79 = 63,
80 = 64), whereas #4991's chapter-17 work measured book page = PDF page − 11
(PDF 322 = book 311). Anyone re-checking these must re-measure the offset in the
region they are reading.
A. "Glimm–Jaffe Proposition 4.2.4" does not exist
Glimm–Jaffe §4.2 (book pp. 58–59, PDF 74–75) contains exactly Proposition
4.2.1 (correlations monotone in the couplings, p. 58), Proposition 4.2.2
(Ising couplings are ferromagnetic and correlations are at most 1, p. 58) and
Theorem 4.2.3 (correlations converge as the volume grows, p. 59); §4.3
begins immediately after Theorem 4.2.3 on p. 59. Chapter 4 ends on book p. 71
(PDF 87) with no exercise or problem section. The string 4.2.4 occurs zero
times in .self-local/refs/Glimm.Jaffe.Quantum_Physics.txt, whose §4.2 hits are
7× 4.2.1, 9× 4.2.2, 3× 4.2.3.
The repository nevertheless attributes h-direction (and, in places, β-direction)
correlation monotonicity to "GJ Prop 4.2.4" at 36 lines across 9 files:
IsingModel/InfiniteVolume/MonotoneH.lean (module header, section header and
the theorem docstring, which additionally calls it "p. 58, exercise")IsingModel/InfiniteVolume/MonotoneBeta.leanIsingModel/AmbientLattice/MagnetizationAlongExhaustion.leanIsingModel/Concrete/LatticeGraphCorrelation/SiteIndepMagTwoPointMonotone.leanIsingModel/Concrete/LatticeGraphCorrelation/TwoPointCorrelationInfiniteMonotoneCubicEx.leanIsingModel/Concrete/LatticeGraphCorrelation/LatticeMassHighTemperature/PosAndAntitone.leanIsingModel/FieldDerivative/CorrelationMonotonicity.leandocs/index.mdtex/proof-guide.tex
Two of those 36 lines attribute the same number to Friedli–Velenik instead
(FieldDerivative/CorrelationMonotonicity.lean:58 and docs/index.md:1979,
both "FV §4.2 Prop. 4.2.4 (p. 58)"). That is not a rescue: Friedli–Velenik
number their results flat within a chapter ("Proposition 4.21", "Exercise 4.2"),
so 4.2.4 is not an FV label either, and the string does not occur in
.self-local/refs/Friedli.Velenik.txt.
The mathematics is fine — h-monotonicity really does follow from GJ's own
Proposition 4.2.1, because raising h raises the singleton couplings J_{i},
which is exactly the remark GJ makes on p. 58 after Proposition 4.2.2 ("with a
positive external field, 0 ≤ h, the Ising model measure (4.2.2) is still
ferromagnetic"). Only the label is invented.
Suggested disposition: replace "Prop 4.2.4" by "Proposition 4.2.1, p. 58,
applied to the singleton couplings" (or by the p. 58 remark) rather than by a
blanket search-and-replace, since the β-direction sites are a repository
extension that GJ does not state at all.
B. Corollary 4.3.5 is on book p. 63, and the repository says both 62 and 63
Corollary 4.3.5 (the (n-1)!!-type pairing bound) is stated and proved on book
p. 63 (PDF 79); book p. 62 (PDF 78) holds Corollary 4.3.4 and the Remark
about the Ursell functions. The repository is internally inconsistent about
this:
For contrast, Inequalities/GHS/Truncated4.lean:137's "Cor. 4.3.3
(Glimm–Jaffe, §4.3, p. 61)" is correct, and the U_4 ≤ 0 reading of
Corollary 4.3.3 is indeed the remark on p. 62 — which is a plausible mechanical
origin for the p. 62 drift on 4.3.5.
Suggested disposition: rewrite the 4.3.5 page citations to p. 63 and keep the
4.3.3 ones at p. 61.
Scope note
Wave 4 of #4984 uses the verified values in the headers it rewrites
(§4.3, Corollary 4.3.5, p. 63, Corollary 4.3.4, p. 62, Corollary 4.3.3, p. 61, §4.2 Proposition 4.2.1, p. 58, Theorem 4.2.3, p. 59) and carries no
4.2.4 reference. The 36 + 10 sites above are all outside its frozen file set.
Refs #4984
Found while doing the page-scoped citation verification for the #4984 header
campaign (wave 4, LGC
Finite*). Both items are outside that wave's frozen17-file scope, so they are filed here rather than absorbed, following the
#4987 / #4989 / #4991 precedent.
Verification method for everything below: page-scoped extraction
(
pdftotext -f N -l Non.self-local/refs/Glimm.Jaffe.P428.*.pdf), never theflat OCR text. The page offset is not constant across the book: in the
chapter-4 region book page = PDF page − 16 (PDF 71 = book 55 = the chapter
opening, PDF 73 = 57, 74 = 58, 75 = 59, 76 = 60, 77 = 61, 78 = 62, 79 = 63,
80 = 64), whereas #4991's chapter-17 work measured book page = PDF page − 11
(PDF 322 = book 311). Anyone re-checking these must re-measure the offset in the
region they are reading.
A. "Glimm–Jaffe Proposition 4.2.4" does not exist
Glimm–Jaffe §4.2 (book pp. 58–59, PDF 74–75) contains exactly Proposition
4.2.1 (correlations monotone in the couplings, p. 58), Proposition 4.2.2
(Ising couplings are ferromagnetic and correlations are at most 1, p. 58) and
Theorem 4.2.3 (correlations converge as the volume grows, p. 59); §4.3
begins immediately after Theorem 4.2.3 on p. 59. Chapter 4 ends on book p. 71
(PDF 87) with no exercise or problem section. The string
4.2.4occurs zerotimes in
.self-local/refs/Glimm.Jaffe.Quantum_Physics.txt, whose §4.2 hits are7×
4.2.1, 9×4.2.2, 3×4.2.3.The repository nevertheless attributes h-direction (and, in places, β-direction)
correlation monotonicity to "GJ Prop 4.2.4" at 36 lines across 9 files:
IsingModel/InfiniteVolume/MonotoneH.lean(module header, section header andthe theorem docstring, which additionally calls it "p. 58, exercise")
IsingModel/InfiniteVolume/MonotoneBeta.leanIsingModel/AmbientLattice/MagnetizationAlongExhaustion.leanIsingModel/Concrete/LatticeGraphCorrelation/SiteIndepMagTwoPointMonotone.leanIsingModel/Concrete/LatticeGraphCorrelation/TwoPointCorrelationInfiniteMonotoneCubicEx.leanIsingModel/Concrete/LatticeGraphCorrelation/LatticeMassHighTemperature/PosAndAntitone.leanIsingModel/FieldDerivative/CorrelationMonotonicity.leandocs/index.mdtex/proof-guide.texTwo of those 36 lines attribute the same number to Friedli–Velenik instead
(
FieldDerivative/CorrelationMonotonicity.lean:58anddocs/index.md:1979,both "FV §4.2 Prop. 4.2.4 (p. 58)"). That is not a rescue: Friedli–Velenik
number their results flat within a chapter ("Proposition 4.21", "Exercise 4.2"),
so
4.2.4is not an FV label either, and the string does not occur in.self-local/refs/Friedli.Velenik.txt.The mathematics is fine — h-monotonicity really does follow from GJ's own
Proposition 4.2.1, because raising
hraises the singleton couplingsJ_{i},which is exactly the remark GJ makes on p. 58 after Proposition 4.2.2 ("with a
positive external field, 0 ≤ h, the Ising model measure (4.2.2) is still
ferromagnetic"). Only the label is invented.
Suggested disposition: replace "Prop 4.2.4" by "Proposition 4.2.1, p. 58,
applied to the singleton couplings" (or by the p. 58 remark) rather than by a
blanket search-and-replace, since the β-direction sites are a repository
extension that GJ does not state at all.
B. Corollary 4.3.5 is on book p. 63, and the repository says both 62 and 63
Corollary 4.3.5 (the
(n-1)!!-type pairing bound) is stated and proved on bookp. 63 (PDF 79); book p. 62 (PDF 78) holds Corollary 4.3.4 and the Remark
about the Ursell functions. The repository is internally inconsistent about
this:
Concrete/LatticeGraphCorrelation/UniformMagCorrelationTrivialCor4_3_5.lean(3 sites, from 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 2).
Inequalities/GHS/NPoint.lean(2 sites),Inequalities/Lebowitz/Cor435.lean(3 sites),AmbientLattice/SpontaneousMono.lean,docs/index.md(at leastlines 653, 1082, 1255).
Inequalities/GHS/Truncated3Contraction.lean:25.For contrast,
Inequalities/GHS/Truncated4.lean:137's "Cor. 4.3.3(Glimm–Jaffe, §4.3, p. 61)" is correct, and the
U_4 ≤ 0reading ofCorollary 4.3.3 is indeed the remark on p. 62 — which is a plausible mechanical
origin for the p. 62 drift on 4.3.5.
Suggested disposition: rewrite the 4.3.5 page citations to p. 63 and keep the
4.3.3 ones at p. 61.
Scope note
Wave 4 of #4984 uses the verified values in the headers it rewrites
(
§4.3, Corollary 4.3.5, p. 63,Corollary 4.3.4, p. 62,Corollary 4.3.3, p. 61,§4.2 Proposition 4.2.1, p. 58,Theorem 4.2.3, p. 59) and carries no4.2.4reference. The 36 + 10 sites above are all outside its frozen file set.Refs #4984