Build tight (diagonal-free) per-stage increment chain — #2965#2996
Merged
Conversation
The weak derivBound carries a diagonal term ⟨σ_rσ_s⟩⟨σ_kσ_l⟩ whose shell
sum is ⟨σ_rσ_s⟩·O(|∂box_k|), which diverges with shell size and cannot
prove convergence of c_k. Re-derive the entire per-stage increment chain
with the tight ball-boundary Simon-Lieb bound derivBoundTight (cross
products only, via cor_4_3_3_scaled):
- Tight.lean: scaledCorrelation_one_sub_zero_le_derivBoundTight,
correlation_sub_deleteEdges_le_derivBoundTight,
derivBoundTight_le_of_correlation_le.
- PerStageIncrement.lean: correlation_pair_sub_inducedGraph_le_derivBoundTight,
correlation_pair_two_box_le_derivBoundTight.
- CubicPerStageIncrement.lean:
correlationAlongExhaustion_cubic_succ_sub_le_derivBoundTight.
- CubicShellInfiniteVolumeBound.lean:
derivBoundTight_inducedGraph_cubic_le_infiniteVolume_sum.
Net diagonal-free bound:
c_{k+1} − c_k ≤ β·J·∑_{⟨a,b⟩∈shell}[g{r,a}g{s,b} + g{r,b}g{s,a}]
(g = infinite-volume correlation), the summable form on which Phase B
spatial decay yields a geometric rate.
Each tight lemma mirrors its weak counterpart (#2972/#2974/#2989/#2992/
#2993/#2994/#2995); the component-factorization and observable-matching
infrastructure is bound-independent and reused unchanged.
Docs and proof-guide synced.
Part of #2965
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
5 tasks
phasetr
added a commit
that referenced
this pull request
May 27, 2026
Add `derivBoundTight_inducedGraph_cubic_le_decay_sum` (Issue #2965, Phase B): in the high-temperature regime contractionFactor d (cubicExhaustion d) p r₀ < 1, for r,s ∈ box_n on no E₀-edge, derivBoundTight … E₀ … ⟨r,_⟩ ⟨s,_⟩ ≤ β·J·∑_{⟨a,b⟩∈E₀}[cf^{d(r,a)/(r₀+2)}·cf^{d(s,b)/(r₀+2)} + cf^{d(r,b)/(r₀+2)}·cf^{d(s,a)/(r₀+2)}] where cf = contractionFactor and d is the ℓ¹ lattice distance. Applies the per-pair spatial decay correlationInfinite_latticeGraph_le_contractionFactor_pow_dist_pair termwise to the diagonal-free infinite-volume bound derivBoundTight_inducedGraph_cubic_le_infiniteVolume_sum (#2996). Distinctness r ≠ a.val etc. follows from r,s being on no E₀-edge (Sym2.mem_iff). The cross-product-only (tight) structure guarantees every factor genuinely decays — the diagonal-free decay-sum input from which a geometric per-stage rate is extracted (shell-edge distance/counting aggregation downstream). Docs and proof-guide synced. Part of #2965 Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
phasetr
added a commit
that referenced
this pull request
May 27, 2026
* feat: cubic shell decay-sum bound (Part of #2965) * Bound cubic-shell derivBoundTight by a spatial-decay sum Add `derivBoundTight_inducedGraph_cubic_le_decay_sum` (Issue #2965, Phase B): in the high-temperature regime contractionFactor d (cubicExhaustion d) p r₀ < 1, for r,s ∈ box_n on no E₀-edge, derivBoundTight … E₀ … ⟨r,_⟩ ⟨s,_⟩ ≤ β·J·∑_{⟨a,b⟩∈E₀}[cf^{d(r,a)/(r₀+2)}·cf^{d(s,b)/(r₀+2)} + cf^{d(r,b)/(r₀+2)}·cf^{d(s,a)/(r₀+2)}] where cf = contractionFactor and d is the ℓ¹ lattice distance. Applies the per-pair spatial decay correlationInfinite_latticeGraph_le_contractionFactor_pow_dist_pair termwise to the diagonal-free infinite-volume bound derivBoundTight_inducedGraph_cubic_le_infiniteVolume_sum (#2996). Distinctness r ≠ a.val etc. follows from r,s being on no E₀-edge (Sym2.mem_iff). The cross-product-only (tight) structure guarantees every factor genuinely decays — the diagonal-free decay-sum input from which a geometric per-stage rate is extracted (shell-edge distance/counting aggregation downstream). Docs and proof-guide synced. Part of #2965 Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * State d≥1/ferromagnetic/h=0 hypotheses in docs+tex (codex cross-check) Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 <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.
Part of #2965
Motivation
The weak
derivBoundcarries a diagonal term⟨σ_rσ_s⟩⟨σ_kσ_l⟩whose shell sum is⟨σ_rσ_s⟩·O(|∂box_k|), which diverges with the shell size and so cannot prove convergence ofc_k. This PR re-derives the entire per-stage increment chain with the tight ball-boundary Simon–Lieb boundderivBoundTight(cross products⟨σ_rσ_k⟩⟨σ_sσ_l⟩ + ⟨σ_rσ_l⟩⟨σ_sσ_k⟩only, no diagonal), via the existingball_boundary_simon_lieb_tight/cor_4_3_3_scaled.Tight chain (each mirrors its weak counterpart)
Tight.lean:scaledCorrelation_one_sub_zero_le_derivBoundTight,correlation_sub_deleteEdges_le_derivBoundTight,derivBoundTight_le_of_correlation_le.PerStageIncrement.lean:correlation_pair_sub_inducedGraph_le_derivBoundTight,correlation_pair_two_box_le_derivBoundTight.CubicPerStageIncrement.lean:correlationAlongExhaustion_cubic_succ_sub_le_derivBoundTight.CubicShellInfiniteVolumeBound.lean:derivBoundTight_inducedGraph_cubic_le_infiniteVolume_sum.The component-factorization and observable-matching infrastructure (
correlation_deleteEdges_filter_pair_eq,nestedFinsetEquiv,correlation_inducedGraph_nested_finset,liftFinset_pair, the finite ≤ infinite bridge) is bound-independent and reused unchanged.Net result
(g = infinite-volume correlation) — the diagonal-free, summable form on which the Phase B spatial decay (#2966) yields a geometric rate.
Verification
lake buildof all four files — green, zero linter warnings.lake exe GKSTest— all pass.grep sorry— zero.docs/index.md+tex/proof-guide.texsynced; proof-guide compiles (no new errors/undefined); no Japanese.🤖 Generated with Claude Code