Grace/Cumulus/Combinatorics/ParityAlternative.g17

Open in Workbench Download source

Imports

ParitySystems

Declarations

Source

1-- The alternative for parity systems: a system is solvable exactly when no2-- left-kernel vector sees an odd right-hand side, proved by eliminating one3-- column at a time at a pivot row, which preserves obstructions and lifts4-- solutions.5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Combinatorics.ParityAlternative11import ParitySystems1213-- Section: Elimination.1415-- Elimination of the column c at a pivot row p meeting it: the pivot row is16-- added to every other row meeting c, and then the row p and the column c17-- are deleted. The right-hand side follows the rows.18def pivoted (A R C p c : Set) : Set :=19  ((R ∖ {p}) × (C ∖ {c})) ∩ (A △ (cofiber(A, R, c) × fiber(A, C, p)))2021def pivotRows (A R b p c : Set) : Set := { r ∈ cofiber(A, R, c) | p ∈ b }2223def pivotedSide (A R b p c : Set) : Set :=24  (R ∖ {p}) ∩ (b △ pivotRows(A, R, b, p, c))2526theorem pivoted.subset (A R C p c : Set)27  shows pivoted(A, R, C, p, c) ⊆ R × (C ∖ {c})28proof29  intros q hq30  unfold pivoted at hq31  have parts := intersection.membership.forward with hq32  obtain ⟨_, r, hr, x, hx, rfl⟩ := product.membership.forward with parts.left33  have row : r ∈ R := (difference.singleton_membership.forward with hr).left34  exact product.pair with row, hx3536theorem pivotedSide.subset (A R b p c : Set)37  shows pivotedSide(A, R, b, p, c) ⊆ R38proof39  intros r hr40  unfold pivotedSide at hr41  have parts := intersection.membership.forward with hr42  exact (difference.singleton_membership.forward with parts.left).left4344-- The rows of the pivoted matrix, met by a set t of the remaining columns:45-- a row missing c is unchanged, a row meeting c has the pivot row added.46theorem pivoted.row_unchanged (A R C p c r t : Set)47  requires row : r ∈ R48  requires other : r ≠ p49  requires missing : ¬(r, c) ∈ A50  requires inside : t ⊆ C ∖ {c}51  shows fiber(pivoted(A, R, C, p, c), C ∖ {c}, r) ∩ t = fiber(A, C, r) ∩ t52proof53  ext x54  simp [pivoted, fiber.membership, cofiber.membership, intersection.membership,55    difference.singleton_membership, product.pair_membership,56    symmetricDifference.membership]5758theorem pivoted.row_added (A R C p c r t : Set)59  requires row : r ∈ R60  requires other : r ≠ p61  requires meets : (r, c) ∈ A62  requires inside : t ⊆ C ∖ {c}63  shows fiber(pivoted(A, R, C, p, c), C ∖ {c}, r) ∩ t =64    (fiber(A, C, r) ∩ t) △ (fiber(A, C, p) ∩ t)65proof66  ext x67  simp [pivoted, fiber.membership, cofiber.membership, intersection.membership,68    difference.singleton_membership, product.pair_membership,69    symmetricDifference.membership]7071-- The columns, met by a set y of rows: a column missing the pivot row is72-- unchanged off p, a column meeting it has the column c added.73theorem pivoted.column_unchanged (A R C p c x y : Set)74  requires column : x ∈ C ∖ {c}75  requires missing : ¬(p, x) ∈ A76  requires rows : y ⊆ R77  shows cofiber(pivoted(A, R, C, p, c), R, x) ∩ y =78    cofiber(A, R, x) ∩ (y ∖ {p})79proof80  ext r81  simp [pivoted, fiber.membership, cofiber.membership, intersection.membership,82    difference.singleton_membership, product.pair_membership,83    symmetricDifference.membership]8485theorem pivoted.column_added (A R C p c x y : Set)86  requires column : x ∈ C ∖ {c}87  requires meets : (p, x) ∈ A88  requires rows : y ⊆ R89  shows cofiber(pivoted(A, R, C, p, c), R, x) ∩ y =90    (cofiber(A, R, x) ∩ (y ∖ {p})) △ (cofiber(A, R, c) ∩ (y ∖ {p}))91proof92  ext r93  simp [pivoted, fiber.membership, cofiber.membership, intersection.membership,94    difference.singleton_membership, product.pair_membership,95    symmetricDifference.membership]9697-- The pivoted right-hand side: a row r ≠ p is set when b and the correction98-- by the pivot row disagree.99theorem pivotedSide.member (A R b p c r : Set)100  requires row : r ∈ R101  requires other : r ≠ p102  shows r ∈ pivotedSide(A, R, b, p, c) ↔ ¬(r ∈ b ↔ ((r, c) ∈ A ∧ p ∈ b))103proof104  simp [pivotedSide, pivotRows, cofiber.membership, intersection.membership,105    difference.singleton_membership, symmetricDifference.membership]106107theorem pivotedSide.rows_unset (A R b p c y : Set)108  requires rows : y ⊆ R109  requires unset : ¬p ∈ b110  shows y ∩ pivotedSide(A, R, b, p, c) = b ∩ (y ∖ {p})111proof112  ext r113  simp [pivotedSide, pivotRows, cofiber.membership, intersection.membership,114    difference.singleton_membership, symmetricDifference.membership]115116theorem pivotedSide.rows_set (A R b p c y : Set)117  requires rows : y ⊆ R118  requires pivotSet : p ∈ b119  shows y ∩ pivotedSide(A, R, b, p, c) =120    (b ∩ (y ∖ {p})) △ (cofiber(A, R, c) ∩ (y ∖ {p}))121proof122  ext r123  simp [pivotedSide, pivotRows, cofiber.membership, intersection.membership,124    difference.singleton_membership, symmetricDifference.membership]125126-- A solution t of the pivoted system extends to one of the original: the127-- rows other than p are satisfied by t as they were, and c is added to t128-- exactly when the pivot row asks for it.129theorem pivoted.extend (A R C b p c t : Set)130  requires finiteColumns : Finite(C)131  requires column : c ∈ C132  requires pivotRow : p ∈ R133  requires pivot : (p, c) ∈ A134  requires solution :135    Solves(pivoted(A, R, C, p, c), R, C ∖ {c}, pivotedSide(A, R, b, p, c), t)136  shows ∃ s, Solves(A, R, C, b, s)137proof138  have inside := solution.left139  have finiteT : Finite(t) :=140    Finite.subset with (Finite.difference with finiteColumns), inside141  have fresh : ¬c ∈ t142    intro hc143    have bad := inside with c, hc144    simp at bad145  have inPivot : c ∈ fiber(A, C, p) := ⟨column, pivot⟩146  have extend : ∀ X ⊆ {c},147      (EvenSet(fiber(A, C, p) ∩ t) ↔ (c ∈ X ↔ p ∈ b)) →148      Solves(A, R, C, b, t ∪ X)149    intros X part fixed150    constructor151    . simp152    . intros r hr153      rw EvenSet.intersection_union_part with finiteT, part, fresh154      have inRow : c ∈ fiber(A, C, r) ↔ (r, c) ∈ A by simp [column]155      by_cases same : r = p156      . rw same157        tauto158      . have reduced := solution.right with r, hr159        rw pivotedSide.member with hr, same at reduced160        by_cases meets : (r, c) ∈ A161        . have finiteRow : Finite(fiber(A, C, r) ∩ t) :=162            Finite.subset with finiteT, intersection.subset_right163          have finitePivot : Finite(fiber(A, C, p) ∩ t) :=164            Finite.subset with finiteT, intersection.subset_right165          rw [(pivoted.row_added with hr, same, meets, inside),166            (EvenSet.symmetricDifference with finiteRow, finitePivot)]167            at reduced168          tauto169        . rw pivoted.row_unchanged with hr, same, meets, inside at reduced170          tauto171  by_cases fixed : EvenSet(fiber(A, C, p) ∩ t) ↔ ¬p ∈ b172  . witness t ∪ ∅173    have choice : EvenSet(fiber(A, C, p) ∩ t) ↔ (c ∈ ∅ ↔ p ∈ b) by simp174    exact extend with ∅, empty.subset, choice175  . witness t ∪ {c}176    have choice : EvenSet(fiber(A, C, p) ∩ t) ↔ (c ∈ {c} ↔ p ∈ b) by simp177    exact extend with {c}, Subset.reflexive, choice178179-- An obstruction y of the pivoted system lifts to one of the original: the180-- columns other than c are even over y ∖ {p} as they were, and p is added181-- exactly when the column c is odd there.182theorem pivoted.lift (A R C b p c y : Set)183  requires finiteRows : Finite(R)184  requires pivotRow : p ∈ R185  requires pivot : (p, c) ∈ A186  requires obstruction : Obstructs(pivoted(A, R, C, p, c), R, C ∖ {c},187    pivotedSide(A, R, b, p, c), y)188  shows ∃ z, Obstructs(A, R, C, b, z)189proof190  have rows := obstruction.left191  have finiteRest : Finite(y ∖ {p}) :=192    Finite.difference with (Finite.subset with finiteRows, rows)193  have fresh : ¬p ∈ y ∖ {p} by simp194  have finitePivot : Finite(cofiber(A, R, c) ∩ (y ∖ {p})) :=195    Finite.subset with finiteRest, intersection.subset_right196  have inPivot : p ∈ cofiber(A, R, c) := ⟨pivotRow, pivot⟩197  have lift : ∀ Y ⊆ {p},198      (EvenSet(cofiber(A, R, c) ∩ (y ∖ {p})) ↔ ¬p ∈ Y) →199      Obstructs(A, R, C, b, (y ∖ {p}) ∪ Y)200    intros Y part pivotColumn201    refine ⟨?_, ?_, ?_⟩202    . simp203    . intros x hx204      rw EvenSet.intersection_union_part with finiteRest, part, fresh205      have inColumn : p ∈ cofiber(A, R, x) ↔ (p, x) ∈ A by simp [pivotRow]206      by_cases same : x = c207      . rw same208        tauto209      . have column : x ∈ C ∖ {c} by simp [hx, same]210        have reduced := obstruction.right.left with x, column211        by_cases meets : (p, x) ∈ A212        . have finiteColumn : Finite(cofiber(A, R, x) ∩ (y ∖ {p})) :=213            Finite.subset with finiteRest, intersection.subset_right214          rw [(pivoted.column_added with column, meets, rows),215            (EvenSet.symmetricDifference with finiteColumn, finitePivot)]216            at reduced217          tauto218        . rw pivoted.column_unchanged with column, meets, rows at reduced219          tauto220    . have reduced := obstruction.right.right221      have finiteSide : Finite(b ∩ (y ∖ {p})) :=222        Finite.subset with finiteRest, intersection.subset_right223      rw [intersection.commutative,224        (EvenSet.intersection_union_part with finiteRest, part, fresh)]225      by_cases pivotSet : p ∈ b226      . rw [(pivotedSide.rows_set with rows, pivotSet),227          (EvenSet.symmetricDifference with finiteSide, finitePivot)]228          at reduced229        tauto230      . rw pivotedSide.rows_unset with rows, pivotSet at reduced231        tauto232  by_cases evenColumn : EvenSet(cofiber(A, R, c) ∩ (y ∖ {p}))233  . witness (y ∖ {p}) ∪ ∅234    have choice : EvenSet(cofiber(A, R, c) ∩ (y ∖ {p})) ↔ ¬p ∈ ∅ by simp235    exact lift with ∅, empty.subset, choice236  . witness (y ∖ {p}) ∪ {p}237    have choice : EvenSet(cofiber(A, R, c) ∩ (y ∖ {p})) ↔ ¬p ∈ {p} by simp238    exact lift with {p}, Subset.reflexive, choice239240-- Elimination of a column c: the rows of A meeting c are added to a pivot241-- row, and a solution of the reduced system extends by choosing c. A column242-- no row meets is simply dropped.243theorem paritySystem.eliminate (A R C b c : Set)244  requires finiteRows : Finite(R)245  requires finiteColumns : Finite(C)246  requires matrix : A ⊆ R × C247  requires column : c ∈ C248  requires unobstructed : ¬(∃ y, Obstructs(A, R, C, b, y))249  shows ∃ B, ∃ d, B ⊆ R × (C ∖ {c}) ∧ d ⊆ R ∧250    ¬(∃ y, Obstructs(B, R, C ∖ {c}, d, y)) ∧251    (∀ t, Solves(B, R, C ∖ {c}, d, t) → ∃ s, Solves(A, R, C, b, s))252proof253  by_cases pivot : ∃ p ∈ R, (p, c) ∈ A254  . obtain ⟨p, pivotRow, meets⟩ := pivot255    refine ⟨pivoted(A, R, C, p, c), pivotedSide(A, R, b, p, c),256      pivoted.subset, pivotedSide.subset, ?_, ?_⟩257    . intro obstructed258      obtain ⟨y, obstruction⟩ := obstructed259      exact unobstructed260        with (pivoted.lift with finiteRows, pivotRow, meets, obstruction)261    . intros t solution262      exact pivoted.extend263        with finiteColumns, column, pivotRow, meets, solution264  . have noPivot : ∀ r ∈ R, ¬(r, c) ∈ A265      intros r hr hrc266      exact pivot with ⟨r, hr, hrc⟩267    refine ⟨A, b ∩ R, ?_, intersection.subset_right, ?_, ?_⟩268    . -- The column c of A is empty.269      intros q hq270      obtain ⟨_, r, hr, x, hx, rfl⟩ :=271        product.membership.forward with (matrix with q, hq)272      have other : x ≠ c273        intro same274        rw same at hq275        exact noPivot with r, hr, hq276      exact product.pair with hr, (difference.singleton_membership.backward277        with ⟨hx, other⟩)278    . -- An obstruction of the reduced system obstructs A, c being even.279      intro obstructed280      obtain ⟨y, obstruction⟩ := obstructed281      have rows := obstruction.left282      apply unobstructed283      witness y284      refine ⟨rows, ?_, ?_⟩285      . intros x hx286        by_cases same : x = c287        . have none : cofiber(A, R, c) ∩ y = ∅ by ext r; simp [noPivot]288          rw [same, none]289          exact EvenSet.empty290        . have remaining : x ∈ C ∖ {c} by simp [hx, same]291          exact obstruction.right.left with x, remaining292      . have same : y ∩ (b ∩ R) = y ∩ b by ext r; simp293        rw ← same294        exact obstruction.right.right295    . -- A solution of the reduced system solves A.296      intros t solution297      witness t298      have inside := solution.left299      constructor300      . intros x hx301        exact (inside with x, hx).left302      . intros r hr303        have reduced := solution.right with r, hr304        have same : fiber(A, C ∖ {c}, r) ∩ t = fiber(A, C, r) ∩ t by ext x; simp305        rw same at reduced306        rw reduced307        simp [hr]308309-- Section: The alternative.310311-- Eliminating the columns one at a time: an unobstructed system over no312-- columns has the empty solution, since a row r ∈ b would obstruct by313-- itself.314theorem paritySystem.solvable (R C : Set)315  requires finiteRows : Finite(R)316  requires finiteColumns : Finite(C)317  shows ∀ A, ∀ b, A ⊆ R × C → ¬(∃ y, Obstructs(A, R, C, b, y)) →318    ∃ t, Solves(A, R, C, b, t)319proof320  induction finiteColumns with G c321  | empty =>322    intros A b matrix unobstructed323    witness ∅324    constructor325    . simp326    . intros r hr327      have none : fiber(A, ∅, r) ∩ ∅ = ∅ by ext x; simp328      have absent : ¬r ∈ b329        intro hrb330        apply unobstructed331        witness {r}332        refine ⟨singleton.subset_iff.backward with hr, ?_, ?_⟩333        . intros x hx334          simp at hx335        . rw EvenSet.singleton_intersection336          tauto337      rw none338      simp [EvenSet.empty, absent]339  | insert using ih =>340    intros A b matrix unobstructed341    have column : c ∈ G ∪ {c} by simp342    have finiteStep : Finite(G ∪ {c}) :=343      Finite.union with GFinite, Finite.singleton344    obtain ⟨B, d, reducedMatrix, _, reducedUnobstructed, extension⟩ :=345      paritySystem.eliminate346        with finiteRows, finiteStep, matrix, column, unobstructed347    have same : (G ∪ {c}) ∖ {c} = G by ext x; simp [cFresh]348    rw same at reducedMatrix349    rw under same at reducedUnobstructed, extension350    obtain ⟨t, solution⟩ := ih with B, d, reducedMatrix, reducedUnobstructed351    exact extension with t, solution352353theorem paritySystem.alternative (A R C b : Set)354  requires finiteRows : Finite(R)355  requires finiteColumns : Finite(C)356  requires matrix : A ⊆ R × C357  requires side : b ⊆ R358  shows (∃ t, Solves(A, R, C, b, t)) ↔ ¬(∃ y, Obstructs(A, R, C, b, y))359proof360  constructor361  . intros solvable obstructed362    obtain ⟨t, solution⟩ := solvable363    obtain ⟨y, obstruction⟩ := obstructed364    exact Solves.not_obstructed365      with finiteRows, finiteColumns, matrix, solution, obstruction366  . intro unobstructed367    have solvable := paritySystem.solvable with finiteRows, finiteColumns368    exact solvable with A, b, matrix, unobstructed369