feat: correlation factorization on disjoint sum graph — #2965#2975
Merged
Conversation
Add the component-factorization core (missing from SumModel.lean): - spinProduct_map_inl / spinProduct_map_inr: an inl/inr-supported observable on Sum.elim σ₁ σ₂ depends only on the matching component. - correlation_sum_inl: correlation (G ⊕g H) p (A.map inl) = correlation G p A - correlation_sum_inr: correlation (G ⊕g H) p (B.map inr) = correlation H p B An observable inside one connected component is unaffected by the disjoint other component: the opposite-component partition factor cancels between numerator and Z (via Config.sumEquiv, hamiltonian_sum, partitionFunction_sum). This is the bridge needed to translate the bond-deletion increment (correlation_sub_deleteEdges_le_derivBound) into a finite-volume exhaustion-stage increment. Part of #2965 Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
) Per codex cross-check: clarify correlation_sum_inl/inr is disjoint-sum factorization (one inl/inr summand, not necessarily connected), and that the deleteEdges→box-sum graph-isomorphism bridge to the exhaustion-stage increment remains a separate step. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This was referenced May 26, 2026
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
Adds the component-factorization core (previously missing from
SumModel.lean, which hadpartitionFunction_sumbut no correlation version):spinProduct_map_inl/spinProduct_map_inr: aninl/inr-supported observable onSum.elim σ₁ σ₂depends only on the matching component.correlation_sum_inl:correlation (G ⊕g H) p (A.map inl) = correlation G p Acorrelation_sum_inr:correlation (G ⊕g H) p (B.map inr) = correlation H p BAn observable inside one connected component is unaffected by the disjoint other component: the opposite-component partition factor cancels between numerator and
Z(viaConfig.sumEquiv,hamiltonian_sum,partitionFunction_sum). This is the bridge needed to translate the bond-deletion increment (correlation_sub_deleteEdges_le_derivBound, #2974) into a finite-volume exhaustion-stage increment.lake build IsingModel.SumModelgreen, sorry 0, linter clean, tex compiles.🤖 Generated with Claude Code