feat(gj-5.1): unconditional high-temperature distance cluster decay — closes #4274 (audit B7) - #4275
Merged
Merged
Conversation
… discharge Summable (#4274 B7) Resolves the one tractable hypothesis-gap from the audit #4267 (B7): the distance-cluster-decay wrapper truncated2Infinite_latticeGraph_tendsto_atTop_zero_of_summable was conditional on a Summable hypothesis. This discharges it at high temperature. truncated2Infinite_latticeGraph_summable_of_high_temp: for any exhaustion Λ, ferromagnetic ⟨J,0,β⟩, and βJ·2d < 1, the infinite-volume Ursell 2-point function j ↦ U₂(i,j) is Summable, via truncated2Infinite_summable_of_high_temp (finite susceptibility bound βJ·2d/(1−βJ·2d), FV §3.7.3 / Simon–Lieb GKS-II) with the per-vertex incident-edge count ≤ 2d (edgeFilter_card_eq_degree + inducedLatticeGraph_degree_le). truncated2Infinite_latticeGraph_tendsto_atTop_zero_of_high_temp and its cofinite companion: the unconditional distance-→∞ (and cofinite) decay U₂(i,j) → 0. Added to CorrelationDecay.lean (importing the Simon–Lieb/susceptibility layer SummabilityCluster, NOT the analyticity/cluster-expansion chain) so the new theorems share the file's local Fintype instance with the gated wrappers. Axiom-free (#print axioms = [propext, Classical.choice, Quot.sound]; no Vitali). docs/index.md + tex/proof-guide.tex synced. Closes #4274. Part of #4267 / #4214 (§5.1). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ms live in CorrelationDecay.lean) The B7 high-temperature cluster-decay theorems are defined in CorrelationDecay.lean (sharing the file's local Fintype instance with the gated wrappers, avoiding the instance-mismatch isDefEq blowup). The separate CorrelationDecayHighTemp.lean was a redundant earlier draft and is removed. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This was referenced Jun 24, 2026
Closed
Closed
phasetr
added a commit
that referenced
this pull request
Jun 24, 2026
…oses #4268 (audit B1) Discharges the §17.5 PseudoMassLatticeDistanceBridge adjacent hypothesis h_adj_exp unconditionally in the strict high-temperature window 0 < βJ·2d < 1/2, using the finite high-temperature susceptibility bound merged in B7 #4275. SummabilityCluster.lean: - correlationInfinite_le_susceptibility_bound_of_high_temp: at h=0, GKS-II nonnegativity makes a single pair term ≤ the whole susceptibility sum, so correlationInfinite {i,w} ≤ βJD/(1−βJD) (singleton private helper + susceptibilityAlongExhaustion_le_of_high_temp + le_of_tendsto). - correlationInfinite_latticeGraph_le_susceptibility_bound_of_high_temp: D=2d specialization. This is the missing distance-1 bound (Simon–Lieb peeling only gives ≤ 1 at distance 1). HLSBridgeUnconditional.lean: - correlationInfinite_latticeGraph_pair_le_exp_neg_of_high_temp: for B := βJ2d/(1−βJ2d) ∈ (0,1) (i.e. βJ2d < 1/2), corr {0,w} ≤ exp(−M) for any M ≤ −log B. - pseudoMassLatticeDistanceBridge_of_high_temp: choosing M := min(min 1 (−log B)) (simonLiebRate/(2(α+1))) satisfies 0<M, M≤1, (α+1)M ≤ simonLiebRate/2 and h_adj_exp simultaneously, giving an unconditional PseudoMassLatticeDistanceBridge via the trichotomy constructor. - tsum_correlationInfinite_pair_product_le_const_of_high_temp (+ diagonal): unconditional §17.5 HLS pair-product sum bound, no adjacent-decay hypothesis. Axiom-free (#print axioms = [propext, Classical.choice, Quot.sound]; no Vitali). lake build + GKSTest pass; linter-clean; docs/index.md + tex/proof-guide.tex synced. Closes #4268. Part of #4267 / #4214 (§17.5). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
phasetr
added a commit
that referenced
this pull request
Jun 24, 2026
…oses #4268 (audit B1) (#4277) * chore(gj-17.5): scaffold unconditional adjacent-pair susceptibility bridge — #4268 * feat(gj-17.5): unconditional adjacent-pair susceptibility bridge — closes #4268 (audit B1) Discharges the §17.5 PseudoMassLatticeDistanceBridge adjacent hypothesis h_adj_exp unconditionally in the strict high-temperature window 0 < βJ·2d < 1/2, using the finite high-temperature susceptibility bound merged in B7 #4275. SummabilityCluster.lean: - correlationInfinite_le_susceptibility_bound_of_high_temp: at h=0, GKS-II nonnegativity makes a single pair term ≤ the whole susceptibility sum, so correlationInfinite {i,w} ≤ βJD/(1−βJD) (singleton private helper + susceptibilityAlongExhaustion_le_of_high_temp + le_of_tendsto). - correlationInfinite_latticeGraph_le_susceptibility_bound_of_high_temp: D=2d specialization. This is the missing distance-1 bound (Simon–Lieb peeling only gives ≤ 1 at distance 1). HLSBridgeUnconditional.lean: - correlationInfinite_latticeGraph_pair_le_exp_neg_of_high_temp: for B := βJ2d/(1−βJ2d) ∈ (0,1) (i.e. βJ2d < 1/2), corr {0,w} ≤ exp(−M) for any M ≤ −log B. - pseudoMassLatticeDistanceBridge_of_high_temp: choosing M := min(min 1 (−log B)) (simonLiebRate/(2(α+1))) satisfies 0<M, M≤1, (α+1)M ≤ simonLiebRate/2 and h_adj_exp simultaneously, giving an unconditional PseudoMassLatticeDistanceBridge via the trichotomy constructor. - tsum_correlationInfinite_pair_product_le_const_of_high_temp (+ diagonal): unconditional §17.5 HLS pair-product sum bound, no adjacent-decay hypothesis. Axiom-free (#print axioms = [propext, Classical.choice, Quot.sound]; no Vitali). lake build + GKSTest pass; linter-clean; docs/index.md + tex/proof-guide.tex synced. Closes #4268. Part of #4267 / #4214 (§17.5). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * docs(gj-17.5): state βJ2d<1/2 sub-window scope of the adjacent bridge (cross-check #4277) Per the squash-merge cross-check: the unconditional discharge of h_adj_exp holds on the strict sub-window 0<βJ·2d<1/2 (susceptibility ceiling B<1); the wider band 1/2≤βJ·2d<1 is intrinsically out of reach (B≥1) and still rests on an assumed adjacent input. Stated explicitly in docs/index.md and tex/proof-guide.tex. Part of #4267 / #4214 (§17.5). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 (1M context) <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.
Closes #4274. Part of the hypothesis-gap audit #4267 (the one tractable item, B7) and #4214 (§5.1).
Summary
Discharges the
Summablehypothesis of the conditional distance-cluster-decay wrappertruncated2Infinite_latticeGraph_tendsto_atTop_zero_of_summableat high temperature, giving the unconditional ℤ^d cluster-decay statement.truncated2Infinite_latticeGraph_summable_of_high_temp— for any exhaustionΛ, ferromagnetic⟨J,0,β⟩(0≤J,0<β), and the Simon–Lieb conditionβ·J·2d < 1, the infinite-volume Ursell two-point functionj ↦ U₂(i,j)isSummable, viatruncated2Infinite_summable_of_high_temp(finite susceptibility boundβJ·2d/(1−βJ·2d), FV §3.7.3 / Simon–Lieb GKS-II) with the per-vertex incident-edge count≤ 2d(edgeFilter_card_eq_degree+inducedLatticeGraph_degree_le, exactly as inclusterProperty_latticeGraph_of_high_temp).truncated2Infinite_latticeGraph_tendsto_atTop_zero_of_high_temp+…_tendsto_cofinite_zero_of_high_temp— the unconditional distance-→∞(andcofinite) decayU₂(i,j) → 0.The theorems are added to
CorrelationDecay.lean(importing the Simon–Lieb / susceptibility layerSummabilityCluster, not the analyticity/cluster-expansion chain) so they share the file'slocalFintype instance with the gated wrappers — avoiding an instance-mismatchisDefEqblowup that a separate file produced.Verification
lake build✅ (5624 jobs), linter-warning-free.lake exe GKSTest✅ all tests passed.#print axioms truncated2Infinite_latticeGraph_tendsto_atTop_zero_of_high_temp=[propext, Classical.choice, Quot.sound](no Vitali — the chain is the GKS/Simon–Lieb finite-volume layer only).docs/index.md+tex/proof-guide.texsynced (TeX compiles, no Japanese contamination).claude -p); strictclaude -preview pre-merge.References: Glimm–Jaffe, 2nd ed., §5.1, pp. 72–79; Friedli–Velenik §3.7.3 (Simon–Lieb / susceptibility).
🤖 Generated with Claude Code