Fixed-Host Colored Deletion Decks

This module starts the Lean infrastructure for the fixed-host singleton analysis in proof_sketch.tex.

The fixed-host problem keeps one graph K fixed and compares subsets U V : Set V by the colored vertex-deletion decks of (K, S, U) and (K, S, V), where S is a passive first color and U/V are the active second colors.

The definitions here are intentionally modest: colored card isomorphisms, deleted colors, fixed-host same-deck, and the one-hole/two-hole cards used in the low/complementary rectangular boundary.

theorem SimpleGraph.exists_positive_iterate_eq_self_of_finite {α : Type u_3} [Finite α] [Nonempty α] (f : α → α) : ∃ (x : α) (n : ℕ), 0 < n ∧ f^[n] x = x

A finite nonempty self-map has a positive-period orbit point. This is the generic finite-dynamics fact used below for chosen active successor systems.

structure SimpleGraph.TwoColorIso {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (H : SimpleGraph W) (S T : Set V) (S' T' : Set W) : Type (max u_1 u_2)

A graph isomorphism preserving two vertex colors.

• iso : G ≃g H
• map_first (v : V) : v ∈ S ↔ self.iso.toEquiv v ∈ S'
• map_second (v : V) : v ∈ T ↔ self.iso.toEquiv v ∈ T'

def SimpleGraph.TwoColorIso.refl {V : Type u_1} (G : SimpleGraph V) (S T : Set V) : G.TwoColorIso G S T S T

The identity two-colored isomorphism.

Equations

• SimpleGraph.TwoColorIso.refl G S T = { iso := SimpleGraph.Iso.refl, map_first := ⋯, map_second := ⋯ }

def SimpleGraph.TwoColorIso.symm {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {S T : Set V} {S' T' : Set W} (e : G.TwoColorIso H S T S' T') : H.TwoColorIso G S' T' S T

Reverse a two-colored isomorphism.

Equations

• e.symm = { iso := e.iso.symm, map_first := ⋯, map_second := ⋯ }

def SimpleGraph.TwoColorIso.trans {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {H : SimpleGraph W} {L : SimpleGraph X} {S T : Set V} {S' T' : Set W} {S'' T'' : Set X} (e₁ : G.TwoColorIso H S T S' T') (e₂ : H.TwoColorIso L S' T' S'' T'') : G.TwoColorIso L S T S'' T''

Compose two two-colored isomorphisms.

Equations

• e₁.trans e₂ = { iso := RelIso.trans e₁.iso e₂.iso, map_first := ⋯, map_second := ⋯ }

def SimpleGraph.twinDifferenceSet {V : Type u_1} (K : SimpleGraph V) (u v : V) : Set V

The set of vertices on which two vertices u and v have different adjacency in K, excluding u and v themselves. This is the neighborhood-symmetric-difference set. When u, v are twins in K, this set is empty.

Equations

• K.twinDifferenceSet u v = {w : V | w ≠ u ∧ w ≠ v ∧ (K.Adj u w ↔ ¬K.Adj v w)}

def SimpleGraph.AreTwins {V : Type u_1} (K : SimpleGraph V) (u v : V) : Prop

Two vertices u and v are K-twins when they have the same neighbors among all other vertices.

Equations

• K.AreTwins u v = ∀ (w : V), w ≠ u → w ≠ v → (K.Adj u w ↔ K.Adj v w)

theorem SimpleGraph.twinDifferenceSet_eq_empty_iff_areTwins {V : Type u_1} {K : SimpleGraph V} {u v : V} : K.twinDifferenceSet u v = ∅ ↔ K.AreTwins u v

Twin equivalence: the twin-difference set is empty iff u and v are twins.

theorem SimpleGraph.twinDifferenceSet_comm {V : Type u_1} (K : SimpleGraph V) (u v : V) : K.twinDifferenceSet u v = K.twinDifferenceSet v u

The twin-difference set is symmetric in its two arguments.

theorem SimpleGraph.AreTwins.symm {V : Type u_1} {K : SimpleGraph V} {u v : V} (h : K.AreTwins u v) : K.AreTwins v u

Twins is symmetric.

theorem SimpleGraph.AreTwins.refl {V : Type u_1} (K : SimpleGraph V) (u : V) : K.AreTwins u u

Twins is reflexive: every vertex is a twin of itself.

def SimpleGraph.deleteColor {V : Type u_1} (A : Set V) (z : V) : Set { w : V // w ≠ z }

Delete a vertex from a vertex color.

Equations

• SimpleGraph.deleteColor A z = {w : { w : V // w ≠ z } | ↑w ∈ A}

@[simp]

theorem SimpleGraph.mem_deleteColor {V : Type u_1} (A : Set V) (z : V) (w : { w : V // w ≠ z }) : w ∈ deleteColor A z ↔ ↑w ∈ A

@[reducible, inline]

abbrev SimpleGraph.fixedHostCardGraph {V : Type u_1} (K : SimpleGraph V) (z : V) : SimpleGraph { w : V // w ≠ z }

The fixed-host colored card obtained from (K, S, U) by deleting z.

Equations

• K.fixedHostCardGraph z = K.deleteVert z

def SimpleGraph.FixedHostCardIso {V : Type u_1} (K : SimpleGraph V) (S U V' : Set V) (z w : V) : Prop

Two fixed-host colored cards are isomorphic.

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.FixedHostCardIso.symm {V : Type u_1} {K : SimpleGraph V} {S U V' : Set V} {z w : V} (h : K.FixedHostCardIso S U V' z w) : K.FixedHostCardIso S V' U w z

Fixed-host colored card isomorphism is symmetric.

def SimpleGraph.FixedHostSameDeck {V : Type u_1} (K : SimpleGraph V) (S U V' : Set V) : Prop

Equality of fixed-host two-colored deletion decks, represented by a matching of deleted vertices.

Equations

• K.FixedHostSameDeck S U V' = ∃ (σ : V ≃ V), ∀ (z : V), K.FixedHostCardIso S U V' z (σ z)

def SimpleGraph.FixedHostSameSubdeck {V : Type u_1} (K : SimpleGraph V) (S U V' R R' : Set V) : Prop

Equality of restricted fixed-host two-colored deletion decks. The deleted vertices on the left are restricted to R, and the deleted vertices on the right are restricted to R'.

This is the Lean object corresponding to a single color-size slice in the fixed-host singleton argument.

Equations

• K.FixedHostSameSubdeck S U V' R R' = ∃ (σ : ↑R ≃ ↑R'), ∀ (z : ↑R), K.FixedHostCardIso S U V' ↑z ↑(σ z)

theorem SimpleGraph.FixedHostSameDeck.refl {V : Type u_1} (K : SimpleGraph V) (S U : Set V) : K.FixedHostSameDeck S U U

Fixed-host same-deck is reflexive.

theorem SimpleGraph.FixedHostSameDeck.symm {V : Type u_1} {K : SimpleGraph V} {S U V' : Set V} (h : K.FixedHostSameDeck S U V') : K.FixedHostSameDeck S V' U

Fixed-host same-deck is symmetric.

theorem SimpleGraph.FixedHostSameSubdeck.refl {V : Type u_1} (K : SimpleGraph V) (S U R : Set V) : K.FixedHostSameSubdeck S U U R R

Restricted fixed-host same-deck is reflexive.

theorem SimpleGraph.FixedHostSameSubdeck.symm {V : Type u_1} {K : SimpleGraph V} {S U V' R R' : Set V} (h : K.FixedHostSameSubdeck S U V' R R') : K.FixedHostSameSubdeck S V' U R' R

Restricted fixed-host same-deck is symmetric.

def SimpleGraph.singletonLeft {V : Type u_1} (T : Set V) (a : V) : Set V

The left singleton second color T ∪ {a}.

Equations

• SimpleGraph.singletonLeft T a = T ∪ {a}

@[simp]

theorem SimpleGraph.mem_singletonLeft {V : Type u_1} (T : Set V) (a x : V) : x ∈ singletonLeft T a ↔ x ∈ T ∨ x = a

def SimpleGraph.singletonRight {V : Type u_1} (T : Set V) (b : V) : Set V

The right singleton second color T ∪ {b}.

Equations

• SimpleGraph.singletonRight T b = T ∪ {b}

@[simp]

theorem SimpleGraph.mem_singletonRight {V : Type u_1} (T : Set V) (b x : V) : x ∈ singletonRight T b ↔ x ∈ T ∨ x = b

def SimpleGraph.singletonOutside {V : Type u_1} (T : Set V) (a b : V) : Set V

The outside set O = V(K) \ (T ∪ {a,b}) in the singleton switch.

Equations

• SimpleGraph.singletonOutside T a b = {x : V | x ∉ T ∧ x ≠ a ∧ x ≠ b}

@[simp]

theorem SimpleGraph.mem_singletonOutside {V : Type u_1} (T : Set V) (a b x : V) : x ∈ singletonOutside T a b ↔ x ∉ T ∧ x ≠ a ∧ x ≠ b

def SimpleGraph.complementaryDeleteLeft {V : Type u_1} (T : Set V) (a b : V) : Set V

Vertices deleted in the complementary slice on the a-side: O ∪ {b}.

Equations

• SimpleGraph.complementaryDeleteLeft T a b = SimpleGraph.singletonOutside T a b ∪ {b}

@[simp]

theorem SimpleGraph.mem_complementaryDeleteLeft {V : Type u_1} (T : Set V) (a b x : V) : x ∈ complementaryDeleteLeft T a b ↔ x ∈ singletonOutside T a b ∨ x = b

def SimpleGraph.complementaryDeleteRight {V : Type u_1} (T : Set V) (a b : V) : Set V

Vertices deleted in the complementary slice on the b-side: O ∪ {a}.

Equations

• SimpleGraph.complementaryDeleteRight T a b = SimpleGraph.singletonOutside T a b ∪ {a}

@[simp]

theorem SimpleGraph.mem_complementaryDeleteRight {V : Type u_1} (T : Set V) (a b x : V) : x ∈ complementaryDeleteRight T a b ↔ x ∈ singletonOutside T a b ∨ x = a

def SimpleGraph.FixedHostSingletonState {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The fixed-host singleton hypotheses: the active second color changes from T ∪ {a} to T ∪ {b} and the fixed-host colored decks agree.

Equations

• K.FixedHostSingletonState S T a b = (a ∉ T ∧ b ∉ T ∧ a ≠ b ∧ K.FixedHostSameDeck S (SimpleGraph.singletonLeft T a) (SimpleGraph.singletonRight T b))

def SimpleGraph.FixedHostSingletonSolved {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The desired singleton conclusion: a color-preserving automorphism of the fixed host carries T ∪ {a} to T ∪ {b}.

Equations

• K.FixedHostSingletonSolved S T a b = Nonempty (K.TwoColorIso K S (SimpleGraph.singletonLeft T a) S (SimpleGraph.singletonRight T b))

def SimpleGraph.FixedHostSingletonConjecture {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The fixed-host singleton conjecture as a Lean proposition.

Equations

• K.FixedHostSingletonConjecture S T a b = (K.FixedHostSingletonState S T a b → K.FixedHostSingletonSolved S T a b)

def SimpleGraph.LowSliceSameDeck {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

Equality of the low color-size slice {{H_a}} + {{A_t : t ∈ T}} = {{H_b}} + {{B_t : t ∈ T}}, represented by a matching between the second-colored deletion vertices.

Equations

• K.LowSliceSameDeck S T a b = K.FixedHostSameSubdeck S (SimpleGraph.singletonLeft T a) (SimpleGraph.singletonRight T b) (SimpleGraph.singletonLeft T a) (SimpleGraph.singletonRight T b)

def SimpleGraph.ComplementarySliceSameDeck {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

Equality of the complementary color-size slice {{C_b^a}} + {{C_o^a : o ∈ O}} = {{C_a^b}} + {{C_o^b : o ∈ O}}, represented by a matching between the non-second-colored deletion vertices.

Equations

• One or more equations did not get rendered due to their size.

def SimpleGraph.LowSliceOrbitReconstruction {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

A sharper possible route: the low slice alone reconstructs the fixed-host orbit of the singleton color set.

Equations

• K.LowSliceOrbitReconstruction S T a b = (K.LowSliceSameDeck S T a b → K.FixedHostSingletonSolved S T a b)

structure SimpleGraph.FixedHostCardIsoData {V : Type u_1} (K : SimpleGraph V) (S U U' : Set V) (x y : V) : Type u_1

A chosen fixed-host card isomorphism. Unlike FixedHostCardIso, this remembers the actual card map, so we can ask whether its deleted-vertex star extends correctly.

• cardIso : (K.deleteVert x).TwoColorIso (K.deleteVert y) (deleteColor S x) (deleteColor U x) (deleteColor S y) (deleteColor U' y)

theorem SimpleGraph.FixedHostCardIsoData.cardIsoProp {V : Type u_1} {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) : K.FixedHostCardIso S U U' x y

A chosen fixed-host card isomorphism gives the corresponding existential card isomorphism.

def SimpleGraph.FixedHostCardIsoData.ZeroStarError {V : Type u_1} {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) : Prop

The deleted-vertex star error is zero when the card isomorphism transports the neighbors of the left deleted vertex to the neighbors of the right deleted vertex.

Equations

• e.ZeroStarError = ∀ (z : { w : V // w ≠ x }), K.Adj x ↑z ↔ K.Adj y ↑(e.cardIso.iso.toEquiv z)

def SimpleGraph.FixedHostCardIsoData.StarMismatch {V : Type u_1} {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) (z : { w : V // w ≠ x }) : Prop

A concrete failed adjacency in the deleted star of a chosen card isomorphism.

Equations

• e.StarMismatch z = ¬(K.Adj x ↑z ↔ K.Adj y ↑(e.cardIso.iso.toEquiv z))

def SimpleGraph.FixedHostCardIsoData.ActiveStarMismatch {V : Type u_1} {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) (z : { w : V // w ≠ x }) : Prop

A star mismatch whose source endpoint remains active after deleting x.

Equations

• e.ActiveStarMismatch z = (e.StarMismatch z ∧ ↑z ∈ U)

theorem SimpleGraph.FixedHostCardIsoData.zeroStarError_iff_no_starMismatch {V : Type u_1} {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) : e.ZeroStarError ↔ ∀ (z : { w : V // w ≠ x }), ¬e.StarMismatch z

Zero star error is the same as having no concrete star mismatch.

theorem SimpleGraph.FixedHostCardIsoData.exists_starMismatch_of_not_zeroStarError {V : Type u_1} {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) (h : ¬e.ZeroStarError) : ∃ (z : { w : V // w ≠ x }), e.StarMismatch z

A nonzero star error has a concrete witness.

theorem SimpleGraph.FixedHostCardIsoData.zeroStarError_of_no_starMismatch {V : Type u_1} {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) (h : ∀ (z : { w : V // w ≠ x }), ¬e.StarMismatch z) : e.ZeroStarError

If every concrete mismatch is absent, the star error is zero.

theorem SimpleGraph.FixedHostCardIsoData.map_first_iff {V : Type u_1} {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) (z : { w : V // w ≠ x }) : ↑z ∈ S ↔ ↑(e.cardIso.iso.toEquiv z) ∈ S

The chosen card map preserves the first color away from the deleted vertices.

theorem SimpleGraph.FixedHostCardIsoData.map_second_iff {V : Type u_1} {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) (z : { w : V // w ≠ x }) : ↑z ∈ U ↔ ↑(e.cardIso.iso.toEquiv z) ∈ U'

The chosen card map carries the left second color to the right second color away from the deleted vertices.

noncomputable def SimpleGraph.FixedHostCardIsoData.starErrorCount {V : Type u_1} [Finite V] {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) : ℕ

The number of deleted-star adjacencies on which a chosen card isomorphism fails to extend.

Equations

• e.starErrorCount = Fintype.card { z : { w : V // w ≠ x } // e.StarMismatch z }

theorem SimpleGraph.FixedHostCardIsoData.starErrorCount_eq_zero_iff {V : Type u_1} [Finite V] {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) : e.starErrorCount = 0 ↔ e.ZeroStarError

The star-error count is zero exactly when the deleted star is transported correctly.

theorem SimpleGraph.FixedHostCardIsoData.starErrorCount_pos_iff {V : Type u_1} [Finite V] {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) : 0 < e.starErrorCount ↔ ¬e.ZeroStarError

Positive star-error count is the same as nonzero deleted-star error.

theorem SimpleGraph.FixedHostCardIsoData.starErrorCount_even {V : Type u_1} [Finite V] {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) : Even e.starErrorCount

The star-error count of a chosen card isomorphism is even.

This is the deleted-star parity lemma: the chosen card isomorphism gives an isomorphism between the two deleted-vertex graphs, hence the deleted vertices have equal degree. The star-error count is the size of the symmetric difference of the two neighborhoods (as transported through the card iso), which has the same parity as the sum of the degrees, which is even since the degrees agree.

theorem SimpleGraph.FixedHostCardIsoData.deletedFirstColor_card_lt_of_mem {V : Type u_1} [Fintype V] [DecidableEq V] {S : Set V} [DecidablePred fun (w : V) => w ∈ S] {x : V} (hx : x ∈ S) : Fintype.card { w : V // w ≠ x ∧ w ∈ S } < Fintype.card { w : V // w ∈ S }

If the deleted vertex is first-colored, then the first-colored part of the deleted card is strictly smaller than the full first color.

theorem SimpleGraph.FixedHostCardIsoData.deletedFirstColor_card_eq_of_not_mem {V : Type u_1} [Fintype V] [DecidableEq V] {S : Set V} [DecidablePred fun (w : V) => w ∈ S] {x : V} (hx : x ∉ S) : Fintype.card { w : V // w ≠ x ∧ w ∈ S } = Fintype.card { w : V // w ∈ S }

If the deleted vertex is not first-colored, then deleting it does not change the size of the first-colored part of the card.

theorem SimpleGraph.FixedHostCardIsoData.card_firstColor_eq {V : Type u_1} [Fintype V] [DecidableEq V] {K : SimpleGraph V} {S U U' : Set V} [DecidablePred fun (w : V) => w ∈ S] {x y : V} (e : K.FixedHostCardIsoData S U U' x y) : Fintype.card { w : V // w ≠ x ∧ w ∈ S } = Fintype.card { w : V // w ≠ y ∧ w ∈ S }

A first-color-preserving card isomorphism identifies the cardinalities of the first-colored parts of the two deleted cards.

theorem SimpleGraph.FixedHostCardIsoData.firstColor_deleted_status_iff {V : Type u_1} [Finite V] {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) : x ∈ S ↔ y ∈ S

In a finite host, the first-color status of the deleted vertex is visible from any first-color-preserving card isomorphism.

def SimpleGraph.FixedHostCardIsoData.extendedEquiv {V : Type u_1} [DecidableEq V] {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) : V ≃ V

Extend a card bijection between K - x and K - y to the full vertex set by sending the left deleted vertex x to the right deleted vertex y.

Equations

• e.extendedEquiv = (Equiv.optionSubtypeNe x).symm.trans (e.cardIso.iso.optionCongr.trans (Equiv.optionSubtypeNe y))

@[simp]

theorem SimpleGraph.FixedHostCardIsoData.extendedEquiv_apply_deleted {V : Type u_1} [DecidableEq V] {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) : e.extendedEquiv x = y

theorem SimpleGraph.FixedHostCardIsoData.extendedEquiv_apply_ne {V : Type u_1} [DecidableEq V] {K : SimpleGraph V} {S U U' : Set V} {x y z : V} (e : K.FixedHostCardIsoData S U U' x y) (hz : z ≠ x) : e.extendedEquiv z = ↑(e.cardIso.iso.toEquiv ⟨z, hz⟩)

def SimpleGraph.FixedHostCardIsoData.extendIsoOfZeroStarError {V : Type u_1} [DecidableEq V] {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) (hstar : e.ZeroStarError) : K ≃g K

A zero-star-error card isomorphism extends to a graph automorphism of the fixed host, sending the deleted vertex on the left to the deleted vertex on the right.

Equations

• e.extendIsoOfZeroStarError hstar = { toEquiv := e.extendedEquiv, map_rel_iff' := ⋯ }

def SimpleGraph.FixedHostCardIsoData.extendTwoColorIsoOfZeroStarError {V : Type u_1} [DecidableEq V] {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) (hFirst : x ∈ S ↔ y ∈ S) (hSecond : x ∈ U ↔ y ∈ U') (hstar : e.ZeroStarError) : K.TwoColorIso K S U S U'

If the deleted vertices have matching color status, then a zero-star-error card isomorphism extends to a two-colored automorphism of the full fixed host.

Equations

• e.extendTwoColorIsoOfZeroStarError hFirst hSecond hstar = { iso := e.extendIsoOfZeroStarError hstar, map_first := ⋯, map_second := ⋯ }

theorem SimpleGraph.FixedHostCardIsoData.nonempty_twoColorIso_of_zeroStarError {V : Type u_1} {K : SimpleGraph V} {S U U' : Set V} {x y : V} (e : K.FixedHostCardIsoData S U U' x y) (hFirst : x ∈ S ↔ y ∈ S) (hSecond : x ∈ U ↔ y ∈ U') (hstar : e.ZeroStarError) : Nonempty (K.TwoColorIso K S U S U')

Nonempty wrapper for the general zero-star card-extension lemma.

def SimpleGraph.FixedHostCardIsoData.ofTwoColorIso {V : Type u_1} {K : SimpleGraph V} {S U U' : Set V} (e : K.TwoColorIso K S U S U') (x : V) : K.FixedHostCardIsoData S U U' x (e.iso.toEquiv x)

Restrict a full two-colored automorphism to the card obtained by deleting x and its image.

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.FixedHostCardIsoData.ofTwoColorIso_zeroStarError {V : Type u_1} {K : SimpleGraph V} {S U U' : Set V} (e : K.TwoColorIso K S U S U') (x : V) : (ofTwoColorIso e x).ZeroStarError

The card restriction of a full automorphism has zero deleted-star error.

theorem SimpleGraph.FixedHostCardIsoData.solved_singleton_of_zeroStarError_active {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b x y : V} (e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) x y) (hFirst : x ∈ S ↔ y ∈ S) (hxActive : x ∈ singletonLeft T a) (hyActive : y ∈ singletonRight T b) (hstar : e.ZeroStarError) : K.FixedHostSingletonSolved S T a b

Singleton-switch specialization of the general zero-star card-extension lemma for a low-slice step deleting active vertices on both sides.

structure SimpleGraph.FixedHostSubdeckIsoData {V : Type u_1} (K : SimpleGraph V) (S U U' R R' : Set V) : Type u_1

A chosen matching of two restricted fixed-host subdecks, including the actual card isomorphism for each matched deleted vertex.

• toEquiv : ↑R ≃ ↑R'
• cardIso (z : ↑R) : K.FixedHostCardIsoData S U U' ↑z ↑(self.toEquiv z)

theorem SimpleGraph.FixedHostSubdeckIsoData.sameSubdeck {V : Type u_1} {K : SimpleGraph V} {S U U' R R' : Set V} (e : K.FixedHostSubdeckIsoData S U U' R R') : K.FixedHostSameSubdeck S U U' R R'

A chosen restricted subdeck matching gives the corresponding existential same-subdeck proposition.

noncomputable def SimpleGraph.FixedHostSubdeckIsoData.ofSameSubdeck {V : Type u_1} {K : SimpleGraph V} {S U U' R R' : Set V} (h : K.FixedHostSameSubdeck S U U' R R') : K.FixedHostSubdeckIsoData S U U' R R'

Choose concrete card isomorphisms from an existential restricted subdeck matching.

Equations

• SimpleGraph.FixedHostSubdeckIsoData.ofSameSubdeck h = { toEquiv := Classical.choose h, cardIso := fun (z : ↑R) => { cardIso := Classical.choice ⋯ } }

@[reducible, inline]

abbrev SimpleGraph.LowSliceIsoData {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Type u_1

A chosen low-slice matching for the singleton switch.

Equations

• K.LowSliceIsoData S T a b = K.FixedHostSubdeckIsoData S (SimpleGraph.singletonLeft T a) (SimpleGraph.singletonRight T b) (SimpleGraph.singletonLeft T a) (SimpleGraph.singletonRight T b)

def SimpleGraph.LowSliceZeroStarPair {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The active zero-star pair target: some low-slice card match deletes an active vertex on each side, has matching first-color status, and has zero deleted-star error.

Equations

• One or more equations did not get rendered due to their size.

structure SimpleGraph.LowSliceZeroStarMatching {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Type u_1

A perfect zero-star matching of the active deletion deck. This is the global version of LowSliceZeroStarPair: every active deleted vertex is matched to an active deleted vertex by a card isomorphism whose deleted-star error is zero.

• toEquiv : ↑(singletonLeft T a) ≃ ↑(singletonRight T b)
• cardIso (x : ↑(singletonLeft T a)) : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑(self.toEquiv x)
• first_status (x : ↑(singletonLeft T a)) : ↑x ∈ S ↔ ↑(self.toEquiv x) ∈ S
• zero_star (x : ↑(singletonLeft T a)) : (self.cardIso x).ZeroStarError

theorem SimpleGraph.LowSliceZeroStarMatching.solved {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (m : K.LowSliceZeroStarMatching S T a b) : K.FixedHostSingletonSolved S T a b

A perfect zero-star matching solves the singleton switch.

noncomputable def SimpleGraph.LowSliceZeroStarMatching.of_solved {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (h : K.FixedHostSingletonSolved S T a b) : K.LowSliceZeroStarMatching S T a b

Any full solution induces a perfect zero-star matching of the active deletion deck.

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.LowSliceZeroStarMatching.nonempty_iff_solved {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} : Nonempty (K.LowSliceZeroStarMatching S T a b) ↔ K.FixedHostSingletonSolved S T a b

Existence of a perfect zero-star matching is equivalent to the desired orbit conclusion.

theorem SimpleGraph.LowSliceZeroStarMatching.to_pair {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (m : K.LowSliceZeroStarMatching S T a b) : K.LowSliceZeroStarPair S T a b

A perfect zero-star matching contains, in particular, an active zero-star pair.

theorem SimpleGraph.LowSliceZeroStarPair.solved {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (h : K.LowSliceZeroStarPair S T a b) : K.FixedHostSingletonSolved S T a b

An active zero-star pair is enough to solve the singleton switch.

theorem SimpleGraph.LowSliceZeroStarPair.of_solved {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (h : K.FixedHostSingletonSolved S T a b) : K.LowSliceZeroStarPair S T a b

Conversely, any full solution restricts to an active zero-star pair. Thus LowSliceZeroStarPair is the orbit conclusion packaged as a deck-visible witness.

theorem SimpleGraph.LowSliceZeroStarPair.iff_solved {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} : K.LowSliceZeroStarPair S T a b ↔ K.FixedHostSingletonSolved S T a b

Active zero-star pairs are equivalent to the desired fixed-host singleton orbit conclusion.

theorem SimpleGraph.LowSliceZeroStarPair.iff_nonempty_zeroStarMatching {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} : K.LowSliceZeroStarPair S T a b ↔ Nonempty (K.LowSliceZeroStarMatching S T a b)

The one-pair and perfect-matching zero-star formulations are equivalent. The perfect matching is not extra mathematics: a full solution induces one, and any one of its edges is already enough.

theorem SimpleGraph.LowSliceZeroStarPair.exists_starMismatch_of_no_pair {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (hno : ¬K.LowSliceZeroStarPair S T a b) (x : ↑(singletonLeft T a)) (y : ↑(singletonRight T b)) (e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y) (hFirst : ↑x ∈ S ↔ ↑y ∈ S) : ∃ (z : { w : V // w ≠ ↑x }), e.StarMismatch z

In a no-zero-star-pair obstruction, every active card match has a concrete deleted-star mismatch.

theorem SimpleGraph.LowSliceZeroStarPair.no_pair_iff_all_matches_have_starMismatch {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} : ¬K.LowSliceZeroStarPair S T a b ↔ ∀ (x : ↑(singletonLeft T a)) (y : ↑(singletonRight T b)) (e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y), (↑x ∈ S ↔ ↑y ∈ S) → ∃ (z : { w : V // w ≠ ↑x }), e.StarMismatch z

Normal form for the local obstruction: there is no active zero-star pair exactly when every active card match has a concrete deleted-star mismatch.

def SimpleGraph.LowSliceZeroStarPairConjecture {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The current focused local conjecture: low-slice equality exposes an active zero-star pair.

Equations

• K.LowSliceZeroStarPairConjecture S T a b = (K.LowSliceSameDeck S T a b → K.LowSliceZeroStarPair S T a b)

theorem SimpleGraph.LowSliceOrbitReconstruction.of_zeroStarPair {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (h : K.LowSliceZeroStarPairConjecture S T a b) : K.LowSliceOrbitReconstruction S T a b

The active zero-star pair conjecture implies the low-slice orbit reconstruction target.

theorem SimpleGraph.LowSliceZeroStarPairConjecture.iff_orbitReconstruction {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} : K.LowSliceZeroStarPairConjecture S T a b ↔ K.LowSliceOrbitReconstruction S T a b

The active-zero-star formulation is equivalent to low-slice orbit reconstruction; it is a local witness formulation of the same target.

noncomputable def SimpleGraph.LowSliceIsoData.ofSameDeck {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (h : K.LowSliceSameDeck S T a b) : K.LowSliceIsoData S T a b

Choose a concrete low-slice matching from low-slice deck equality.

Equations

• SimpleGraph.LowSliceIsoData.ofSameDeck h = SimpleGraph.FixedHostSubdeckIsoData.ofSameSubdeck h

theorem SimpleGraph.LowSliceIsoData.first_status {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (e : K.LowSliceIsoData S T a b) (x : ↑(singletonLeft T a)) : ↑x ∈ S ↔ ↑(e.toEquiv x) ∈ S

In finite hosts, every chosen low-slice card match has matching passive first-color status.

theorem SimpleGraph.LowSliceIsoData.solved_of_zeroStarError_at {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (e : K.LowSliceIsoData S T a b) (x : ↑(singletonLeft T a)) (hFirst : ↑x ∈ S ↔ ↑(e.toEquiv x) ∈ S) (hstar : (e.cardIso x).ZeroStarError) : K.FixedHostSingletonSolved S T a b

If one matched low-slice card has zero star error and the two deleted vertices have the same passive first-color status, then that single card match extends to a full solution of the singleton switch.

def SimpleGraph.LowSliceIsoData.toZeroStarMatching {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (e : K.LowSliceIsoData S T a b) (hFirst : ∀ (x : ↑(singletonLeft T a)), ↑x ∈ S ↔ ↑(e.toEquiv x) ∈ S) (hstar : ∀ (x : ↑(singletonLeft T a)), (e.cardIso x).ZeroStarError) : K.LowSliceZeroStarMatching S T a b

If every chosen low-slice card match has zero star error and matching first-color status, then the chosen low-slice matching is a perfect zero-star matching.

Equations

• e.toZeroStarMatching hFirst hstar = { toEquiv := e.toEquiv, cardIso := e.cardIso, first_status := hFirst, zero_star := hstar }

@[reducible, inline]

abbrev SimpleGraph.ComplementarySliceIsoData {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Type u_1

A chosen complementary-slice matching for the singleton switch.

Equations

• One or more equations did not get rendered due to their size.

def SimpleGraph.ComplementarySliceZeroStarPair {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The complementary-slice zero-star pair target: some complementary-slice card match deletes a vertex from O ∪ {b} on the left and O ∪ {a} on the right, with matching first-color status, and has zero deleted-star error.

A complementary zero-star pair plays the same role as a low-slice zero-star pair: it extends to a full fixed-host singleton solution. The two slices give two independent routes to orbit success.

Equations

• One or more equations did not get rendered due to their size.

structure SimpleGraph.ComplementarySliceZeroStarMatching {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Type u_1

A perfect complementary-slice zero-star matching: every complementary-slice deleted vertex on the left is matched to a complementary-slice deleted vertex on the right by a card isomorphism whose deleted-star error is zero.

• toEquiv : ↑(complementaryDeleteLeft T a b) ≃ ↑(complementaryDeleteRight T a b)
• cardIso (x : ↑(complementaryDeleteLeft T a b)) : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑(self.toEquiv x)
• first_status (x : ↑(complementaryDeleteLeft T a b)) : ↑x ∈ S ↔ ↑(self.toEquiv x) ∈ S
• zero_star (x : ↑(complementaryDeleteLeft T a b)) : (self.cardIso x).ZeroStarError

theorem SimpleGraph.FixedHostCardIsoData.solved_singleton_of_zeroStarError_complementary {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b x y : V} (e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) x y) (hFirst : x ∈ S ↔ y ∈ S) (hxNotActive : x ∉ singletonLeft T a) (hyNotActive : y ∉ singletonRight T b) (hstar : e.ZeroStarError) : K.FixedHostSingletonSolved S T a b

Singleton-switch specialization of the general zero-star card-extension lemma for a complementary-slice step deleting non-singleton vertices on both sides.

theorem SimpleGraph.ComplementarySliceZeroStarPair.mem_not_active_of_b_not_active {V : Type u_1} {T : Set V} {a b : V} (hb : b ∉ singletonLeft T a) {x : V} (hx : x ∈ complementaryDeleteLeft T a b) : x ∉ singletonLeft T a

A vertex in complementaryDeleteLeft is outside singletonLeft, provided the endpoint b itself is not active. This is the non-degeneracy assumption that b ∉ T ∪ {a} — typically holds in the singleton-switch setup.

theorem SimpleGraph.ComplementarySliceZeroStarPair.mem_not_active_right_of_a_not_active {V : Type u_1} {T : Set V} {a b : V} (ha : a ∉ singletonRight T b) {y : V} (hy : y ∈ complementaryDeleteRight T a b) : y ∉ singletonRight T b

Analogous: a vertex in complementaryDeleteRight is outside singletonRight, provided a ∉ T ∪ {b}.

theorem SimpleGraph.ComplementarySliceZeroStarPair.solved {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (hb : b ∉ singletonLeft T a) (ha : a ∉ singletonRight T b) (h : K.ComplementarySliceZeroStarPair S T a b) : K.FixedHostSingletonSolved S T a b

A complementary-slice zero-star pair is enough to solve the singleton switch, provided a, b are genuinely "outside" the active colors of the other side (the standard non-degeneracy: b ∉ T ∪ {a} and a ∉ T ∪ {b}).

theorem SimpleGraph.ComplementarySliceZeroStarMatching.to_pair {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (m : K.ComplementarySliceZeroStarMatching S T a b) (hne : Nonempty ↑(complementaryDeleteLeft T a b)) : K.ComplementarySliceZeroStarPair S T a b

Any chosen complementary-slice zero-star matching produces a complementary-slice zero-star pair.

theorem SimpleGraph.ComplementarySliceZeroStarMatching.solved {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (hb : b ∉ singletonLeft T a) (ha : a ∉ singletonRight T b) (m : K.ComplementarySliceZeroStarMatching S T a b) : K.FixedHostSingletonSolved S T a b

A perfect complementary-slice zero-star matching solves the singleton switch (given the non-degeneracy assumptions on a and b).

theorem SimpleGraph.ComplementarySliceZeroStarPair.of_solved {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (hb : b ∉ singletonLeft T a) (h : K.FixedHostSingletonSolved S T a b) : K.ComplementarySliceZeroStarPair S T a b

Conversely, any full singleton-switch solution restricts to a complementary-slice zero-star pair, using b on the left side.

theorem SimpleGraph.ComplementarySliceZeroStarPair.iff_solved {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (hb : b ∉ singletonLeft T a) (ha : a ∉ singletonRight T b) : K.ComplementarySliceZeroStarPair S T a b ↔ K.FixedHostSingletonSolved S T a b

Complementary-slice zero-star pairs are equivalent to the desired fixed-host singleton orbit conclusion (given non-degeneracy on a, b).

@[reducible, inline]

abbrev SimpleGraph.deleteTwoVertex {V : Type u_1} (t o : V) : Type u_1

The two-hole vertex type obtained by deleting t and o.

Equations

• SimpleGraph.deleteTwoVertex t o = { x : V // x ≠ t ∧ x ≠ o }

def SimpleGraph.deleteTwo {V : Type u_1} (K : SimpleGraph V) (t o : V) : SimpleGraph (deleteTwoVertex t o)

The graph K - {t,o}.

Equations

• K.deleteTwo t o = SimpleGraph.induce {x : V | x ≠ t ∧ x ≠ o} K

def SimpleGraph.deleteTwoColor {V : Type u_1} (A : Set V) (t o : V) : Set (deleteTwoVertex t o)

Delete two vertices from a color.

Equations

• SimpleGraph.deleteTwoColor A t o = {x : SimpleGraph.deleteTwoVertex t o | ↑x ∈ A}

@[simp]

theorem SimpleGraph.mem_deleteTwoColor {V : Type u_1} (A : Set V) (t o : V) (x : deleteTwoVertex t o) : x ∈ deleteTwoColor A t o ↔ ↑x ∈ A

def SimpleGraph.FixedHostCardIsoData.restrictDeleteTwo {V : Type u_1} {K : SimpleGraph V} {S U U' : Set V} {x y z : V} (e : K.FixedHostCardIsoData S U U' x y) (hz : z ≠ x) : (K.deleteTwo x z).TwoColorIso (K.deleteTwo y ↑(e.cardIso.iso.toEquiv ⟨z, hz⟩)) (deleteTwoColor S x z) (deleteTwoColor U x z) (deleteTwoColor S y ↑(e.cardIso.iso.toEquiv ⟨z, hz⟩)) (deleteTwoColor U' y ↑(e.cardIso.iso.toEquiv ⟨z, hz⟩))

Restrict a chosen one-card isomorphism to the two-hole card obtained by also deleting a surviving vertex z. This is the formal version of isolating a star-error witness in a common two-hole base.

Equations

• One or more equations did not get rendered due to their size.

structure SimpleGraph.LowSliceCardFirstError {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) (x : ↑(singletonLeft T a)) (y : ↑(singletonRight T b)) (e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y) : Type u_1

A localized first star error for one active low-slice card match. The witness records both the failed deleted-star adjacency and the common two-hole colored card obtained by deleting the failed surviving vertex as well.

• z : { w : V // w ≠ ↑x }
• mismatch : e.StarMismatch self.z
• twoHoleIso : (K.deleteTwo ↑x ↑self.z).TwoColorIso (K.deleteTwo ↑y ↑(e.cardIso.iso.toEquiv self.z)) (deleteTwoColor S ↑x ↑self.z) (deleteTwoColor (singletonLeft T a) ↑x ↑self.z) (deleteTwoColor S ↑y ↑(e.cardIso.iso.toEquiv self.z)) (deleteTwoColor (singletonRight T b) ↑y ↑(e.cardIso.iso.toEquiv self.z))

def SimpleGraph.LowSliceCardFirstError.imageZ {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} {x : ↑(singletonLeft T a)} {y : ↑(singletonRight T b)} {e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y} (E : K.LowSliceCardFirstError S T a b x y e) : V

The image of the first-error vertex on the right card.

Equations

• E.imageZ = ↑(e.cardIso.iso.toEquiv E.z)

def SimpleGraph.LowSliceCardFirstError.Active {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} {x : ↑(singletonLeft T a)} {y : ↑(singletonRight T b)} {e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y} (E : K.LowSliceCardFirstError S T a b x y e) : Prop

The first-error witness is active when its source vertex is still in the left active color after deleting x.

Equations

• E.Active = (↑E.z ∈ SimpleGraph.singletonLeft T a)

def SimpleGraph.LowSliceCardFirstError.Inactive {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} {x : ↑(singletonLeft T a)} {y : ↑(singletonRight T b)} {e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y} (E : K.LowSliceCardFirstError S T a b x y e) : Prop

The first-error witness is inactive when its source vertex is outside the left active color after deleting x.

Equations

• E.Inactive = (↑E.z ∉ SimpleGraph.singletonLeft T a)

theorem SimpleGraph.LowSliceCardFirstError.imageZ_ne_deleted {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} {x : ↑(singletonLeft T a)} {y : ↑(singletonRight T b)} {e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y} (E : K.LowSliceCardFirstError S T a b x y e) : E.imageZ ≠ ↑y

The localized target vertex is still present in the right card.

theorem SimpleGraph.LowSliceCardFirstError.sourceActive_iff_targetActive {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} {x : ↑(singletonLeft T a)} {y : ↑(singletonRight T b)} {e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y} (E : K.LowSliceCardFirstError S T a b x y e) : ↑E.z ∈ singletonLeft T a ↔ E.imageZ ∈ singletonRight T b

The first-error witness has the same active-color status on the two localized cards.

theorem SimpleGraph.LowSliceCardFirstError.sourceInactive_iff_targetInactive {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} {x : ↑(singletonLeft T a)} {y : ↑(singletonRight T b)} {e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y} (E : K.LowSliceCardFirstError S T a b x y e) : ↑E.z ∉ singletonLeft T a ↔ E.imageZ ∉ singletonRight T b

Equivalently, inactive first-error witnesses also stay inactive.

theorem SimpleGraph.LowSliceCardFirstError.active_or_inactive {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} {x : ↑(singletonLeft T a)} {y : ↑(singletonRight T b)} {e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y} (E : K.LowSliceCardFirstError S T a b x y e) : E.Active ∧ E.imageZ ∈ singletonRight T b ∨ E.Inactive ∧ E.imageZ ∉ singletonRight T b

Every localized first error is either active-active or inactive-inactive.

theorem SimpleGraph.LowSliceCardFirstError.active_or_inactive_source {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} {x : ↑(singletonLeft T a)} {y : ↑(singletonRight T b)} {e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y} (E : K.LowSliceCardFirstError S T a b x y e) : E.Active ∨ E.Inactive

Every localized first error is, in source terms, active or inactive.

def SimpleGraph.LowSliceCardFirstError.sourceActiveVertex {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} {x : ↑(singletonLeft T a)} {y : ↑(singletonRight T b)} {e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y} (E : K.LowSliceCardFirstError S T a b x y e) (hE : E.Active) : ↑(singletonLeft T a)

Recenter an active first-error witness at its source first-error vertex.

Equations

• E.sourceActiveVertex hE = ⟨↑E.z, hE⟩

def SimpleGraph.LowSliceCardFirstError.targetActiveVertex {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} {x : ↑(singletonLeft T a)} {y : ↑(singletonRight T b)} {e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y} (E : K.LowSliceCardFirstError S T a b x y e) (hE : E.Active) : ↑(singletonRight T b)

Recenter an active first-error witness at its target first-error vertex.

Equations

• E.targetActiveVertex hE = ⟨E.imageZ, ⋯⟩

theorem SimpleGraph.LowSliceCardFirstError.sourceFirst_iff_targetFirst {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} {x : ↑(singletonLeft T a)} {y : ↑(singletonRight T b)} {e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y} (E : K.LowSliceCardFirstError S T a b x y e) : ↑E.z ∈ S ↔ E.imageZ ∈ S

The first-error witness has the same passive first-color status on the two localized cards.

def SimpleGraph.LowSliceLocalObstruction {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The local obstruction form: every visible active card match with matching first-color status has a concrete first star error above a common two-hole colored card.

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.LowSliceZeroStarPair.exists_starMismatch_with_twoHole_of_no_pair {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (hno : ¬K.LowSliceZeroStarPair S T a b) (x : ↑(singletonLeft T a)) (y : ↑(singletonRight T b)) (e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y) (hFirst : ↑x ∈ S ↔ ↑y ∈ S) : ∃ (z : { w : V // w ≠ ↑x }), e.StarMismatch z ∧ Nonempty ((K.deleteTwo ↑x ↑z).TwoColorIso (K.deleteTwo ↑y ↑(e.cardIso.iso.toEquiv z)) (deleteTwoColor S ↑x ↑z) (deleteTwoColor (singletonLeft T a) ↑x ↑z) (deleteTwoColor S ↑y ↑(e.cardIso.iso.toEquiv z)) (deleteTwoColor (singletonRight T b) ↑y ↑(e.cardIso.iso.toEquiv z)))

In a no-zero-star-pair obstruction, every active card match localizes to a two-hole card together with a concrete star mismatch over that two-hole base.

theorem SimpleGraph.LowSliceZeroStarPair.cardFirstError_of_no_pair {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (hno : ¬K.LowSliceZeroStarPair S T a b) (x : ↑(singletonLeft T a)) (y : ↑(singletonRight T b)) (e : K.FixedHostCardIsoData S (singletonLeft T a) (singletonRight T b) ↑x ↑y) (hFirst : ↑x ∈ S ↔ ↑y ∈ S) : Nonempty (K.LowSliceCardFirstError S T a b x y e)

In a no-zero-star-pair obstruction, every visible active card match has a packaged first-error witness.

theorem SimpleGraph.LowSliceZeroStarPair.localObstruction_iff_no_pair {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} : K.LowSliceLocalObstruction S T a b ↔ ¬K.LowSliceZeroStarPair S T a b

The absence of an active zero-star pair is equivalent to the local first-error obstruction.

theorem SimpleGraph.LowSliceZeroStarPair.localObstruction_of_no_pair {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (hno : ¬K.LowSliceZeroStarPair S T a b) : K.LowSliceLocalObstruction S T a b

Restatement in the direction used by the proof campaign: if there is no active zero-star pair, then the obstruction can be worked with locally above each active card edge.

theorem SimpleGraph.LowSliceIsoData.firstError_of_no_pair {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (e : K.LowSliceIsoData S T a b) (hno : ¬K.LowSliceZeroStarPair S T a b) (x : ↑(singletonLeft T a)) : Nonempty (K.LowSliceCardFirstError S T a b x (e.toEquiv x) (e.cardIso x))

Under a no-zero-star-pair assumption, every edge of a chosen finite low-slice matching has a packaged first-error witness.

noncomputable def SimpleGraph.LowSliceIsoData.totalStarErrorCount {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (e : K.LowSliceIsoData S T a b) : ℕ

The total deleted-star error of a chosen low-slice matching.

Equations

• e.totalStarErrorCount = ∑ x : ↑(SimpleGraph.singletonLeft T a), (e.cardIso x).starErrorCount

theorem SimpleGraph.LowSliceIsoData.totalStarErrorCount_even {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (e : K.LowSliceIsoData S T a b) : Even e.totalStarErrorCount

The total deleted-star error of any chosen low-slice matching is even.

theorem SimpleGraph.LowSliceIsoData.totalStarErrorCount_eq_zero_iff {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (e : K.LowSliceIsoData S T a b) : e.totalStarErrorCount = 0 ↔ ∀ (x : ↑(singletonLeft T a)), (e.cardIso x).ZeroStarError

Total star error is zero exactly when every matched low-slice card has zero star error.

def SimpleGraph.LowSliceIsoData.toZeroStarMatchingOfTotalErrorZero {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (e : K.LowSliceIsoData S T a b) (hzero : e.totalStarErrorCount = 0) : K.LowSliceZeroStarMatching S T a b

A zero-total-error low-slice matching is a perfect zero-star matching.

Equations

• e.toZeroStarMatchingOfTotalErrorZero hzero = e.toZeroStarMatching ⋯ ⋯

def SimpleGraph.LowSliceIsoData.ofZeroStarMatching {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (m : K.LowSliceZeroStarMatching S T a b) : K.LowSliceIsoData S T a b

Forget the zero-star fields of a perfect zero-star matching, keeping only the underlying chosen low-slice matching.

Equations

• SimpleGraph.LowSliceIsoData.ofZeroStarMatching m = { toEquiv := m.toEquiv, cardIso := m.cardIso }

theorem SimpleGraph.LowSliceIsoData.totalStarErrorCount_ofZeroStarMatching {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (m : K.LowSliceZeroStarMatching S T a b) : (ofZeroStarMatching m).totalStarErrorCount = 0

The low-slice matching underlying a perfect zero-star matching has total star error zero.

def SimpleGraph.LowSliceIsoData.NoZeroStarEdge {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b : V} (e : K.LowSliceIsoData S T a b) : Prop

A chosen low-slice matching has no zero-star edge.

Equations

• e.NoZeroStarEdge = ∀ (x : ↑(SimpleGraph.singletonLeft T a)), ¬(e.cardIso x).ZeroStarError

theorem SimpleGraph.LowSliceIsoData.noZeroStarEdge_iff_forall_pos {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (e : K.LowSliceIsoData S T a b) : e.NoZeroStarEdge ↔ ∀ (x : ↑(singletonLeft T a)), 0 < (e.cardIso x).starErrorCount

No zero-star edge is equivalent to every matched card carrying positive star error.

def SimpleGraph.LowSliceIsoData.IsMinimumStarError {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (e : K.LowSliceIsoData S T a b) : Prop

A chosen low-slice matching has minimum total star error among all chosen low-slice matchings.

Equations

• e.IsMinimumStarError = ∀ (e' : K.LowSliceIsoData S T a b), e.totalStarErrorCount ≤ e'.totalStarErrorCount

structure SimpleGraph.LowSliceMinimumErrorMatching {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) [Finite V] : Type u_1

A minimum-error chosen low-slice matching. This is the formal counterpart of choosing a minimum-error active-card matching in the proof sketch.

• toIsoData : K.LowSliceIsoData S T a b
• minimum : self.toIsoData.IsMinimumStarError

theorem SimpleGraph.LowSliceMinimumErrorMatching.exists_of_sameDeck {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (hlow : K.LowSliceSameDeck S T a b) : Nonempty (K.LowSliceMinimumErrorMatching S T a b)

Low-slice equality admits a minimum-error chosen matching. The proof uses well-ordering of ℕ on the set of total star-error values, not finiteness of the space of card isomorphisms.

structure SimpleGraph.LowSliceMinimumErrorMatching.ActiveFirstError {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (m : K.LowSliceMinimumErrorMatching S T a b) (x : ↑(singletonLeft T a)) : Type u_1

An active first-error witness above one edge of a minimum-error matching.

• error : K.LowSliceCardFirstError S T a b x (m.toIsoData.toEquiv x) (m.toIsoData.cardIso x)
• active : self.error.Active

structure SimpleGraph.LowSliceMinimumErrorMatching.InactiveFirstError {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (m : K.LowSliceMinimumErrorMatching S T a b) (x : ↑(singletonLeft T a)) : Type u_1

An inactive first-error witness above one edge of a minimum-error matching.

• error : K.LowSliceCardFirstError S T a b x (m.toIsoData.toEquiv x) (m.toIsoData.cardIso x)
• inactive : self.error.Inactive

def SimpleGraph.LowSliceMinimumErrorMatching.ActiveFirstError.source {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.ActiveFirstError x) : ↑(singletonLeft T a)

The active source vertex reached by following this first error.

Equations

• E.source = E.error.sourceActiveVertex ⋯

def SimpleGraph.LowSliceMinimumErrorMatching.ActiveFirstError.target {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.ActiveFirstError x) : ↑(singletonRight T b)

The active target vertex reached by following this first error.

Equations

• E.target = E.error.targetActiveVertex ⋯

def SimpleGraph.LowSliceMinimumErrorMatching.ActiveFirstError.nextLeft {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.ActiveFirstError x) : ↑(singletonLeft T a)

The left vertex currently matched to the active target of this first error. This is the successor vertex in the alternating exchange graph.

Equations

• E.nextLeft = m.toIsoData.toEquiv.symm E.target

@[simp]

theorem SimpleGraph.LowSliceMinimumErrorMatching.ActiveFirstError.toEquiv_nextLeft {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.ActiveFirstError x) : m.toIsoData.toEquiv E.nextLeft = E.target

def SimpleGraph.LowSliceMinimumErrorMatching.ActiveFirstError.Coherent {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.ActiveFirstError x) : Prop

A coherent active first error points at the right mate of its own active source. These are the side-cycle cases in the exchange picture.

Equations

• E.Coherent = (E.source = E.nextLeft)

def SimpleGraph.LowSliceMinimumErrorMatching.ActiveFirstError.Noncoherent {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.ActiveFirstError x) : Prop

A noncoherent active first error is a genuine alternating exchange step.

Equations

• E.Noncoherent = (E.source ≠ E.nextLeft)

theorem SimpleGraph.LowSliceMinimumErrorMatching.ActiveFirstError.coherent_or_noncoherent {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.ActiveFirstError x) : E.Coherent ∨ E.Noncoherent

theorem SimpleGraph.LowSliceMinimumErrorMatching.ActiveFirstError.target_eq_toEquiv_source_of_coherent {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.ActiveFirstError x) (h : E.Coherent) : E.target = m.toIsoData.toEquiv E.source

In the coherent case, the active target is exactly the matched mate of the active source.

theorem SimpleGraph.LowSliceMinimumErrorMatching.ActiveFirstError.source_ne_base {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.ActiveFirstError x) : E.source ≠ x

The active first-error source is genuinely different from the deleted base of the card where it was found.

theorem SimpleGraph.LowSliceMinimumErrorMatching.ActiveFirstError.target_ne_baseTarget {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.ActiveFirstError x) : E.target ≠ m.toIsoData.toEquiv x

The active first-error target is genuinely different from the deleted right-hand base of the card where it was found.

theorem SimpleGraph.LowSliceMinimumErrorMatching.ActiveFirstError.nextLeft_ne_base {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.ActiveFirstError x) : E.nextLeft ≠ x

The successor of an active first error is also different from the deleted base where the error was found.

def SimpleGraph.LowSliceMinimumErrorMatching.ActiveFirstError.recenteredTwoHoleIso {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.ActiveFirstError x) : (K.deleteTwo ↑x ↑E.source).TwoColorIso (K.deleteTwo ↑(m.toIsoData.toEquiv x) ↑E.target) (deleteTwoColor S ↑x ↑E.source) (deleteTwoColor (singletonLeft T a) ↑x ↑E.source) (deleteTwoColor S ↑(m.toIsoData.toEquiv x) ↑E.target) (deleteTwoColor (singletonRight T b) ↑(m.toIsoData.toEquiv x) ↑E.target)

Following an active first error carries a concrete two-hole transport from the old edge to the recentered active pair.

Equations

• E.recenteredTwoHoleIso = id E.error.twoHoleIso

theorem SimpleGraph.LowSliceMinimumErrorMatching.ActiveFirstError.adjacency_mismatch {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.ActiveFirstError x) : ¬(K.Adj ↑x ↑E.source ↔ K.Adj ↑(m.toIsoData.toEquiv x) ↑(m.toIsoData.toEquiv E.nextLeft))

The adjacency-mismatch lemma for an active first error: the host adjacency between the deleted base and the active source vertex disagrees with the host adjacency between the matched mate of the base and the matched mate of the observer successor. This holds for both coherent and noncoherent active first errors and is the unified geometric content of the deleted-star error.

def SimpleGraph.LowSliceMinimumErrorMatching.ActiveFirstError.coherentTwoHoleIso {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.ActiveFirstError x) (h : E.Coherent) : (K.deleteTwo ↑x ↑E.source).TwoColorIso (K.deleteTwo ↑(m.toIsoData.toEquiv x) ↑(m.toIsoData.toEquiv E.source)) (deleteTwoColor S ↑x ↑E.source) (deleteTwoColor (singletonLeft T a) ↑x ↑E.source) (deleteTwoColor S ↑(m.toIsoData.toEquiv x) ↑(m.toIsoData.toEquiv E.source)) (deleteTwoColor (singletonRight T b) ↑(m.toIsoData.toEquiv x) ↑(m.toIsoData.toEquiv E.source))

In the coherent case, the recentered two-hole transport deletes a matched active pair on the right.

Equations

• E.coherentTwoHoleIso h = ⋯.mpr E.recenteredTwoHoleIso

def SimpleGraph.LowSliceMinimumErrorMatching.InactiveFirstError.source {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.InactiveFirstError x) : ↑(complementaryDeleteLeft T a b)

The complementary-side source vertex reached by following an inactive first error.

Equations

• E.source = ⟨↑E.error.z, ⋯⟩

def SimpleGraph.LowSliceMinimumErrorMatching.InactiveFirstError.target {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.InactiveFirstError x) : ↑(complementaryDeleteRight T a b)

The complementary-side target vertex reached by following an inactive first error.

Equations

• E.target = ⟨E.error.imageZ, ⋯⟩

def SimpleGraph.LowSliceMinimumErrorMatching.InactiveFirstError.recenteredTwoHoleIso {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.InactiveFirstError x) : (K.deleteTwo ↑x ↑E.source).TwoColorIso (K.deleteTwo ↑(m.toIsoData.toEquiv x) ↑E.target) (deleteTwoColor S ↑x ↑E.source) (deleteTwoColor (singletonLeft T a) ↑x ↑E.source) (deleteTwoColor S ↑(m.toIsoData.toEquiv x) ↑E.target) (deleteTwoColor (singletonRight T b) ↑(m.toIsoData.toEquiv x) ↑E.target)

Following an inactive first error carries a concrete two-hole transport from the old active edge to a complementary-side recentering.

Equations

• E.recenteredTwoHoleIso = id E.error.twoHoleIso

def SimpleGraph.LowSliceMinimumErrorMatching.InactiveFirstError.SourceOutsideCore {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.InactiveFirstError x) : Prop

The inactive source lies in the outside core O.

Equations

• E.SourceOutsideCore = (↑E.source ∉ T ∧ ↑E.source ≠ a ∧ ↑E.source ≠ b)

def SimpleGraph.LowSliceMinimumErrorMatching.InactiveFirstError.SourceAtB {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.InactiveFirstError x) : Prop

The inactive source is the opposite endpoint b.

Equations

• E.SourceAtB = (↑E.source = b)

def SimpleGraph.LowSliceMinimumErrorMatching.InactiveFirstError.TargetOutsideCore {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.InactiveFirstError x) : Prop

The inactive target lies in the outside core O.

Equations

• E.TargetOutsideCore = (↑E.target ∉ T ∧ ↑E.target ≠ a ∧ ↑E.target ≠ b)

def SimpleGraph.LowSliceMinimumErrorMatching.InactiveFirstError.TargetAtA {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.InactiveFirstError x) : Prop

The inactive target is the opposite endpoint a.

Equations

• E.TargetAtA = (↑E.target = a)

theorem SimpleGraph.LowSliceMinimumErrorMatching.InactiveFirstError.source_outside_or_atB {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.InactiveFirstError x) : E.SourceOutsideCore ∨ E.SourceAtB

theorem SimpleGraph.LowSliceMinimumErrorMatching.InactiveFirstError.target_outside_or_atA {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.InactiveFirstError x) : E.TargetOutsideCore ∨ E.TargetAtA

def SimpleGraph.LowSliceMinimumErrorMatching.InactiveFirstError.EndpointExposing {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.InactiveFirstError x) : Prop

An inactive first error exposes one of the opposite endpoints.

Equations

• E.EndpointExposing = (E.SourceAtB ∨ E.TargetAtA)

def SimpleGraph.LowSliceMinimumErrorMatching.InactiveFirstError.OuterResidual {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.InactiveFirstError x) : Prop

An inactive first error stays entirely in the outside core.

Equations

• E.OuterResidual = (E.SourceOutsideCore ∧ E.TargetOutsideCore)

theorem SimpleGraph.LowSliceMinimumErrorMatching.InactiveFirstError.endpointExposing_or_outerResidual {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.InactiveFirstError x) : E.EndpointExposing ∨ E.OuterResidual

theorem SimpleGraph.LowSliceMinimumErrorMatching.InactiveFirstError.outerResidual_not_endpointExposing {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.InactiveFirstError x) (h : E.OuterResidual) : ¬E.EndpointExposing

A purely outer inactive residual does not expose either endpoint.

theorem SimpleGraph.LowSliceMinimumErrorMatching.InactiveFirstError.not_endpointExposing_iff_outerResidual {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {m : K.LowSliceMinimumErrorMatching S T a b} {x : ↑(singletonLeft T a)} (E : m.InactiveFirstError x) : ¬E.EndpointExposing ↔ E.OuterResidual

Inactive first errors not seen at the endpoints are exactly outer residuals.

theorem SimpleGraph.LowSliceMinimumErrorMatching.totalStarErrorCount_eq_zero_of_pair {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (m : K.LowSliceMinimumErrorMatching S T a b) (hpair : K.LowSliceZeroStarPair S T a b) : m.toIsoData.totalStarErrorCount = 0

A minimum-error matching has total error zero whenever an active zero-star pair exists.

theorem SimpleGraph.LowSliceMinimumErrorMatching.totalStarErrorCount_eq_zero_iff_pair {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (m : K.LowSliceMinimumErrorMatching S T a b) : m.toIsoData.totalStarErrorCount = 0 ↔ K.LowSliceZeroStarPair S T a b

For a minimum-error matching, total error zero is equivalent to the active zero-star pair target.

theorem SimpleGraph.LowSliceMinimumErrorMatching.totalStarErrorCount_pos_iff_no_pair {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (m : K.LowSliceMinimumErrorMatching S T a b) : 0 < m.toIsoData.totalStarErrorCount ↔ ¬K.LowSliceZeroStarPair S T a b

For a minimum-error matching, positive total error is exactly the no-pair obstruction.

theorem SimpleGraph.LowSliceMinimumErrorMatching.noZeroStarEdge_iff_no_pair {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (m : K.LowSliceMinimumErrorMatching S T a b) : m.toIsoData.NoZeroStarEdge ↔ ¬K.LowSliceZeroStarPair S T a b

For a minimum-error matching, having no zero-star edge is exactly the local no-pair obstruction.

theorem SimpleGraph.LowSliceMinimumErrorMatching.firstError_of_no_pair {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (m : K.LowSliceMinimumErrorMatching S T a b) (hno : ¬K.LowSliceZeroStarPair S T a b) (x : ↑(singletonLeft T a)) : Nonempty (K.LowSliceCardFirstError S T a b x (m.toIsoData.toEquiv x) (m.toIsoData.cardIso x))

Under the no-pair obstruction, every edge of a minimum-error matching has a packaged first-error witness.

theorem SimpleGraph.LowSliceMinimumErrorMatching.firstError_active_or_inactive_of_no_pair {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (m : K.LowSliceMinimumErrorMatching S T a b) (hno : ¬K.LowSliceZeroStarPair S T a b) (x : ↑(singletonLeft T a)) : Nonempty (m.ActiveFirstError x) ∨ Nonempty (m.InactiveFirstError x)

Every first-error witness above a minimum-error no-pair obstruction is in one of the two color-compatible branches: active-active or inactive-inactive.

def SimpleGraph.LowSliceMinimumErrorZeroConjecture {V : Type u_1} [Finite V] (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The strengthened minimum-error route: every low-slice equality has a minimum-error matching of total star error zero.

Equations

• K.LowSliceMinimumErrorZeroConjecture S T a b = (K.LowSliceSameDeck S T a b → ∃ (m : K.LowSliceMinimumErrorMatching S T a b), m.toIsoData.totalStarErrorCount = 0)

structure SimpleGraph.LowSlicePositiveMinimumObstruction {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b : V) [Finite V] : Type u_1

A fully packaged positive minimum-error obstruction to the current route.

• low : K.LowSliceSameDeck S T a b
• min : K.LowSliceMinimumErrorMatching S T a b
• positive : 0 < self.min.toIsoData.totalStarErrorCount

def SimpleGraph.NoLowSlicePositiveMinimumObstruction {V : Type u_1} [Finite V] (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The exact no-positive-obstruction form of the minimum-error route.

Equations

• K.NoLowSlicePositiveMinimumObstruction S T a b = ¬Nonempty (K.LowSlicePositiveMinimumObstruction S T a b)

theorem SimpleGraph.LowSliceZeroStarPairConjecture.of_minimumErrorZero {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (h : K.LowSliceMinimumErrorZeroConjecture S T a b) : K.LowSliceZeroStarPairConjecture S T a b

The minimum-error-zero route implies the active zero-star-pair conjecture.

theorem SimpleGraph.LowSliceMinimumErrorZeroConjecture.iff_zeroStarPairConjecture {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} : K.LowSliceMinimumErrorZeroConjecture S T a b ↔ K.LowSliceZeroStarPairConjecture S T a b

The minimum-error-zero formulation is equivalent to the active zero-star pair formulation.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.nonempty_iff_not_minimumErrorZero {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} : Nonempty (K.LowSlicePositiveMinimumObstruction S T a b) ↔ ¬K.LowSliceMinimumErrorZeroConjecture S T a b

Failing the minimum-error-zero route is equivalent to exhibiting a positive minimum-error obstruction.

theorem SimpleGraph.NoLowSlicePositiveMinimumObstruction.iff_minimumErrorZero {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} : K.NoLowSlicePositiveMinimumObstruction S T a b ↔ K.LowSliceMinimumErrorZeroConjecture S T a b

Ruling out positive minimum-error obstructions is exactly the minimum-error-zero route.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.no_pair {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) : ¬K.LowSliceZeroStarPair S T a b

A positive minimum-error obstruction has no active zero-star pair.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.totalStarErrorCount_ge_two {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) : 2 ≤ o.min.toIsoData.totalStarErrorCount

The total star error of a positive minimum-error obstruction is at least 2. This follows from the parity lemma: a per-card star error is always even, so the total is even, and a positive even number is at least 2.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.noZeroStarEdge {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) : o.min.toIsoData.NoZeroStarEdge

A positive minimum-error obstruction has no zero-star edge in its chosen minimum matching.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.cardIso_starErrorCount_ge_two {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) (x : ↑(singletonLeft T a)) : 2 ≤ (o.min.toIsoData.cardIso x).starErrorCount

In a positive minimum-error obstruction, every card iso in the chosen matching has star error count at least 2. This is the parity lemma applied edge-wise: each card is forced to have at least one mismatch (no zero-star edges), and the parity lemma forces the count to be even.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.totalStarErrorCount_ge_two_mul_ncard {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) : 2 * (singletonLeft T a).ncard ≤ o.min.toIsoData.totalStarErrorCount

In a positive minimum-error obstruction, the total star error is at least twice the number of singleton-left vertices. This is the parity bound summed over all matched edges.

theorem SimpleGraph.LowSliceMinimumErrorMatching.totalStarErrorCount_zero_or_ge {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (m : K.LowSliceMinimumErrorMatching S T a b) : m.toIsoData.totalStarErrorCount = 0 ∨ 2 * (singletonLeft T a).ncard ≤ m.toIsoData.totalStarErrorCount

Star-error gap for minimum-error matchings: the total star error is either zero or at least 2 * |singletonLeft T a|.

This packages the parity bound at the matching level: a minimum-error matching with strictly positive total error gives a positive obstruction, which by the parity bound has total at least twice the number of left vertices. In particular, a minimum-error matching cannot have total star error equal to 1, 3, 5, ... or any value strictly between 0 and 2|singletonLeft|.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.no_activeFirstError_of_T_empty {V : Type u_1} [Finite V] {K : SimpleGraph V} {S : Set V} {a b : V} (m : K.LowSliceMinimumErrorMatching S ∅ a b) (x : ↑(singletonLeft ∅ a)) (E : m.ActiveFirstError x) : False

With empty T, there is no active first-error witness anywhere. This is because singletonLeft ∅ a = {a}, so the witness vertex z ≠ a cannot be in singletonLeft, contradicting the active condition.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.not_allActiveBranches_of_T_empty {V : Type u_1} [Finite V] {K : SimpleGraph V} {S : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S ∅ a b) : ¬∀ (x : ↑(singletonLeft ∅ a)), Nonempty (o.min.ActiveFirstError x)

With empty T, no positive minimum-error obstruction admits the all-active branch. This rules out one of the five subforks (the all-coherent and noncoherent active cycle forks) in the special case T = ∅.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.firstError_active_or_inactive {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) (x : ↑(singletonLeft T a)) : Nonempty (o.min.ActiveFirstError x) ∨ Nonempty (o.min.InactiveFirstError x)

Every edge of a positive minimum-error obstruction splits into the active or inactive first-error branch.

def SimpleGraph.LowSlicePositiveMinimumObstruction.HasActiveBranch {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) (x : ↑(singletonLeft T a)) : Prop

The active branch is available above the matched edge x.

Equations

• o.HasActiveBranch x = Nonempty (o.min.ActiveFirstError x)

def SimpleGraph.LowSlicePositiveMinimumObstruction.HasInactiveBranch {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) (x : ↑(singletonLeft T a)) : Prop

The inactive branch is available above the matched edge x.

Equations

• o.HasInactiveBranch x = Nonempty (o.min.InactiveFirstError x)

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.hasActive_or_hasInactive {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) (x : ↑(singletonLeft T a)) : o.HasActiveBranch x ∨ o.HasInactiveBranch x

def SimpleGraph.LowSlicePositiveMinimumObstruction.AllActiveBranches {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) : Prop

All matched edges admit an active first-error branch.

Equations

• o.AllActiveBranches = ∀ (x : ↑(SimpleGraph.singletonLeft T a)), o.HasActiveBranch x

def SimpleGraph.LowSlicePositiveMinimumObstruction.AllInactiveBranches {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) : Prop

All matched edges admit an inactive first-error branch.

Equations

• o.AllInactiveBranches = ∀ (x : ↑(SimpleGraph.singletonLeft T a)), o.HasInactiveBranch x

def SimpleGraph.LowSlicePositiveMinimumObstruction.HasMixedBranches {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) : Prop

A positive obstruction has both active and inactive first-error branches somewhere in the chosen minimum matching.

Equations

• o.HasMixedBranches = ((∃ (x : ↑(SimpleGraph.singletonLeft T a)), o.HasActiveBranch x) ∧ ∃ (x : ↑(SimpleGraph.singletonLeft T a)), o.HasInactiveBranch x)

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.exists_inactiveBranch_of_not_allActive {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) (hnot : ¬o.AllActiveBranches) : ∃ (x : ↑(singletonLeft T a)), o.HasInactiveBranch x

If a positive obstruction is not active everywhere, it has an inactive branch somewhere.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.exists_activeBranch_of_not_allInactive {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) (hnot : ¬o.AllInactiveBranches) : ∃ (x : ↑(singletonLeft T a)), o.HasActiveBranch x

If a positive obstruction is not inactive everywhere, it has an active branch somewhere.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.branch_trichotomy {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) : o.AllActiveBranches ∨ o.AllInactiveBranches ∨ o.HasMixedBranches

Every positive minimum-error obstruction is all-active, all-inactive, or genuinely mixed.

structure SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveTransportStep {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) : Type u_1

A packaged active exchange step inside a positive minimum-error obstruction.

• base : ↑(singletonLeft T a)
• witness : o.min.ActiveFirstError self.base

structure SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) : Type u_1

A chosen active first-error witness over every matched edge of a positive minimum-error obstruction.

• witness (x : ↑(singletonLeft T a)) : o.min.ActiveFirstError x

noncomputable def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.ofAllActiveBranches {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (h : o.AllActiveBranches) : o.ActiveObserverSystem

Choose an active observer system from the proposition that every edge has an active branch.

Equations

• SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.ofAllActiveBranches h = { witness := fun (x : ↑(SimpleGraph.singletonLeft T a)) => Classical.choice ⋯ }

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.step {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) (x : ↑(singletonLeft T a)) : o.ActiveTransportStep

The active transport step selected at x.

Equations

• B.step x = { base := x, witness := B.witness x }

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.source {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) (x : ↑(singletonLeft T a)) : ↑(singletonLeft T a)

The defect source selected at x.

Equations

• B.source x = (B.witness x).source

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.next {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) (x : ↑(singletonLeft T a)) : ↑(singletonLeft T a)

The observer successor selected at x.

Equations

• B.next x = (B.witness x).nextLeft

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.observerMap {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) : ↑(singletonLeft T a) → ↑(singletonLeft T a)

The self-map on active vertices obtained by following selected observer successors.

Equations

• B.observerMap x = B.next x

@[simp]

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.observerMap_apply {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) (x : ↑(singletonLeft T a)) : B.observerMap x = B.next x

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.source_ne_self {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) (x : ↑(singletonLeft T a)) : B.source x ≠ x

A selected active source is never the deleted base where it is observed.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.next_ne_self {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) (x : ↑(singletonLeft T a)) : B.next x ≠ x

The selected observer successor is never the same as the deleted base.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.observerMap_ne_self {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) (x : ↑(singletonLeft T a)) : B.observerMap x ≠ x

The selected observer map has no fixed point.

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.CoherentAt {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) (x : ↑(singletonLeft T a)) : Prop

The selected active witness at x is coherent.

Equations

• B.CoherentAt x = (B.witness x).Coherent

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.NoncoherentAt {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) (x : ↑(singletonLeft T a)) : Prop

The selected active witness at x is noncoherent.

Equations

• B.NoncoherentAt x = (B.witness x).Noncoherent

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.coherentAt_or_noncoherentAt {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) (x : ↑(singletonLeft T a)) : B.CoherentAt x ∨ B.NoncoherentAt x

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.source_eq_next_of_coherentAt {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) {x : ↑(singletonLeft T a)} (h : B.CoherentAt x) : B.source x = B.next x

At a coherent selected active witness, the defect source is the observer successor.

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.coherentMatchedTwoHoleIsoAt {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) (x : ↑(singletonLeft T a)) (h : B.CoherentAt x) : (K.deleteTwo ↑x ↑(B.next x)).TwoColorIso (K.deleteTwo ↑(o.min.toIsoData.toEquiv x) ↑(o.min.toIsoData.toEquiv (B.next x))) (deleteTwoColor S ↑x ↑(B.next x)) (deleteTwoColor (singletonLeft T a) ↑x ↑(B.next x)) (deleteTwoColor S ↑(o.min.toIsoData.toEquiv x) ↑(o.min.toIsoData.toEquiv (B.next x))) (deleteTwoColor (singletonRight T b) ↑(o.min.toIsoData.toEquiv x) ↑(o.min.toIsoData.toEquiv (B.next x)))

A coherent selected active witness is a matched two-hole transport from the base to its observer successor.

Equations

• B.coherentMatchedTwoHoleIsoAt x h = id (⋯.mp ((B.witness x).coherentTwoHoleIso h))

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.HasObserverCycle {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) : Prop

A selected observer cycle for an active observer system.

Equations

• B.HasObserverCycle = ∃ (x : ↑(SimpleGraph.singletonLeft T a)) (n : ℕ), 1 < n ∧ B.observerMap^[n] x = x

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.exists_observerCycle {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) : B.HasObserverCycle

Any chosen active observer system has a nontrivial finite observer cycle.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.exists_activeObserverCycle_of_allActiveBranches {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (h : o.AllActiveBranches) : ∃ (B : o.ActiveObserverSystem), B.HasObserverCycle

If every edge of a positive obstruction has an active branch, then one can choose active first errors so as to get a nontrivial observer cycle.

structure SimpleGraph.LowSlicePositiveMinimumObstruction.InactiveObserverSystem {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) : Type u_1

A chosen inactive first-error witness over every matched edge of a positive minimum-error obstruction.

• witness (x : ↑(singletonLeft T a)) : o.min.InactiveFirstError x

noncomputable def SimpleGraph.LowSlicePositiveMinimumObstruction.InactiveObserverSystem.ofAllInactiveBranches {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (h : o.AllInactiveBranches) : o.InactiveObserverSystem

Choose an inactive observer system from the proposition that every edge has an inactive branch.

Equations

• SimpleGraph.LowSlicePositiveMinimumObstruction.InactiveObserverSystem.ofAllInactiveBranches h = { witness := fun (x : ↑(SimpleGraph.singletonLeft T a)) => Classical.choice ⋯ }

def SimpleGraph.LowSlicePositiveMinimumObstruction.InactiveObserverSystem.source {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.InactiveObserverSystem) (x : ↑(singletonLeft T a)) : ↑(complementaryDeleteLeft T a b)

The selected inactive source at x.

Equations

• B.source x = (B.witness x).source

def SimpleGraph.LowSlicePositiveMinimumObstruction.InactiveObserverSystem.target {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.InactiveObserverSystem) (x : ↑(singletonLeft T a)) : ↑(complementaryDeleteRight T a b)

The selected inactive target at x.

Equations

• B.target x = (B.witness x).target

def SimpleGraph.LowSlicePositiveMinimumObstruction.InactiveObserverSystem.EndpointExposingAt {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.InactiveObserverSystem) (x : ↑(singletonLeft T a)) : Prop

The selected inactive witness at x exposes an endpoint.

Equations

• B.EndpointExposingAt x = (B.witness x).EndpointExposing

def SimpleGraph.LowSlicePositiveMinimumObstruction.InactiveObserverSystem.OuterResidualAt {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.InactiveObserverSystem) (x : ↑(singletonLeft T a)) : Prop

The selected inactive witness at x remains in the outside core.

Equations

• B.OuterResidualAt x = (B.witness x).OuterResidual

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.InactiveObserverSystem.endpointExposingAt_or_outerResidualAt {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.InactiveObserverSystem) (x : ↑(singletonLeft T a)) : B.EndpointExposingAt x ∨ B.OuterResidualAt x

def SimpleGraph.LowSlicePositiveMinimumObstruction.InactiveObserverSystem.AllEndpointExposing {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.InactiveObserverSystem) : Prop

Every selected inactive witness exposes an endpoint.

Equations

• B.AllEndpointExposing = ∀ (x : ↑(SimpleGraph.singletonLeft T a)), B.EndpointExposingAt x

def SimpleGraph.LowSlicePositiveMinimumObstruction.InactiveObserverSystem.HasOuterResidual {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.InactiveObserverSystem) : Prop

Some selected inactive witness remains entirely in the outside core.

Equations

• B.HasOuterResidual = ∃ (x : ↑(SimpleGraph.singletonLeft T a)), B.OuterResidualAt x

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.InactiveObserverSystem.allEndpointExposing_or_hasOuterResidual {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.InactiveObserverSystem) : B.AllEndpointExposing ∨ B.HasOuterResidual

A chosen all-inactive system is either endpoint-exposing everywhere or has an explicit outer residual.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.exists_inactiveObserverSystem_of_allInactiveBranches {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (h : o.AllInactiveBranches) : ∃ (B : o.InactiveObserverSystem), B.AllEndpointExposing ∨ B.HasOuterResidual

If every edge of a positive obstruction has an inactive branch, then one can choose inactive first errors and split them into endpoint and outer cases.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.strategy_fork {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) : (∃ (B : o.ActiveObserverSystem), B.HasObserverCycle) ∨ (∃ (B : o.InactiveObserverSystem), B.AllEndpointExposing ∨ B.HasOuterResidual) ∨ o.HasMixedBranches

The current strategic fork for any positive minimum-error obstruction: active observer cycle, all-inactive endpoint/outer split, or mixed branches.

def SimpleGraph.LowSlicePositiveMinimumObstruction.NoActiveObserverCycleFork {V : Type u_1} [Finite V] (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The active-cycle fork is impossible.

Equations

• SimpleGraph.LowSlicePositiveMinimumObstruction.NoActiveObserverCycleFork K S T a b = ∀ (o : K.LowSlicePositiveMinimumObstruction S T a b), ¬∃ (B : o.ActiveObserverSystem), B.HasObserverCycle

def SimpleGraph.LowSlicePositiveMinimumObstruction.NoInactiveEndpointOuterFork {V : Type u_1} [Finite V] (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The all-inactive endpoint/outer fork is impossible.

Equations

• One or more equations did not get rendered due to their size.

def SimpleGraph.LowSlicePositiveMinimumObstruction.NoMixedBranchFork {V : Type u_1} [Finite V] (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The genuinely mixed active/inactive branch fork is impossible.

Equations

• SimpleGraph.LowSlicePositiveMinimumObstruction.NoMixedBranchFork K S T a b = ∀ (o : K.LowSlicePositiveMinimumObstruction S T a b), ¬o.HasMixedBranches

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.NoLowSlicePositiveMinimumObstruction.of_no_strategy_forks {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (hactive : NoActiveObserverCycleFork K S T a b) (hinactive : NoInactiveEndpointOuterFork K S T a b) (hmixed : NoMixedBranchFork K S T a b) : K.NoLowSlicePositiveMinimumObstruction S T a b

Ruling out the three concrete strategy forks rules out every positive minimum-error obstruction.

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveTransportStep.source {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (A : o.ActiveTransportStep) : ↑(singletonLeft T a)

The source of a packaged active exchange step.

Equations

• A.source = A.witness.source

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveTransportStep.target {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (A : o.ActiveTransportStep) : ↑(singletonRight T b)

The target of a packaged active exchange step.

Equations

• A.target = A.witness.target

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveTransportStep.nextBase {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (A : o.ActiveTransportStep) : ↑(singletonLeft T a)

The next base vertex obtained by pulling the target back through the chosen minimum matching.

Equations

• A.nextBase = A.witness.nextLeft

@[simp]

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveTransportStep.toEquiv_nextBase {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (A : o.ActiveTransportStep) : o.min.toIsoData.toEquiv A.nextBase = A.target

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveTransportStep.Coherent {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (A : o.ActiveTransportStep) : Prop

A coherent packaged active step is a side-cycle step.

Equations

• A.Coherent = A.witness.Coherent

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveTransportStep.Noncoherent {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (A : o.ActiveTransportStep) : Prop

A noncoherent packaged active step is a genuine alternating exchange step.

Equations

• A.Noncoherent = A.witness.Noncoherent

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveTransportStep.coherent_or_noncoherent {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (A : o.ActiveTransportStep) : A.Coherent ∨ A.Noncoherent

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveTransportStep.coherent_iff_source_eq_nextBase {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (A : o.ActiveTransportStep) : A.Coherent ↔ A.source = A.nextBase

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveTransportStep.noncoherent_iff_source_ne_nextBase {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (A : o.ActiveTransportStep) : A.Noncoherent ↔ A.source ≠ A.nextBase

A packaged active step is noncoherent exactly when its source and successor are distinct.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveTransportStep.source_ne_base {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (A : o.ActiveTransportStep) : A.source ≠ A.base

The source of an active exchange step is not its base card.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveTransportStep.nextBase_ne_base {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (A : o.ActiveTransportStep) : A.nextBase ≠ A.base

The successor of an active exchange step is not its base card.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveTransportStep.three_distinct_of_noncoherent {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (A : o.ActiveTransportStep) (hA : A.Noncoherent) : A.source ≠ A.base ∧ A.nextBase ≠ A.base ∧ A.source ≠ A.nextBase

A noncoherent active step is a three-distinct-vertex configuration.

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveExchangeRel {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) (u v : ↑(singletonLeft T a)) : Prop

The directed active exchange relation carried by active first-error steps. An edge points from the defect source to the left vertex matched to its target.

Equations

• o.ActiveExchangeRel u v = ∃ (A : o.ActiveTransportStep), A.source = u ∧ A.nextBase = v

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverRel {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) (u v : ↑(singletonLeft T a)) : Prop

The observer-successor relation carried by active first-error steps. This edge points from the deleted base card to the left vertex matched to the first-error target.

Equations

• o.ActiveObserverRel u v = ∃ (A : o.ActiveTransportStep), A.base = u ∧ A.nextBase = v

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveNoncoherentRel {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) (u v : ↑(singletonLeft T a)) : Prop

The noncoherent part of the active exchange relation. These are the candidate descent or correction-cycle edges.

Equations

• o.ActiveNoncoherentRel u v = ∃ (A : o.ActiveTransportStep), A.source = u ∧ A.nextBase = v ∧ A.Noncoherent

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.activeExchangeRel_of_step {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (A : o.ActiveTransportStep) : o.ActiveExchangeRel A.source A.nextBase

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.activeObserverRel_of_step {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (A : o.ActiveTransportStep) : o.ActiveObserverRel A.base A.nextBase

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.activeNoncoherentRel_of_step {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (A : o.ActiveTransportStep) (hA : A.Noncoherent) : o.ActiveNoncoherentRel A.source A.nextBase

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.not_activeNoncoherentRel_self {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) (u : ↑(singletonLeft T a)) : ¬o.ActiveNoncoherentRel u u

The noncoherent active exchange relation has no loops.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.activeNoncoherentRel_ne {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} {u v : ↑(singletonLeft T a)} (h : o.ActiveNoncoherentRel u v) : u ≠ v

Every noncoherent active exchange edge connects distinct active vertices.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.activeNoncoherentRel_of_noncoherentAt {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) (x : ↑(singletonLeft T a)) (h : B.NoncoherentAt x) : o.ActiveNoncoherentRel (B.source x) (B.observerMap x)

A selected noncoherent active witness gives a noncoherent correction edge.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.not_activeObserverRel_self {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) (u : ↑(singletonLeft T a)) : ¬o.ActiveObserverRel u u

Observer-successor active edges also have no loops.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.activeObserverRel_ne {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} {u v : ↑(singletonLeft T a)} (h : o.ActiveObserverRel u v) : u ≠ v

Every observer-successor active edge connects distinct active vertices.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.activeObserverRel_observerMap {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) (x : ↑(singletonLeft T a)) : o.ActiveObserverRel x (B.observerMap x)

A selected active observer system gives an observer edge from every base to its selected successor.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.activeObserverRel_iterate {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) (x : ↑(singletonLeft T a)) (n : ℕ) : o.ActiveObserverRel (B.observerMap^[n] x) (B.observerMap^[n + 1] x)

Consecutive vertices along the selected active observer orbit form observer relation edges.

structure SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (o : K.LowSlicePositiveMinimumObstruction S T a b) : Type u_1

A packaged nontrivial cycle in a selected active observer system.

• system : o.ActiveObserverSystem
• base : ↑(singletonLeft T a)
• period : ℕ
• period_gt_one : 1 < self.period
• closes : self.system.observerMap^[self.period] self.base = self.base

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.CoherentAtIndex {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) (n : ℕ) : Prop

The selected witness at index n of the cycle is coherent.

Equations

• C.CoherentAtIndex n = C.system.CoherentAt (C.system.observerMap^[n] C.base)

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.NoncoherentAtIndex {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) (n : ℕ) : Prop

The selected witness at index n of the cycle is noncoherent.

Equations

• C.NoncoherentAtIndex n = C.system.NoncoherentAt (C.system.observerMap^[n] C.base)

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.coherent_or_noncoherent_at_index {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) (n : ℕ) : C.CoherentAtIndex n ∨ C.NoncoherentAtIndex n

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.AllCoherent {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) : Prop

Every selected witness on the active observer cycle is coherent.

Equations

• C.AllCoherent = ∀ (n : ℕ), C.CoherentAtIndex n

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.HasNoncoherent {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) : Prop

Some selected witness on the active observer cycle is noncoherent.

Equations

• C.HasNoncoherent = ∃ (n : ℕ), C.NoncoherentAtIndex n

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.allCoherent_or_hasNoncoherent {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) : C.AllCoherent ∨ C.HasNoncoherent

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.edge_at {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) (n : ℕ) : o.ActiveObserverRel (C.system.observerMap^[n] C.base) (C.system.observerMap^[n + 1] C.base)

Consecutive vertices on an active observer cycle are observer-relation edges.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.last_edge_to_base {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) : o.ActiveObserverRel (C.system.observerMap^[C.period - 1] C.base) C.base

The last edge of the cycle returns to the base after using the closing equation.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.noncoherentCorrectionEdge_at {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) {n : ℕ} (h : C.NoncoherentAtIndex n) : o.ActiveNoncoherentRel (C.system.source (C.system.observerMap^[n] C.base)) (C.system.observerMap^[n + 1] C.base)

A noncoherent index on the observer cycle gives a noncoherent correction edge from the defect source to the next observer vertex.

def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.coherentMatchedTwoHoleIso_at {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) (hall : C.AllCoherent) (n : ℕ) : (K.deleteTwo ↑(C.system.observerMap^[n] C.base) ↑(C.system.observerMap^[n + 1] C.base)).TwoColorIso (K.deleteTwo ↑(o.min.toIsoData.toEquiv (C.system.observerMap^[n] C.base)) ↑(o.min.toIsoData.toEquiv (C.system.observerMap^[n + 1] C.base))) (deleteTwoColor S ↑(C.system.observerMap^[n] C.base) ↑(C.system.observerMap^[n + 1] C.base)) (deleteTwoColor (singletonLeft T a) ↑(C.system.observerMap^[n] C.base) ↑(C.system.observerMap^[n + 1] C.base)) (deleteTwoColor S ↑(o.min.toIsoData.toEquiv (C.system.observerMap^[n] C.base)) ↑(o.min.toIsoData.toEquiv (C.system.observerMap^[n + 1] C.base))) (deleteTwoColor (singletonRight T b) ↑(o.min.toIsoData.toEquiv (C.system.observerMap^[n] C.base)) ↑(o.min.toIsoData.toEquiv (C.system.observerMap^[n + 1] C.base)))

On an all-coherent active observer cycle, every cycle edge carries a matched two-hole transport between consecutive active vertices and their matched mates.

Equations

• C.coherentMatchedTwoHoleIso_at hall n = ⋯.mpr (C.system.coherentMatchedTwoHoleIsoAt (C.system.observerMap^[n] C.base) ⋯)

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.adjacency_mismatch_at {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) (hall : C.AllCoherent) (n : ℕ) : ¬(K.Adj ↑(C.system.observerMap^[n] C.base) ↑(C.system.observerMap^[n + 1] C.base) ↔ K.Adj ↑(o.min.toIsoData.toEquiv (C.system.observerMap^[n] C.base)) ↑(o.min.toIsoData.toEquiv (C.system.observerMap^[n + 1] C.base)))

On an all-coherent active observer cycle, the host adjacency between two consecutive cycle bases disagrees with the host adjacency between their matched mates under the chosen minimum matching. This is the geometric content of the coherent active first error: the only "missing" adjacency information on each side is exactly the edge between the deleted base and the next cycle vertex, and that information disagrees.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.matching_moves_consecutive_at {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) (hall : C.AllCoherent) (n : ℕ) : ¬(↑(o.min.toIsoData.toEquiv (C.system.observerMap^[n] C.base)) = ↑(C.system.observerMap^[n] C.base) ∧ ↑(o.min.toIsoData.toEquiv (C.system.observerMap^[n + 1] C.base)) = ↑(C.system.observerMap^[n + 1] C.base))

On an all-coherent active observer cycle, the chosen matching cannot fix two consecutive cycle vertices pointwise: at every index, at least one of the two consecutive matched mates is genuinely different from the cycle vertex itself. This is the parity obstruction to the matching being "trivial" on the cycle.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.exists_moved_by_matching {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) (hall : C.AllCoherent) : ∃ (n : ℕ), ↑(o.min.toIsoData.toEquiv (C.system.observerMap^[n] C.base)) ≠ ↑(C.system.observerMap^[n] C.base)

On an all-coherent active observer cycle, the chosen matching moves at least one cycle vertex: there is some index where the matched mate differs from the cycle vertex on the host.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.minimalPeriod_base_pos {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) : 0 < Function.minimalPeriod C.system.observerMap C.base

The base of an active observer cycle has a positive minimal period under the observer map.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.minimalPeriod_base_ne_one {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) : Function.minimalPeriod C.system.observerMap C.base ≠ 1

The base of an active observer cycle has minimal period not equal to one — the observer map has no fixed points.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.minimalPeriod_base_gt_one {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) : 1 < Function.minimalPeriod C.system.observerMap C.base

The base of an active observer cycle has minimal period strictly greater than one — the observer map has no fixed points, so cycles cannot collapse to a single vertex.

noncomputable def SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.toMinimalPeriod {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) : o.ActiveObserverCycle

A minimal-period active observer cycle: redefine the cycle to use the minimal period at the same base. The iterates over [0, period) are then pairwise distinct.

Equations

• C.toMinimalPeriod = { system := C.system, base := C.base, period := Function.minimalPeriod C.system.observerMap C.base, period_gt_one := ⋯, closes := ⋯ }

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.toMinimalPeriod_iterate_injOn {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) {m n : ℕ} (hm : m < C.toMinimalPeriod.period) (hn : n < C.toMinimalPeriod.period) : C.toMinimalPeriod.system.observerMap^[m] C.toMinimalPeriod.base = C.toMinimalPeriod.system.observerMap^[n] C.toMinimalPeriod.base ↔ m = n

Iterates of the observer map below the minimal period are pairwise distinct at the base of the minimal-period cycle.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.minimalPeriod_le_ncard_singletonLeft {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) : Function.minimalPeriod C.system.observerMap C.base ≤ (singletonLeft T a).ncard

The minimal period of an active observer cycle is bounded by the size of singletonLeft T a.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.ncard_singletonLeft_ge_two_of_cycle {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) : 2 ≤ (singletonLeft T a).ncard

The number of singleton-left vertices is at least 2 whenever there is an active observer cycle on a positive minimum-error obstruction. This rules out trivial cases like T = ∅ for the all-active branch.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverSystem.starErrorCount_ge_two {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (B : o.ActiveObserverSystem) (x : ↑(singletonLeft T a)) : 2 ≤ (o.min.toIsoData.cardIso x).starErrorCount

Along any active observer system on a positive minimum-error obstruction, the chosen minimum-error card iso at every base has star error count at least 2.

This combines two facts: (i) the active first-error witness at each base contributes at least one star mismatch; (ii) the parity lemma forces the per-card star error count to be even.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.ActiveObserverCycle.starErrorCount_at_cycle_ge_two {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (C : o.ActiveObserverCycle) (n : ℕ) : 2 ≤ (o.min.toIsoData.cardIso (C.system.observerMap^[n] C.base)).starErrorCount

On an active observer cycle (under the all-active branch), the chosen minimum-error card iso at any cycle base has star error at least 2.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.exists_activeObserverCycleStructure_of_allActiveBranches {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} {o : K.LowSlicePositiveMinimumObstruction S T a b} (h : o.AllActiveBranches) : Nonempty o.ActiveObserverCycle

The all-active branch yields a packaged active observer cycle.

def SimpleGraph.LowSlicePositiveMinimumObstruction.NoAllCoherentActiveCycleFork {V : Type u_1} [Finite V] (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The all-coherent active observer-cycle fork is impossible.

Equations

• SimpleGraph.LowSlicePositiveMinimumObstruction.NoAllCoherentActiveCycleFork K S T a b = ∀ (o : K.LowSlicePositiveMinimumObstruction S T a b) (C : o.ActiveObserverCycle), ¬C.AllCoherent

def SimpleGraph.LowSlicePositiveMinimumObstruction.NoNoncoherentActiveCycleFork {V : Type u_1} [Finite V] (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The active observer-cycle fork with a noncoherent index is impossible.

Equations

• SimpleGraph.LowSlicePositiveMinimumObstruction.NoNoncoherentActiveCycleFork K S T a b = ∀ (o : K.LowSlicePositiveMinimumObstruction S T a b) (C : o.ActiveObserverCycle), ¬C.HasNoncoherent

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.NoActiveObserverCycleFork.of_no_active_cycle_subforks {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (hcoh : NoAllCoherentActiveCycleFork K S T a b) (hnon : NoNoncoherentActiveCycleFork K S T a b) : NoActiveObserverCycleFork K S T a b

Ruling out the all-coherent and noncoherent active cycle subforks rules out the active observer-cycle fork.

def SimpleGraph.LowSlicePositiveMinimumObstruction.NoAllEndpointExposingInactiveFork {V : Type u_1} [Finite V] (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The all-inactive fork where every selected witness exposes an endpoint is impossible.

Equations

• One or more equations did not get rendered due to their size.

def SimpleGraph.LowSlicePositiveMinimumObstruction.NoOuterResidualInactiveFork {V : Type u_1} [Finite V] (K : SimpleGraph V) (S T : Set V) (a b : V) : Prop

The all-inactive fork with an explicit outer residual is impossible.

Equations

• SimpleGraph.LowSlicePositiveMinimumObstruction.NoOuterResidualInactiveFork K S T a b = ∀ (o : K.LowSlicePositiveMinimumObstruction S T a b) (B : o.InactiveObserverSystem), ¬B.HasOuterResidual

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.NoInactiveEndpointOuterFork.of_no_inactive_subforks {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (hend : NoAllEndpointExposingInactiveFork K S T a b) (houter : NoOuterResidualInactiveFork K S T a b) : NoInactiveEndpointOuterFork K S T a b

Ruling out the endpoint-exposing and outer-residual inactive subforks rules out the all-inactive endpoint/outer fork.

theorem SimpleGraph.LowSlicePositiveMinimumObstruction.NoLowSlicePositiveMinimumObstruction.of_no_refined_forks {V : Type u_1} [Finite V] {K : SimpleGraph V} {S T : Set V} {a b : V} (hcoh : NoAllCoherentActiveCycleFork K S T a b) (hnon : NoNoncoherentActiveCycleFork K S T a b) (hend : NoAllEndpointExposingInactiveFork K S T a b) (houter : NoOuterResidualInactiveFork K S T a b) (hmixed : NoMixedBranchFork K S T a b) : K.NoLowSlicePositiveMinimumObstruction S T a b

The refined five-branch reduction for the minimum-error obstruction route.

def SimpleGraph.twoHoleASecondColor {V : Type u_1} (T : Set V) (a t o : V) : Set (deleteTwoVertex t o)

The a-side two-hole second color (T \ {t}) ∪ {a} on K - {t,o}.

Equations

• SimpleGraph.twoHoleASecondColor T a t o = SimpleGraph.deleteTwoColor (SimpleGraph.singletonLeft T a) t o

@[simp]

theorem SimpleGraph.mem_twoHoleASecondColor {V : Type u_1} (T : Set V) (a t o : V) (x : deleteTwoVertex t o) : x ∈ twoHoleASecondColor T a t o ↔ ↑x ∈ T ∨ ↑x = a

def SimpleGraph.twoHoleBSecondColor {V : Type u_1} (T : Set V) (b t o : V) : Set (deleteTwoVertex t o)

The b-side two-hole second color (T \ {t}) ∪ {b} on K - {t,o}.

Equations

• SimpleGraph.twoHoleBSecondColor T b t o = SimpleGraph.deleteTwoColor (SimpleGraph.singletonRight T b) t o

@[simp]

theorem SimpleGraph.mem_twoHoleBSecondColor {V : Type u_1} (T : Set V) (b t o : V) (x : deleteTwoVertex t o) : x ∈ twoHoleBSecondColor T b t o ↔ ↑x ∈ T ∨ ↑x = b

def SimpleGraph.TwoHoleMatch {V : Type u_1} (K : SimpleGraph V) (S T : Set V) (a b t o t' o' : V) : Type u_1

A two-hole match D^a_{t,o} ≅ D^b_{t',o'}.

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.TwoHoleMatch.image_a_mem_right {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b t o t' o' : V} (e : K.TwoHoleMatch S T a b t o t' o') (hat : a ≠ t) (hao : a ≠ o) : ↑(e.iso.toEquiv ⟨a, ⋯⟩) ∈ T ∨ ↑(e.iso.toEquiv ⟨a, ⋯⟩) = b

Under a two-hole match, the image of the moved a-vertex is second-colored on the b-side. This is the Lean version of the first two-hole port bookkeeping statement.

theorem SimpleGraph.TwoHoleMatch.image_second_mem_right {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b t o t' o' : V} (e : K.TwoHoleMatch S T a b t o t' o') (x : deleteTwoVertex t o) (hx : ↑x ∈ T ∨ ↑x = a) : ↑(e.iso.toEquiv x) ∈ T ∨ ↑(e.iso.toEquiv x) = b

Under a two-hole match, the image of any second-colored vertex is second-colored on the b-side.

theorem SimpleGraph.TwoHoleMatch.image_not_second_mem_right {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b t o t' o' : V} (e : K.TwoHoleMatch S T a b t o t' o') (x : deleteTwoVertex t o) (hx : ↑x ∉ T) (hxa : ↑x ≠ a) : ↑(e.iso.toEquiv x) ∉ T ∧ ↑(e.iso.toEquiv x) ≠ b

Under a two-hole match, the image of a non-second-colored vertex is non-second-colored on the b-side.

theorem SimpleGraph.TwoHoleMatch.preimage_b_mem_left {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b t o t' o' : V} (e : K.TwoHoleMatch S T a b t o t' o') (hbt' : b ≠ t') (hbo' : b ≠ o') : ↑(e.iso.symm.toEquiv ⟨b, ⋯⟩) ∈ T ∨ ↑(e.iso.symm.toEquiv ⟨b, ⋯⟩) = a

Under a two-hole match, the preimage of the moved b-vertex is second-colored on the a-side.

theorem SimpleGraph.TwoHoleMatch.image_T_of_maps_a_to_b {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b t o t' o' : V} (e : K.TwoHoleMatch S T a b t o t' o') (hat : a ≠ t) (hao : a ≠ o) (haT : a ∉ T) (hab : ↑(e.iso.toEquiv ⟨a, ⋯⟩) = b) (x : deleteTwoVertex t o) (hxT : ↑x ∈ T) : ↑(e.iso.toEquiv x) ∈ T

If a two-hole match sends the moved a-vertex to the moved b-vertex, then every old T-vertex still maps to an old T-vertex. This is the Lean-facing easy half of "name coherence means side coherence".

theorem SimpleGraph.TwoHoleMatch.image_outside_of_maps_b_to_a {V : Type u_1} {K : SimpleGraph V} {S T : Set V} {a b t o t' o' : V} (e : K.TwoHoleMatch S T a b t o t' o') (hbt : b ≠ t) (hbo : b ≠ o) (hba : ↑(e.iso.toEquiv ⟨b, ⋯⟩) = a) (x : deleteTwoVertex t o) (hxO : ↑x ∈ singletonOutside T a b) : ↑(e.iso.toEquiv x) ∈ singletonOutside T a b

If a two-hole match sends the moved uncolored b-vertex to the moved uncolored a-vertex, then outside vertices stay outside.