feat: Step 576 — polymer incompatibility relation (Mayer expansion foundation, GJ §18.4) - #1418
Merged
Merged
Conversation
…undation, GJ §18.4) Empty start commit. Defines PolymersIncompatible foundation for cluster expansion / Mayer expansion. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…undation, GJ §18.4)
Introduce `PolymersIncompatible P Q := ¬ Disjoint (polymerSupport P) (polymerSupport Q)`
as the foundation for cluster decomposition and Mayer expansion:
- `Decidable` instance (inherited from `Disjoint` on `Finset`)
- `symm` via `disjoint_comm`
- `iff_not_isPolymerVertexDisjoint`: definitional equality (`Iff.rfl`) since
`IsPolymerVertexDisjoint` is literally `Disjoint (polymerSupport _) (polymerSupport _)`
- `iff_exists_shared_vertex` via `Finset.not_disjoint_iff`
- `self_of_isPolymer`: a non-empty polymer is incompatible with itself,
reflecting the multi-set convention for clusters in Mayer expansion
(FV §5.7: clusters are multi-sets where polymers can repeat)
This is the first step toward the §18.4 deferred Mayer expansion:
`log Ξ = ∑_{clusters} Ursell coefficient · ∏ activity`. The clusters
are connected components of the incompatibility graph defined by this
relation.
Cross-checked with codex (FV §5.7 alignment, self-incompatibility
convention, Lean proof soundness all confirmed).
Co-Authored-By: Claude Opus 4.7 (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.
Part of #1344
Summary
PolymersIncompatible P Q := ¬ Disjoint (polymerSupport P) (polymerSupport Q)as the foundation of cluster decomposition for Mayer expansionDisjointdecidable onFinset)disjoint_commmem_polymerSupport_inter)IsPolymerVertexDisjointMotivation
The §18.4 deferred item "Mayer expansion: log Ξ = ∑ Ursell terms" requires a notion of cluster: a multi-set of polymers whose incompatibility graph is connected. This PR introduces the underlying incompatibility relation as the smallest foundation step.
Test plan
lake buildsucceedslake exe GKSTestpassesgrep -rn "sorry" IsingModel/is zerodocs/index.mdupdated (§18.4 row)🤖 Generated with Claude Code