feat: Step 572 — parity transition lemma evenSubgraph_pair_boundary_erase_swap (GJ §18.7) - #1414
Merged
Merged
Conversation
phasetr
changed the title
…rase_swap (GJ §18.7)
Adds evenSubgraph_pair_boundary_erase_swap: for X with ∂X = {i, j} (FV
(3.46) numerator filter at A = {i, j}) and an edge s(i, k) ∈ X with
k ≠ i, k ≠ j, erasing the edge yields X.erase s(i, k) with
∂(X.erase s(i, k)) = {k, j}.
Encodes the boundary-flip ∂(X.erase e) = ∂X △ {endpoints of e}: erasing
edge s(i, k) flips parity at both endpoints i and k (Step 570), turning
i's odd degree into even (i leaves boundary) and k's even degree into
odd (k joins boundary). j's parity is preserved.
Proof by 4-way case analysis on v relative to i, j, k:
- v = i: indicators (1, 1, 0) for ({i,j}, s(i,k), {k,j}); parity check
via Nat.even_add and Even 2.
- v = j: indicators (1, 0, 1); direct.
- v = k: indicators (0, 1, 1); direct.
- v ∉ {i, j, k}: indicators (0, 0, 0); direct.
Also adds `import Mathlib.Combinatorics.SimpleGraph.Metric` to bring
SimpleGraph.dist and Walk into scope for the upcoming Step 573 dist
bound (the inductive capstone using Steps 569+570+571+572).
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
evenSubgraph_pair_boundary_erase_swap: for ∂X = {i, j}, edges(i, k) ∈ Xwithk ∉ {i, j}, erasing the edge moves the boundary to{k, j}.∂(X.erase s(i, k)) = ∂X △ {i, k}underlying the inductive proof of the graph-distance bound.import Mathlib.Combinatorics.SimpleGraph.Metric(preparation for the dist bound in Step 573+).Proof
4-way case analysis on
vvsi,j,k:v = i: indicators(1, 1, 0)for({i,j}, s(i,k), {k,j}).Even(1+a+1) ↔ Even a ↔ Even(0+a). ✓v = j:(1, 0, 1). ✓v = k:(0, 1, 1). ✓v ∉ {i, j, k}:(0, 0, 0). ✓Test plan
lake buildclean