The odd balancing theorem

This file proves the parity lemma at the heart of the compatibility argument: for a symmetric, row-cancelling interaction b over a finite vertex set, the number of frame assignments with no obstruction at any vertex is odd, and in particular nonzero. The proof counts frame assignments modulo two, expands the count over choices of partner vertices, and cancels the non-covering and derangement contributions in pairs.

@[reducible, inline]

abbrev Sabidussi.OddBalance.F2 : Type

The field with two elements, used for the parity counting argument.

Equations

• Sabidussi.OddBalance.F2 = ZMod 2

theorem Sabidussi.OddBalance.F2.indicator_zero (a : F2) : (if a = 0 then 1 else 0) = 1 + a

theorem Sabidussi.OddBalance.F2.mul_self (a : F2) : a * a = a

theorem Sabidussi.OddBalance.F2.add_self (a : F2) : a + a = 0

def Sabidussi.OddBalance.obstruction {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (x : V → Fin 3) (v : V) : F2

The interaction obstruction at a vertex v: the sum over all other vertices u of the pairwise interaction of the chosen frames at v and u.

Equations

• Sabidussi.OddBalance.obstruction b x v = ∑ u ∈ Finset.univ.erase v, b v u (x v) (x u)

def Sabidussi.OddBalance.solutions {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) : Finset (V → Fin 3)

The set of frame choices for which every vertex obstruction vanishes.

Equations

• Sabidussi.OddBalance.solutions b = {x : V → Fin 3 | ∀ (v : V), Sabidussi.OddBalance.obstruction b x v = 0}

theorem Sabidussi.OddBalance.cast_solutions_card {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) : ↑(solutions b).card = ∑ x : V → Fin 3, ∏ v : V, (1 + obstruction b x v)

theorem Sabidussi.OddBalance.prod_one_add_expand {V : Type u_1} [Fintype V] (q : V → F2) : ∏ v : V, (1 + q v) = ∑ S ∈ Finset.univ.powerset, ∏ v ∈ S, q v

theorem Sabidussi.OddBalance.sum_prod_one_add_expand {V : Type u_1} [Fintype V] [DecidableEq V] (q : (V → Fin 3) → V → F2) : ∑ x : V → Fin 3, ∏ v : V, (1 + q x v) = ∑ S ∈ Finset.univ.powerset, ∑ x : V → Fin 3, ∏ v ∈ S, q x v

theorem Sabidussi.OddBalance.prod_sum_expand {V : Type u_1} [DecidableEq V] (S : Finset V) (t : V → Finset V) (a : V → V → F2) : ∏ v ∈ S, ∑ u ∈ t v, a v u = ∑ f : (v : ↥S) → ↥(t ↑v), ∏ v : ↥S, a ↑v ↑(f v)

@[reducible, inline]

abbrev Sabidussi.OddBalance.Choice {V : Type u_1} (S : Finset V) : Type u_1

A choice, for each vertex of S, of a distinct partner vertex.

Equations

• Sabidussi.OddBalance.Choice S = ((v : ↥S) → { u : V // u ≠ ↑v })

def Sabidussi.OddBalance.choiceTerm {V : Type u_1} (b : V → V → Fin 3 → Fin 3 → F2) (S : Finset V) (f : Choice S) (x : V → Fin 3) : F2

The product over S of the pairwise interactions along a choice of partners.

Equations

• Sabidussi.OddBalance.choiceTerm b S f x = ∏ v : ↥S, b (↑v) (↑(f v)) (x ↑v) (x ↑(f v))

theorem Sabidussi.OddBalance.obstruction_product_expand {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (S : Finset V) (x : V → Fin 3) : ∏ v ∈ S, obstruction b x v = ∑ f : Choice S, choiceTerm b S f x

def Sabidussi.OddBalance.totalChoiceTerm {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (S : Finset V) (f : Choice S) : F2

The sum over all frame assignments of the choice term of a fixed choice of partners.

Equations

• Sabidussi.OddBalance.totalChoiceTerm b S f = ∑ x : V → Fin 3, Sabidussi.OddBalance.choiceTerm b S f x

theorem Sabidussi.OddBalance.sum_obstruction_product_expand {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (S : Finset V) : ∑ x : V → Fin 3, ∏ v ∈ S, obstruction b x v = ∑ f : Choice S, totalChoiceTerm b S f

theorem Sabidussi.OddBalance.sum_fun_split_at {V : Type u_1} [Fintype V] [DecidableEq V] {A : Type u_2} {M : Type u_3} [Fintype A] [AddCommMonoid M] (w : V) (F : (V → A) → M) : ∑ x : V → A, F x = ∑ a : A, ∑ y : { v : V // v ≠ w } → A, F ((Equiv.funSplitAt w A).symm (a, y))

theorem Sabidussi.OddBalance.Fintype.prod_eq_mul_mul_prod_compl_pair {M : Type u_2} [CommMonoid M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (a b : ι) (h : a ≠ b) (g : ι → M) : ∏ i : ι, g i = g a * g b * ∏ i ∈ {a, b}ᶜ, g i

theorem Sabidussi.OddBalance.totalChoiceTerm_eq_zero_of_source_leaf {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (hsymm : ∀ (v u : V) (a c : Fin 3), b v u a c = b u v c a) (hrow : ∀ (v u : V) (a : Fin 3), ∑ c : Fin 3, b v u a c = 0) (S : Finset V) (f : Choice S) (v₀ : ↥S) (w : V) (hw : ↑v₀ = w) (hnotTarget : ∀ (v : ↥S), ↑(f v) ≠ w) : totalChoiceTerm b S f = 0

theorem Sabidussi.OddBalance.totalChoiceTerm_eq_zero_of_target_leaf {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (hrow : ∀ (v u : V) (a : Fin 3), ∑ c : Fin 3, b v u a c = 0) (S : Finset V) (f : Choice S) (v₀ : ↥S) (w : V) (hw : ↑(f v₀) = w) (hnotSource : ∀ (v : V), v ≠ w) (huniqueTarget : ∀ (v : ↥S), ↑(f v) = w → v = v₀) : totalChoiceTerm b S f = 0

theorem Sabidussi.OddBalance.totalChoiceTerm_eq_zero_of_twoCycle {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (hsymm : ∀ (v u : V) (a c : Fin 3), b v u a c = b u v c a) (hrow : ∀ (v u : V) (a : Fin 3), ∑ c : Fin 3, b v u a c = 0) (S : Finset V) (f : Choice S) (v₀ v₁ : ↥S) (hne : v₀ ≠ v₁) (hf₀ : ↑(f v₀) = ↑v₁) (hf₁ : ↑(f v₁) = ↑v₀) (_hu₀ : ∀ (v : ↥S), ↑(f v) = ↑v₀ → v = v₁) (hu₁ : ∀ (v : ↥S), ↑(f v) = ↑v₁ → v = v₀) : totalChoiceTerm b S f = 0

def Sabidussi.OddBalance.Derangement {V : Type u_1} (S : Finset V) : Type u_1

A derangement of the vertices of S: a fixed-point-free permutation.

Equations

• Sabidussi.OddBalance.Derangement S = { σ : Equiv.Perm ↥S // ∀ (v : ↥S), σ v ≠ v }

@[implicit_reducible]

noncomputable instance Sabidussi.OddBalance.Derangement.instFintype {V : Type u_1} [DecidableEq V] (S : Finset V) : Fintype (Derangement S)

Equations

• Sabidussi.OddBalance.Derangement.instFintype S = Fintype.ofInjective (fun (d : Sabidussi.OddBalance.Derangement S) => ⇑↑d) ⋯

def Sabidussi.OddBalance.Derangement.choice {V : Type u_1} {S : Finset V} (d : Derangement S) : Choice S

The choice of partners induced by a derangement: each vertex is sent to its image.

Equations

• d.choice v = ⟨↑(↑d v), ⋯⟩

def Sabidussi.OddBalance.Derangement.inv {V : Type u_1} {S : Finset V} (d : Derangement S) : Derangement S

The inverse derangement.

Equations

• d.inv = ⟨Equiv.symm ↑d, ⋯⟩

theorem Sabidussi.OddBalance.Derangement.inv_inv {V : Type u_1} {S : Finset V} (d : Derangement S) : d.inv.inv = d

theorem Sabidussi.OddBalance.choiceTerm_derangement_inv {V : Type u_1} (b : V → V → Fin 3 → Fin 3 → F2) (hsymm : ∀ (v u : V) (a c : Fin 3), b v u a c = b u v c a) (S : Finset V) (d : Derangement S) (x : V → Fin 3) : choiceTerm b S d.inv.choice x = choiceTerm b S d.choice x

theorem Sabidussi.OddBalance.totalChoiceTerm_derangement_inv {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (hsymm : ∀ (v u : V) (a c : Fin 3), b v u a c = b u v c a) (S : Finset V) (d : Derangement S) : totalChoiceTerm b S d.inv.choice = totalChoiceTerm b S d.choice

theorem Sabidussi.OddBalance.totalChoiceTerm_eq_zero_of_derangement_inv_eq_self {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (hsymm : ∀ (v u : V) (a c : Fin 3), b v u a c = b u v c a) (hrow : ∀ (v u : V) (a : Fin 3), ∑ c : Fin 3, b v u a c = 0) (S : Finset V) (hS : S.Nonempty) (d : Derangement S) (hd : d.inv = d) : totalChoiceTerm b S d.choice = 0

def Sabidussi.OddBalance.CoveredChoice {V : Type u_1} (S : Finset V) : Type u_1

A choice of partners whose image covers every vertex of S.

Equations

• Sabidussi.OddBalance.CoveredChoice S = { f : Sabidussi.OddBalance.Choice S // ∀ (w : ↥S), ∃ (v : ↥S), ↑(f v) = ↑w }

@[implicit_reducible]

noncomputable instance Sabidussi.OddBalance.CoveredChoice.instFintype {V : Type u_1} [Fintype V] [DecidableEq V] (S : Finset V) : Fintype (CoveredChoice S)

Equations

• Sabidussi.OddBalance.CoveredChoice.instFintype S = Fintype.ofInjective (fun (f : Sabidussi.OddBalance.CoveredChoice S) => ↑f) ⋯

noncomputable def Sabidussi.OddBalance.CoveredChoice.toDerangement {V : Type u_1} [Fintype V] {S : Finset V} (c : CoveredChoice S) : Derangement S

A covering choice of partners is a bijection, hence a derangement.

Equations

• c.toDerangement = ⟨Equiv.ofBijective (fun (v : ↥S) => ⟨↑(↑c v), ⋯⟩) ⋯, ⋯⟩

def Sabidussi.OddBalance.Derangement.toCoveredChoice {V : Type u_1} {S : Finset V} (d : Derangement S) : CoveredChoice S

The covering choice of partners underlying a derangement.

Equations

• d.toCoveredChoice = ⟨d.choice, ⋯⟩

theorem Sabidussi.OddBalance.CoveredChoice.toDerangement_choice {V : Type u_1} [Fintype V] {S : Finset V} (c : CoveredChoice S) : c.toDerangement.choice = ↑c

theorem Sabidussi.OddBalance.Derangement.choice_injective {V : Type u_1} {S : Finset V} : Function.Injective fun (d : Derangement S) => d.choice

noncomputable def Sabidussi.OddBalance.coveredChoiceEquivDerangement {V : Type u_1} [Fintype V] (S : Finset V) : CoveredChoice S ≃ Derangement S

Covering choices of partners and derangements are in bijection.

Equations

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

theorem Sabidussi.OddBalance.sum_derangement_totalChoiceTerm_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (hsymm : ∀ (v u : V) (a c : Fin 3), b v u a c = b u v c a) (hrow : ∀ (v u : V) (a : Fin 3), ∑ c : Fin 3, b v u a c = 0) (S : Finset V) (hS : S.Nonempty) : ∑ d : Derangement S, totalChoiceTerm b S d.choice = 0

theorem Sabidussi.OddBalance.sum_coveredChoice_totalChoiceTerm_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (hsymm : ∀ (v u : V) (a c : Fin 3), b v u a c = b u v c a) (hrow : ∀ (v u : V) (a : Fin 3), ∑ c : Fin 3, b v u a c = 0) (S : Finset V) (hS : S.Nonempty) : ∑ c : CoveredChoice S, totalChoiceTerm b S ↑c = 0

theorem Sabidussi.OddBalance.sum_choice_totalChoiceTerm_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (hsymm : ∀ (v u : V) (a c : Fin 3), b v u a c = b u v c a) (hrow : ∀ (v u : V) (a : Fin 3), ∑ c : Fin 3, b v u a c = 0) (S : Finset V) (hS : S.Nonempty) : ∑ f : Choice S, totalChoiceTerm b S f = 0

theorem Sabidussi.OddBalance.sum_obstruction_product_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (hsymm : ∀ (v u : V) (a c : Fin 3), b v u a c = b u v c a) (hrow : ∀ (v u : V) (a : Fin 3), ∑ c : Fin 3, b v u a c = 0) (S : Finset V) (hS : S.Nonempty) : ∑ x : V → Fin 3, ∏ v ∈ S, obstruction b x v = 0

theorem Sabidussi.OddBalance.sum_one_fin3_assignments {V : Type u_1} [Fintype V] [DecidableEq V] : ∑ _x : V → Fin 3, 1 = 1

theorem Sabidussi.OddBalance.cast_solutions_card_eq_one {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (hsymm : ∀ (v u : V) (a c : Fin 3), b v u a c = b u v c a) (hrow : ∀ (v u : V) (a : Fin 3), ∑ c : Fin 3, b v u a c = 0) : ↑(solutions b).card = 1

theorem Sabidussi.OddBalance.solutions_card_odd {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (hsymm : ∀ (v u : V) (a c : Fin 3), b v u a c = b u v c a) (hrow : ∀ (v u : V) (a : Fin 3), ∑ c : Fin 3, b v u a c = 0) : Odd (solutions b).card

theorem Sabidussi.OddBalance.exists_balanced {V : Type u_1} [Fintype V] [DecidableEq V] (b : V → V → Fin 3 → Fin 3 → F2) (hsymm : ∀ (v u : V) (a c : Fin 3), b v u a c = b u v c a) (hrow : ∀ (v u : V) (a : Fin 3), ∑ c : Fin 3, b v u a c = 0) : ∃ (x : V → Fin 3), ∀ (v : V), obstruction b x v = 0

A symmetric row-cancelling interaction has a balanced choice at every vertex.