Grace/Cumulus/Combinatorics/ParitySystems.g17

Open in Workbench Download source

Imports

Cardinal.Parity · Cardinal.Handshake

Declarations

Source

1-- Linear systems over the two-element field in the language of finite sets:2-- a matrix is a relation between rows and columns, a vector a set of its3-- coordinates, and a row equation asks for the parity of a finite set. A4-- left-kernel vector seeing an odd right-hand side obstructs every solution,5-- by counting a block of the matrix both ways.6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Combinatorics.ParitySystems12import Cardinal.Parity13import Cardinal.Handshake1415-- Section: Systems and solutions.1617-- t solves A t = b: for every row r, the row of A meets t in an odd number of18-- columns exactly when r ∈ b.19predicate Solves (A R C b t : Set) :=20  t ⊆ C ∧ (∀ r ∈ R, (EvenSet(fiber(A, C, r) ∩ t) ↔ ¬r ∈ b))2122-- y obstructs: y A = 0, every column meets y evenly, while y b is odd.23predicate Obstructs (A R C b y : Set) :=24  y ⊆ R ∧ (∀ c ∈ C, EvenSet(cofiber(A, R, c) ∩ y)) ∧ ¬EvenSet(y ∩ b)2526-- Parity of the small sets: a subset of {a} is even exactly when it misses a.27theorem EvenSet.subset_singleton (S a : Set)28  requires inside : S ⊆ {a}29  shows EvenSet(S) ↔ ¬a ∈ S30proof31  have shape := subset_singleton.cases with inside32  rcases shape with rfl | rfl33  . simp [EvenSet.empty]34  . unfold EvenSet35    rw cardinality.singleton36    simp [Even.not_one, singleton.self]3738theorem EvenSet.singleton_intersection (a S : Set)39  shows EvenSet({a} ∩ S) ↔ ¬a ∈ S40proof41  have inside : {a} ∩ S ⊆ {a} := intersection.subset_left42  rw EvenSet.subset_singleton with inside43  simp4445-- Adding to t a part X of {a}, with a outside t, changes the parity of S ∩ t46-- exactly when a lies in both S and X.47theorem EvenSet.intersection_union_part (S t X a : Set)48  requires finiteT : Finite(t)49  requires part : X ⊆ {a}50  requires fresh : ¬a ∈ t51  shows EvenSet(S ∩ (t ∪ X)) ↔ (EvenSet(S ∩ t) ↔ ¬(a ∈ S ∧ a ∈ X))52proof53  have finiteLeft : Finite(S ∩ t) :=54    Finite.subset with finiteT, intersection.subset_right55  have partInside : S ∩ X ⊆ {a}56    intros x hx57    exact part with x, hx.right58  have finiteRight : Finite(S ∩ X) :=59    Finite.subset with Finite.singleton, partInside60  have apart : Disjoint(S ∩ t, S ∩ X)61    apply Disjoint.iff.backward62    intros x hx hx263    have same := singleton.membership.forward with (partInside with x, hx2)64    rw same at hx65    exact fresh with hx.right66  rw [intersection.union2_distrib,67    (EvenSet.union_disjoint with finiteLeft, finiteRight, apart),68    (EvenSet.subset_singleton with partInside)]69  simp7071-- Section: The double count.7273-- The block of A over the rows y and the columns t, A ∩ (y × t), grows by74-- the row a's part {a} × fiber(A, t, a) when a joins y, and by the column75-- a's part cofiber(A, y, a) × {a} when a joins t.76theorem EvenSet.block_add_row (A G t a : Set)77  requires finiteG : Finite(G)78  requires finiteT : Finite(t)79  requires fresh : ¬a ∈ G80  shows EvenSet(A ∩ ((G ∪ {a}) × t)) ↔81    (EvenSet(A ∩ (G × t)) ↔ EvenSet(fiber(A, t, a)))82proof83  have split : A ∩ ((G ∪ {a}) × t) = (A ∩ (G × t)) ∪ ({a} × fiber(A, t, a))84    rw [product.union2_left, intersection.union2_distrib, fiber.row]85  have apartG : Disjoint(G, {a}) by simp [Disjoint.iff, fresh]86  have apart : Disjoint(A ∩ (G × t), {a} × fiber(A, t, a)) :=87    Disjoint.of_subset_left with (product.disjoint_of_left with apartG),88      intersection.subset_right89  have finiteBlock : Finite(A ∩ (G × t)) :=90    Finite.subset with (Finite.product with finiteG, finiteT),91      intersection.subset_right92  have finiteFiber : Finite(fiber(A, t, a)) := fiber.finite with finiteT93  have finiteRow : Finite({a} × fiber(A, t, a)) :=94    Finite.product with Finite.singleton, finiteFiber95  have rowParity : EvenSet({a} × fiber(A, t, a)) ↔ EvenSet(fiber(A, t, a))96    unfold EvenSet97    rw cardinality.singleton_product with finiteFiber98  rw [split, (EvenSet.union_disjoint with finiteBlock, finiteRow, apart),99    rowParity]100101theorem cardinality.product_singleton (A b : Set)102  requires finite : Finite(A)103  shows cardinality(A × {b}) = cardinality(A)104proof105  have finiteProduct := Finite.product with finite, (Finite.singleton at b)106  exact cardinality.bijective with finiteProduct,107    (firstProjection.bijective_singleton at A, b)108109theorem EvenSet.block_add_column (A y G a : Set)110  requires finiteY : Finite(y)111  requires finiteG : Finite(G)112  requires fresh : ¬a ∈ G113  shows EvenSet(A ∩ (y × (G ∪ {a}))) ↔114    (EvenSet(A ∩ (y × G)) ↔ EvenSet(cofiber(A, y, a)))115proof116  have column : A ∩ (y × {a}) = cofiber(A, y, a) × {a}117    ext q118    constructor119    . intro hq120      obtain ⟨_, r, hr, x, hx, rfl⟩ := product.membership.forward with hq.right121      rw singleton.membership.forward with hx at hq122      rw singleton.membership.forward with hx123      exact product.pair with ⟨hr, hq.left⟩, singleton.self124    . intro hq125      obtain ⟨_, r, hr, x, hx, rfl⟩ := product.membership.forward with hq126      rw singleton.membership.forward with hx127      exact ⟨hr.right, (product.pair with hr.left, singleton.self)⟩128  have split : A ∩ (y × (G ∪ {a})) =129      (A ∩ (y × G)) ∪ (cofiber(A, y, a) × {a})130    rw [product.union2_right, intersection.union2_distrib, column]131  have apartG : Disjoint(G, {a}) by simp [Disjoint.iff, fresh]132  have apart : Disjoint(A ∩ (y × G), cofiber(A, y, a) × {a}) :=133    Disjoint.of_subset_left with (product.disjoint_of_right with apartG),134      intersection.subset_right135  have finiteBlock : Finite(A ∩ (y × G)) :=136    Finite.subset with (Finite.product with finiteY, finiteG),137      intersection.subset_right138  have cofiberInside : cofiber(A, y, a) ⊆ y139    intros r hr140    exact hr.left141  have finiteCofiber : Finite(cofiber(A, y, a)) :=142    Finite.subset with finiteY, cofiberInside143  have finiteColumn : Finite(cofiber(A, y, a) × {a}) :=144    Finite.product with finiteCofiber, Finite.singleton145  have columnParity : EvenSet(cofiber(A, y, a) × {a}) ↔146      EvenSet(cofiber(A, y, a))147    unfold EvenSet148    rw cardinality.product_singleton with finiteCofiber149  rw [split, (EvenSet.union_disjoint with finiteBlock, finiteColumn, apart),150    columnParity]151152-- Counted row by row: when t solves the system, row r contributes an odd153-- number exactly when r ∈ b, so the block has the parity of y ∩ b.154theorem Solves.block_parity (A R C b t y : Set)155  requires finiteColumns : Finite(C)156  requires solution : Solves(A, R, C, b, t)157  requires rows : y ⊆ R158  requires finiteY : Finite(y)159  shows EvenSet(A ∩ (y × t)) ↔ EvenSet(y ∩ b)160proof161  have inside := solution.left162  have finiteT : Finite(t) := Finite.subset with finiteColumns, inside163  induction finiteY with G a164  | empty =>165    have blockEmpty : A ∩ (∅ × t) = ∅ by ext q; simp [product.left_empty]166    have rowsEmpty : ∅ ∩ b = ∅ by ext r; simp167    rw [blockEmpty, rowsEmpty]168  | insert using ih =>169    have rowFiber : fiber(A, t, a) = fiber(A, C, a) ∩ t by ext x; simp170    have rowParity : EvenSet(fiber(A, t, a)) ↔ ¬a ∈ b171      rw rowFiber172      exact solution.right with a, aMember173    have rowsParity : EvenSet((G ∪ {a}) ∩ b) ↔ (EvenSet(G ∩ b) ↔ ¬a ∈ b)174      rw [intersection.commutative,175        (EvenSet.intersection_union_part with GFinite, Subset.reflexive,176          aFresh),177        intersection.commutative]178      simp179    rw [(EvenSet.block_add_row with GFinite, finiteT, aFresh), rowParity,180      rowsParity, ih]181182-- Counted column by column: when y obstructs, every column contributes an183-- even number.184theorem Obstructs.block_even (A R C b t y : Set)185  requires finiteRows : Finite(R)186  requires obstruction : Obstructs(A, R, C, b, y)187  requires columns : t ⊆ C188  requires finiteT : Finite(t)189  shows EvenSet(A ∩ (y × t))190proof191  have rows := obstruction.left192  have finiteY : Finite(y) := Finite.subset with finiteRows, rows193  induction finiteT with G a194  | empty =>195    have none : A ∩ (y × ∅) = ∅ by ext q; simp [product.right_empty]196    rw none197    exact EvenSet.empty198  | insert using ih =>199    have columnFiber : cofiber(A, y, a) = cofiber(A, R, a) ∩ y by ext r; simp200    have columnParity : EvenSet(cofiber(A, y, a))201      rw columnFiber202      exact obstruction.right.left with a, aMember203    rw EvenSet.block_add_column with finiteY, GFinite, aFresh204    tauto205206-- Counting the block A ∩ (y × t) both ways: by rows its parity is that of207-- y ∩ b, which is odd; by columns it is even.208theorem Solves.not_obstructed (A R C b t y : Set)209  requires finiteRows : Finite(R)210  requires finiteColumns : Finite(C)211  requires matrix : A ⊆ R × C212  requires solution : Solves(A, R, C, b, t)213  requires obstruction : Obstructs(A, R, C, b, y)214  shows ⊥215proof216  have finiteT : Finite(t) := Finite.subset with finiteColumns, solution.left217  have finiteY : Finite(y) := Finite.subset with finiteRows, obstruction.left218  have byRows := Solves.block_parity219    with finiteColumns, solution, obstruction.left, finiteY220  have byColumns := Obstructs.block_even221    with finiteRows, obstruction, solution.left, finiteT222  exact obstruction.right.right with (byRows.forward with byColumns)223