diff --git a/LeanPool/ClassicalMatchingFactors.lean b/LeanPool/ClassicalMatchingFactors.lean
new file mode 100644
index 000000000..e59ee71c6
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors.lean
@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import LeanPool.ClassicalMatchingFactors.Factors.Tutte
+public import LeanPool.ClassicalMatchingFactors.Matching.Certificates
+public import LeanPool.ClassicalMatchingFactors.Matching.Petersen
+public import LeanPool.ClassicalMatchingFactors.Order.ChainPartitions
+public import LeanPool.ClassicalMatchingFactors.Regular.TwoFactors
+
+/-!
+# Classical matching and factor theorems in finite graphs
+
+Source: doi:10.4153/CJM-1954-033-3, url:https://github.com/jtraverso/tutte-f-factor/tree/dc3bbce463c80c499d3e9fa072d13f9145d907d0
+Authors: Juan Pablo Traverso Gianini
+Status: verified
+Main declarations: `BergeMatching.exists_tutte_berge`, `FFactor.tutte_f_factor`
+Tags: graph-theory, matchings, graph-factors, minimax-theorems, finite-orders
+MSC: 05C70, 05C15, 06A07
+-/
diff --git a/LeanPool/ClassicalMatchingFactors/Bipartite/MatchingCover.lean b/LeanPool/ClassicalMatchingFactors/Bipartite/MatchingCover.lean
new file mode 100644
index 000000000..baa098e51
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Bipartite/MatchingCover.lean
@@ -0,0 +1,238 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Hall
+public import Mathlib.Combinatorics.SimpleGraph.VertexCover
+public import Mathlib.Data.Finset.Max
+public import Mathlib.Data.Finset.Powerset
+public import Mathlib.Tactic.Choose
+public import Mathlib.Tactic.Convert
+public import Mathlib.Tactic.FinCases
+public import Mathlib.Tactic.GCongr
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Push
+public import Mathlib.Tactic.Tauto
+/-!
+
+Imported from [jtraverso/konig-edge-colouring](https://github.com/jtraverso/konig-edge-colouring/blob/7c60f7efb69c1747aaf39e5dfa7a89d907cd84ef/Konig/Egervary.lean), registered as PALOMAR-2026-10-15-000019. The original proof is retained; module paths and imports are adapted for this collection.
+
+# The Kőnig–Egerváry theorem
+
+* `card_matching_le_card_vertexCover`: in every finite graph, a matching has at most as many edges
+  as a vertex cover has vertices (each matching edge needs its own cover vertex).
+* `exists_matching_card_eq_vertexCover`: **Kőnig–Egerváry (1931).** In a finite bipartite graph
+  there are a matching and a vertex cover of the same size; hence the maximum size of a matching
+  equals the minimum size of a vertex cover.
+-/
+
+@[expose] public section
+
+open SimpleGraph
+
+namespace Konig.Egervary
+
+/-- **Weak duality.** A matching has at most as many edges as a vertex cover has vertices. -/
+theorem card_matching_le_card_vertexCover {V : Type*} [Finite V] {G : SimpleGraph V}
+    {M : G.Subgraph} (hM : M.IsMatching) {C : Set V} (hC : G.IsVertexCover C) :
+    M.edgeSet.ncard ≤ C.ncard := by
+  classical
+  rcases isEmpty_or_nonempty V with hV | hV
+  · have : M.edgeSet = ∅ := Set.eq_empty_of_forall_notMem fun e => by
+      induction e using Sym2.ind with
+      | _ a b => exact isEmptyElim a
+    simp [this]
+  have hex : ∀ e ∈ M.edgeSet, ∃ v ∈ C, v ∈ e := by
+    intro e he
+    induction e using Sym2.ind with
+    | _ a b =>
+      rw [Subgraph.mem_edgeSet] at he
+      rcases hC (M.adj_sub he) with h | h
+      · exact ⟨a, h, Sym2.mem_mk_left a b⟩
+      · exact ⟨b, h, Sym2.mem_mk_right a b⟩
+  choose! f hfC hfe using hex
+  refine Set.ncard_le_ncard_of_injOn f hfC ?_ (Set.toFinite C)
+  intro e₁ he₁ e₂ he₂ heq
+  obtain ⟨w₁, h₁⟩ := Sym2.mem_iff_exists.1 (hfe e₁ he₁)
+  obtain ⟨w₂, h₂⟩ := Sym2.mem_iff_exists.1 (hfe e₂ he₂)
+  have ha₁ : M.Adj (f e₁) w₁ := by rw [← Subgraph.mem_edgeSet, ← h₁]; exact he₁
+  have ha₂ : M.Adj (f e₁) w₂ := by rw [heq, ← Subgraph.mem_edgeSet, ← h₂]; exact he₂
+  rw [h₁, h₂, ← heq, hM.eq_of_adj_left ha₁ ha₂]
+
+/-- **Kőnig–Egerváry (1931).** A finite bipartite graph has a matching and a vertex cover of the
+same size. -/
+theorem exists_matching_card_eq_vertexCover {V : Type*} [Finite V] (G : SimpleGraph V)
+    (h : G.Colorable 2) :
+    ∃ (M : G.Subgraph) (C : Set V), M.IsMatching ∧ G.IsVertexCover C ∧
+      M.edgeSet.ncard = C.ncard := by
+  classical
+  have := Fintype.ofFinite V
+  obtain ⟨col⟩ := h
+  have hcol : ∀ a b, G.Adj a b → (col a = 0 ↔ col b ≠ 0) := by
+    intro a b hab
+    have key : ∀ i j : Fin 2, i ≠ j → (i = 0 ↔ j ≠ 0) := by decide
+    exact key _ _ (col.valid hab)
+  set L : Finset V := Finset.univ.filter (fun x => col x = 0) with hL
+  set N : Finset V → Finset V :=
+    fun S => Finset.univ.filter (fun y => ∃ x ∈ S, G.Adj x y) with hN
+  have hNR : ∀ S ⊆ L, ∀ y ∈ N S, y ∉ L := by
+    intro S hS y hy hyL
+    simp only [hN, Finset.mem_filter, Finset.mem_univ, true_and] at hy
+    obtain ⟨x, hx, hxy⟩ := hy
+    have hx0 : col x = 0 := (Finset.mem_filter.1 (hS hx)).2
+    have hy0 : col y = 0 := (Finset.mem_filter.1 hyL).2
+    exact ((hcol x y hxy).1 hx0) hy0
+  obtain ⟨S₀, hS₀L, hmax⟩ := Finset.exists_max_image L.powerset
+    (fun S => (S.card : ℤ) - (N S).card) ⟨∅, Finset.empty_mem_powerset L⟩
+  rw [Finset.mem_powerset] at hS₀L
+  have hmax' : ∀ T ⊆ L, (T.card : ℤ) - (N T).card ≤ (S₀.card : ℤ) - (N S₀).card :=
+    fun T hT => hmax T (Finset.mem_powerset.2 hT)
+  have hNS₀ : (N S₀).card ≤ S₀.card := by
+    have := hmax' ∅ (Finset.empty_subset _)
+    have hN0 : N ∅ = ∅ := by simp [hN]
+    rw [hN0] at this
+    simp at this
+    omega
+  set d := S₀.card - (N S₀).card with hd
+  let t : L → Finset (V ⊕ Fin d) :=
+    fun x => (Finset.univ.filter (fun y => G.Adj x y)).disjSum Finset.univ
+  have hall : ∀ s : Finset L, s.card ≤ (s.biUnion t).card := by
+    intro s
+    rcases s.eq_empty_or_nonempty with rfl | ⟨x₀, hx₀⟩
+    · simp
+    set T : Finset V := s.map (Function.Embedding.subtype _) with hT
+    have hTL : T ⊆ L := by
+      intro x hx
+      rw [hT, Finset.mem_map] at hx
+      obtain ⟨x', -, rfl⟩ := hx
+      exact x'.2
+    have h1 := hmax' T hTL
+    have hTc : T.card = s.card := Finset.card_map _
+    have h2 : (N T).disjSum (Finset.univ : Finset (Fin d)) ⊆ s.biUnion t := by
+      intro z hz
+      rw [Finset.mem_biUnion]
+      rcases z with y | i
+      · rw [Finset.inl_mem_disjSum] at hz
+        simp only [hN, Finset.mem_filter, Finset.mem_univ, true_and] at hz
+        obtain ⟨x, hx, hxy⟩ := hz
+        rw [hT, Finset.mem_map] at hx
+        obtain ⟨x', hx', rfl⟩ := hx
+        exact ⟨x', hx', by simpa [t] using hxy⟩
+      · exact ⟨x₀, hx₀, by simp [t]⟩
+    have := Finset.card_le_card h2
+    rw [Finset.card_disjSum, Finset.card_univ, Fintype.card_fin] at this
+    omega
+  obtain ⟨f, hfinj, hft⟩ := (Finset.all_card_le_biUnion_card_iff_exists_injective t).1 hall
+  set g : V → V := fun x => if h : x ∈ L then Sum.elim id (fun _ => x) (f ⟨x, h⟩) else x with hg
+  set L' : Finset V := L.filter (fun x => ∀ h : x ∈ L, ∃ y, f ⟨x, h⟩ = Sum.inl y) with hL'
+  have hL'L : ∀ {x}, x ∈ L' → x ∈ L := fun hx => (Finset.mem_filter.1 hx).1
+  have hgf : ∀ x (hx : x ∈ L'), f ⟨x, hL'L hx⟩ = Sum.inl (g x) := by
+    intro x hx
+    obtain ⟨y, hy⟩ := (Finset.mem_filter.1 hx).2 (hL'L hx)
+    simp [hg, hL'L hx, hy]
+  have hgadj : ∀ x ∈ L', G.Adj x (g x) := by
+    intro x hx
+    have := hft ⟨x, hL'L hx⟩
+    rw [hgf x hx] at this
+    simpa [t] using this
+  have hgR : ∀ x ∈ L', g x ∉ L := by
+    intro x hx hgx
+    have hx0 : col x = 0 := (Finset.mem_filter.1 (hL'L hx)).2
+    exact (hcol x (g x) (hgadj x hx)).1 hx0 (Finset.mem_filter.1 hgx).2
+  have hginj : ∀ x ∈ L', ∀ y ∈ L', g x = g y → x = y := by
+    intro x hx y hy hxy
+    have := hfinj ((hgf x hx).trans ((congrArg Sum.inl hxy).trans (hgf y hy).symm))
+    exact congrArg Subtype.val this
+  have hL'card : L.card - d ≤ L'.card := by
+    have h1 : (L \ L').card ≤ d := by
+      have := Finset.card_le_card_of_injOn
+        (fun x => if h : x ∈ L then f ⟨x, h⟩ else Sum.inl x)
+        (s := L \ L') (t := (Finset.univ : Finset (Fin d)).image Sum.inr) (by
+          intro a ha
+          rw [Finset.mem_coe, Finset.mem_sdiff] at ha
+          have haL := ha.1
+          simp only [hL', Finset.mem_filter, not_and, not_forall, not_exists] at ha
+          obtain ⟨_, hne⟩ := ha.2 haL
+          simp only [haL, dite_true, Finset.coe_image, Finset.coe_univ, Set.image_univ,
+            Set.mem_range]
+          rcases hfa : f ⟨a, haL⟩ with y | i
+          · exact absurd hfa (hne y)
+          · exact ⟨i, rfl⟩) (by
+          intro a ha b hb hab
+          have haL := (Finset.mem_sdiff.1 ha).1
+          have hbL := (Finset.mem_sdiff.1 hb).1
+          simp only [haL, hbL, dite_true] at hab
+          exact congrArg Subtype.val (hfinj hab))
+      rw [Finset.card_image_of_injective _ Sum.inr_injective, Finset.card_univ,
+        Fintype.card_fin] at this
+      exact this
+    have h2 : (L \ L').card = L.card - L'.card :=
+      Finset.card_sdiff_of_subset (Finset.filter_subset _ _)
+    have h3 : L'.card ≤ L.card := Finset.card_le_card (Finset.filter_subset _ _)
+    omega
+  let M : G.Subgraph :=
+    { verts := (L' : Set V) ∪ (L'.image g : Set V)
+      Adj := fun v w => (v ∈ L' ∧ g v = w) ∨ (w ∈ L' ∧ g w = v)
+      adj_sub := by
+        rintro v w (⟨hv, rfl⟩ | ⟨hw, rfl⟩)
+        · exact hgadj v hv
+        · exact (hgadj w hw).symm
+      edge_vert := by
+        rintro v w (⟨hv, rfl⟩ | ⟨hw, rfl⟩)
+        · exact Or.inl hv
+        · exact Or.inr (by simpa using ⟨w, hw, rfl⟩)
+      symm := ⟨fun _ _ h => h.symm⟩ }
+  have hM : M.IsMatching := by
+    intro v hv
+    rcases hv with hv | hv
+    · refine ⟨g v, Or.inl ⟨hv, rfl⟩, ?_⟩
+      rintro w (⟨-, rfl⟩ | ⟨hw, rfl⟩)
+      · rfl
+      · exact absurd (hL'L hv) (hgR w hw)
+    · obtain ⟨u, hu, rfl⟩ : ∃ u ∈ L', g u = v := by simpa using hv
+      refine ⟨u, Or.inr ⟨hu, rfl⟩, ?_⟩
+      rintro w (⟨hgu, -⟩ | ⟨hw, hwu⟩)
+      · exact absurd (hL'L hgu) (hgR u hu)
+      · exact hginj w hw u hu hwu
+  have hMcard : L'.card ≤ M.edgeSet.ncard := by
+    rw [← Set.ncard_coe_finset]
+    refine Set.ncard_le_ncard_of_injOn (fun x => s(x, g x)) ?_ ?_ (Set.toFinite _)
+    · intro x hx
+      exact (Subgraph.mem_edgeSet (G' := M)).2 (Or.inl ⟨hx, rfl⟩)
+    · intro x hx y hy hxy
+      rcases Sym2.eq_iff.1 hxy with ⟨h1, -⟩ | ⟨h1, -⟩
+      · exact h1
+      · exact absurd (h1 ▸ hL'L hx) (hgR y hy)
+  set C : Finset V := (L \ S₀) ∪ N S₀ with hC
+  have hcov1 : ∀ v w, G.Adj v w → col v = 0 → v ∈ C ∨ w ∈ C := by
+    intro v w hvw hv
+    by_cases hvS : v ∈ S₀
+    · right
+      refine Finset.mem_union_right _ ?_
+      simp only [hN, Finset.mem_filter, Finset.mem_univ, true_and]
+      exact ⟨v, hvS, hvw⟩
+    · left
+      exact Finset.mem_union_left _ (Finset.mem_sdiff.2 ⟨by simp [hL, hv], hvS⟩)
+  have hCcov : G.IsVertexCover (C : Set V) := by
+    intro v w hvw
+    by_cases hv : col v = 0
+    · exact hcov1 v w hvw hv
+    · have hw : col w = 0 := by
+        by_contra hw
+        exact hv ((hcol v w hvw).2 hw)
+      exact (hcov1 w v hvw.symm hw).symm
+  have hCcard : C.card = L.card - S₀.card + (N S₀).card := by
+    rw [hC, Finset.card_union_of_disjoint, Finset.card_sdiff_of_subset hS₀L]
+    rw [Finset.disjoint_left]
+    intro y hy hyN
+    exact hNR S₀ hS₀L y hyN (Finset.mem_sdiff.1 hy).1
+  have hS₀c : S₀.card ≤ L.card := Finset.card_le_card hS₀L
+  refine ⟨M, C, hM, hCcov, le_antisymm (card_matching_le_card_vertexCover hM hCcov) ?_⟩
+  rw [Set.ncard_coe_finset, hCcard]
+  omega
+
+end Konig.Egervary
diff --git a/LeanPool/ClassicalMatchingFactors/Factors/Comp.lean b/LeanPool/ClassicalMatchingFactors/Factors/Comp.lean
new file mode 100644
index 000000000..46018e06e
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Factors/Comp.lean
@@ -0,0 +1,255 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Tutte
+public import Mathlib.Data.Finset.Max
+public import Mathlib.Data.Finset.Powerset
+public import Mathlib.Tactic.Choose
+public import Mathlib.Tactic.Convert
+public import Mathlib.Tactic.FinCases
+public import Mathlib.Tactic.GCongr
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Push
+public import Mathlib.Tactic.Tauto
+/-!
+
+Imported from [jtraverso/tutte-f-factor](https://github.com/jtraverso/tutte-f-factor/blob/dc3bbce463c80c499d3e9fa072d13f9145d907d0/FFactorLib/FFactorComp.lean), registered as PALOMAR-2026-10-18-000005. The original proof is retained; module paths and imports are adapted for this collection.
+
+# Auxiliary results on connected components for the f-factor theorem
+
+* `FFactor.oddComponents_ncard_eq_of_label`: counting odd components via a labelling whose
+  fibres are exactly the components.
+* `FFactor.ncard_oddComponents_deleteVerts_le`: removing a vertex `x` from a vertex set `U`
+  whose neighbours outside `U` meet at most two components of `G - U` decreases the number of
+  odd components by at most one.
+-/
+
+@[expose] public section
+
+open Finset SimpleGraph
+
+namespace FFactor
+
+section Label
+
+variable {X L : Type*} (H : SimpleGraph X) (φ : X → L)
+
+theorem label_eq_of_reachable (h1 : ∀ x y, H.Adj x y → φ x = φ y) {x y : X}
+    (h : H.Reachable x y) : φ x = φ y := by
+  obtain ⟨p⟩ := h
+  induction p with
+  | nil => rfl
+  | cons ha _ ih => exact (h1 _ _ ha).trans ih
+
+open Classical in
+theorem oddComponents_ncard_eq_of_label [Fintype X]
+    (h1 : ∀ x y, H.Adj x y → φ x = φ y) (h2 : ∀ x y, φ x = φ y → H.Reachable x y) :
+    H.oddComponents.ncard = #{l ∈ univ.image φ | Odd #{x | φ x = l}} := by
+  let ψ : H.ConnectedComponent → L :=
+    ConnectedComponent.lift φ (fun v w p _ => label_eq_of_reachable H φ h1 ⟨p⟩)
+  have hψ : ∀ x, ψ (H.connectedComponentMk x) = φ x := fun x => rfl
+  have hinj : Function.Injective ψ := by
+    intro c d hcd
+    induction c using ConnectedComponent.ind with | h x => ?_
+    induction d using ConnectedComponent.ind with | h y => ?_
+    exact ConnectedComponent.sound (h2 x y hcd)
+  have hsupp : ∀ c : H.ConnectedComponent, c.supp = {x | φ x = ψ c} := by
+    intro c
+    induction c using ConnectedComponent.ind with | h y => ?_
+    ext x
+    simp only [ConnectedComponent.mem_supp_iff, Set.mem_ofPred_eq, hψ]
+    constructor
+    · intro h; rw [← hψ, ← hψ, h]
+    · intro h; exact ConnectedComponent.sound (h2 x y h)
+  have key : ∀ l, ({x | φ x = l} : Set X).ncard = #{x | φ x = l} := fun l => by
+    rw [← Set.ncard_coe_finset]; simp
+  rw [← Set.ncard_image_of_injective _ hinj, ← Set.ncard_coe_finset]
+  congr 1
+  ext l
+  simp only [Set.mem_image, Set.mem_ofPred_eq, coe_filter, mem_image, mem_univ, true_and]
+  constructor
+  · rintro ⟨c, hc, rfl⟩
+    induction c using ConnectedComponent.ind with | h y => ?_
+    refine ⟨⟨y, rfl⟩, ?_⟩
+    rw [hsupp, key] at hc
+    exact hc
+  · rintro ⟨⟨y, rfl⟩, hodd⟩
+    refine ⟨H.connectedComponentMk y, ?_, rfl⟩
+    show Odd (H.connectedComponentMk y).supp.ncard
+    rw [hsupp, key]
+    exact hodd
+
+end Label
+
+section Removal
+
+variable {W : Type*} (Γ : SimpleGraph W)
+
+/-- The graph `Γ - U`, as in Mathlib's definition of a Tutte violator. -/
+abbrev del (U : Set W) : SimpleGraph ((⊤ : Γ.Subgraph).deleteVerts U).verts :=
+  ((⊤ : Γ.Subgraph).deleteVerts U).coe
+
+theorem mem_del_verts {U : Set W} {a : W} :
+    a ∈ ((⊤ : Γ.Subgraph).deleteVerts U).verts ↔ a ∉ U := by simp
+
+theorem del_adj {U : Set W} {a b : ((⊤ : Γ.Subgraph).deleteVerts U).verts} :
+    (del Γ U).Adj a b ↔ Γ.Adj a b := by
+  constructor
+  · intro h; exact Subgraph.coe_adj_sub _ _ _ h
+  · intro h; exact Subgraph.deleteVerts_adj.mpr ⟨trivial, a.2.2, trivial, b.2.2, h⟩
+
+/-- The inclusion `Γ - U → Γ - (U \ {x})`. -/
+def delIncl (U : Set W) (x : W) : del Γ U →g del Γ (U \ {x}) where
+  toFun a := ⟨a.1, ⟨trivial, fun h => a.2.2 h.1⟩⟩
+  map_rel' h := (del_adj Γ (U := U \ {x})).mpr ((del_adj Γ (U := U)).mp h)
+
+theorem delIncl_injective (U : Set W) (x : W) : Function.Injective (delIncl Γ U x) := by
+  intro a b h
+  have h' := congrArg Subtype.val h
+  exact Subtype.ext h'
+
+theorem ncard_oddComponents_del_le [Finite W] (U : Set W) (x : W) (hx : x ∈ U)
+    (h3 : ∀ a b c : ((⊤ : Γ.Subgraph).deleteVerts U).verts, Γ.Adj x a → Γ.Adj x b →
+      Γ.Adj x c → (del Γ U).Reachable a b ∨ (del Γ U).Reachable a c ∨
+        (del Γ U).Reachable b c) :
+    (del Γ U).oddComponents.ncard ≤ (del Γ (U \ {x})).oddComponents.ncard + 1 := by
+  classical
+  set H := del Γ U
+  set H' := del Γ (U \ {x})
+  let ι := delIncl Γ U x
+  let A : Set H.ConnectedComponent :=
+    {c | ∃ a : ((⊤ : Γ.Subgraph).deleteVerts U).verts, c = H.connectedComponentMk a ∧ Γ.Adj x a}
+  let B : Set H.ConnectedComponent := {c | c ∉ A ∧ Odd c.supp.ncard}
+  -- `A` has at most two elements
+  have hA : A.ncard ≤ 2 := by
+    by_contra hcon
+    push Not at hcon
+    obtain ⟨c1, c2, c3, h1, h2, h3', h12, h13, h23⟩ :=
+      (Set.two_lt_ncard_iff (Set.toFinite _)).mp hcon
+    obtain ⟨a1, rfl, ha1⟩ := h1
+    obtain ⟨a2, rfl, ha2⟩ := h2
+    obtain ⟨a3, rfl, ha3⟩ := h3'
+    rcases h3 a1 a2 a3 ha1 ha2 ha3 with h | h | h
+    · exact h12 (ConnectedComponent.sound h)
+    · exact h13 (ConnectedComponent.sound h)
+    · exact h23 (ConnectedComponent.sound h)
+  have hsub : H.oddComponents ⊆ B ∪ A := by
+    intro c hc
+    by_cases hcA : c ∈ A
+    · exact Or.inr hcA
+    · exact Or.inl ⟨hcA, hc⟩
+  have hodd1 : H.oddComponents.ncard ≤ B.ncard + 2 :=
+    (Set.ncard_le_ncard hsub).trans ((Set.ncard_union_le _ _).trans (by omega))
+  -- the label on `H'`
+  let ψ : ((⊤ : Γ.Subgraph).deleteVerts (U \ {x})).verts → Option H.ConnectedComponent :=
+    fun y => if h : y.1 ∉ U then
+      (if H.connectedComponentMk ⟨y.1, by simpa using h⟩ ∈ A then none
+        else some (H.connectedComponentMk ⟨y.1, by simpa using h⟩)) else none
+  have hψι : ∀ a, H.connectedComponentMk a ∉ A → ψ (ι a) = some (H.connectedComponentMk a) := by
+    intro a ha
+    have h' : (a : W) ∉ U := a.2.2
+    have e : ψ (ι a) = if H.connectedComponentMk a ∈ A then none
+        else some (H.connectedComponentMk a) := dite_eq_left h'
+    rw [e, ite_eq_right ha]
+  have hψ1 : ∀ y z, H'.Adj y z → ψ y = ψ z := by
+    have key : ∀ y z : ((⊤ : Γ.Subgraph).deleteVerts (U \ {x})).verts, H'.Adj y z →
+        (y : W) ∈ U → ψ y = ψ z := by
+      intro y z hyz hy
+      have hyx : (y : W) = x := by have := y.2; simp_all
+      have hy' : ψ y = none := by simp [ψ, hy]
+      rw [hy']
+      by_cases hz : (z : W) ∈ U
+      · simp [ψ, hz]
+      · have hmem : H.connectedComponentMk ⟨z.1, by simpa using hz⟩ ∈ A :=
+          ⟨⟨z.1, by simpa using hz⟩, rfl, hyx ▸ (del_adj Γ (U := U \ {x})).mp hyz⟩
+        simp [ψ, hz, hmem]
+    intro y z hyz
+    by_cases hy : (y : W) ∈ U
+    · exact key y z hyz hy
+    by_cases hz : (z : W) ∈ U
+    · exact (key z y hyz.symm hz).symm
+    have hc : H.connectedComponentMk ⟨y.1, by simpa using hy⟩ =
+        H.connectedComponentMk ⟨z.1, by simpa using hz⟩ :=
+      ConnectedComponent.connectedComponentMk_eq_of_adj
+        ((del_adj Γ (U := U)).mpr ((del_adj Γ (U := U \ {x})).mp hyz))
+    simp only [ψ, hy, hz, not_false_eq_true, dite_true, hc]
+  have hBle : B.ncard ≤ H'.oddComponents.ncard := by
+    apply Set.ncard_le_ncard_of_injOn (fun c => c.map ι)
+    · intro c hc
+      obtain ⟨hcA, hcodd⟩ := hc
+      induction c using ConnectedComponent.ind with | h a => ?_
+      change Odd (H'.connectedComponentMk (ι a)).supp.ncard
+      have hsupp : (H'.connectedComponentMk (ι a)).supp = ι '' (H.connectedComponentMk a).supp := by
+        ext z
+        simp only [ConnectedComponent.mem_supp_iff, Set.mem_image]
+        constructor
+        · intro hz
+          have hzψ : ψ z = some (H.connectedComponentMk a) := by
+            rw [← hψι a hcA]
+            exact label_eq_of_reachable H' ψ hψ1 (ConnectedComponent.exact hz)
+          have hzU : (z : W) ∉ U := by
+            intro h; simp [ψ, h] at hzψ
+          refine ⟨⟨z.1, by simpa using hzU⟩, ?_, rfl⟩
+          simp only [ψ, hzU, not_false_eq_true, dite_true] at hzψ
+          split_ifs at hzψ
+          exact Option.some_injective _ hzψ
+        · rintro ⟨b, hb, rfl⟩
+          rw [← ConnectedComponent.map_mk, ← ConnectedComponent.map_mk, hb]
+      rw [hsupp, Set.ncard_image_of_injective _ (delIncl_injective Γ U x)]
+      exact hcodd
+    · intro c hc d hd hcd
+      induction c using ConnectedComponent.ind with | h a => ?_
+      induction d using ConnectedComponent.ind with | h b => ?_
+      have hr : H'.Reachable (ι a) (ι b) := by
+        apply ConnectedComponent.exact
+        exact hcd
+      have := label_eq_of_reachable H' ψ hψ1 hr
+      rw [hψι a hc.1, hψι b hd.1] at this
+      exact Option.some_injective _ this
+  -- parity
+  have hcard : Nat.card ((⊤ : Γ.Subgraph).deleteVerts (U \ {x})).verts =
+      Nat.card ((⊤ : Γ.Subgraph).deleteVerts U).verts + 1 := by
+    simp only [Nat.card_coe_set_eq, Subgraph.deleteVerts_verts, Subgraph.verts_top]
+    rw [show Set.univ \ (U \ {x}) = insert x (Set.univ \ U) by
+      ext y; by_cases hy : y = x <;> simp [hy, hx]]
+    rw [Set.ncard_insert_of_notMem (by simp [hx])]
+  have hp1 := (odd_ncard_oddComponents H)
+  have hp2 := (odd_ncard_oddComponents H')
+  rw [hcard] at hp2
+  simp only [Nat.odd_iff] at hp1 hp2
+  have hpar : H'.oddComponents.ncard % 2 ≠ H.oddComponents.ncard % 2 := by
+    omega
+  omega
+
+/-- The neighbours of `x` outside `U` meet at most two components of `Γ - U`. -/
+def TwoComp (U : Set W) (x : W) : Prop :=
+  ∀ a b c : ((⊤ : Γ.Subgraph).deleteVerts U).verts, Γ.Adj x a → Γ.Adj x b →
+      Γ.Adj x c → (del Γ U).Reachable a b ∨ (del Γ U).Reachable a c ∨
+        (del Γ U).Reachable b c
+
+/-- There is a Tutte violator none of whose vertices satisfies `TwoComp`. -/
+theorem exists_min_violator [Finite W] (h : ∃ U, Γ.IsTutteViolator U) :
+    ∃ U, Γ.IsTutteViolator U ∧ ∀ x ∈ U, ¬ TwoComp Γ U x := by
+  classical
+  have hex : ∃ n, ∃ U, U.ncard = n ∧ Γ.IsTutteViolator U := by
+    obtain ⟨U, hU⟩ := h; exact ⟨_, U, rfl, hU⟩
+  obtain ⟨U, hUn, hU⟩ := Nat.find_spec hex
+  refine ⟨U, hU, fun x hx htwo => ?_⟩
+  have hle := ncard_oddComponents_del_le Γ U x hx htwo
+  have hcard : (U \ {x}).ncard + 1 = U.ncard := Set.ncard_sdiff_singleton_add_one hx
+  have hviol : Γ.IsTutteViolator (U \ {x}) := by
+    unfold IsTutteViolator at hU ⊢
+    change U.ncard < (del Γ U).oddComponents.ncard at hU
+    change (U \ {x}).ncard < (del Γ (U \ {x})).oddComponents.ncard
+    omega
+  have := Nat.find_min' hex ⟨U \ {x}, rfl, hviol⟩
+  omega
+
+end Removal
+
+end FFactor
diff --git a/LeanPool/ClassicalMatchingFactors/Factors/Count.lean b/LeanPool/ClassicalMatchingFactors/Factors/Count.lean
new file mode 100644
index 000000000..667d30f63
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Factors/Count.lean
@@ -0,0 +1,459 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Tutte
+public import Mathlib.Data.Finset.Max
+public import Mathlib.Data.Finset.Powerset
+public import Mathlib.Tactic.Choose
+public import Mathlib.Tactic.Convert
+public import Mathlib.Tactic.FinCases
+public import Mathlib.Tactic.GCongr
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Push
+public import Mathlib.Tactic.Tauto
+public import LeanPool.ClassicalMatchingFactors.Factors.Defs
+public import LeanPool.ClassicalMatchingFactors.Factors.Suff
+
+/-!
+
+Imported from [jtraverso/tutte-f-factor](https://github.com/jtraverso/tutte-f-factor/blob/dc3bbce463c80c499d3e9fa072d13f9145d907d0/FFactorLib/FFactorCount.lean), registered as PALOMAR-2026-10-18-000005. The original proof is retained; module paths and imports are adapted for this collection.
+
+# Counting the odd components of the gadget minus a normalised Tutte violator
+-/
+
+@[expose] public section
+
+open Finset SimpleGraph
+
+namespace FFactor
+
+variable {V : Type*} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {f : V → ℕ}
+  {U : Set (GV G f)}
+
+open Classical in
+/-- Filters along equivalent predicates (with arbitrary decidability instances) have the same
+cardinality. -/
+theorem card_filter_congr' {α : Type*} [Fintype α] (p q : α → Prop) [DecidablePred p]
+    [DecidablePred q] (h : ∀ a, p a ↔ q a) : #{a | p a} = #{a | q a} := by
+  apply card_bij (fun a _ => a) <;> simp [h]
+
+open Classical in
+/-- Cardinality of a filter over a sum type. -/
+theorem card_filter_sum_type {α β : Type*} [Fintype α] [Fintype β] (P : α ⊕ β → Prop)
+    [DecidablePred P] :
+    #{x | P x} = #{a | P (.inl a)} + #{b | P (.inr b)} := by
+  simp only [card_filter, Fintype.sum_sum_type]
+
+omit [DecidableEq V] in
+open Classical in
+/-- Cardinality of a filter over the vertices of `gadget - U`. -/
+theorem card_filter_verts (P : GV G f → Prop) [DecidablePred P]
+    [DecidablePred (fun x : ((⊤ : (gadget G f).Subgraph).deleteVerts U).verts => P x.1)] :
+    #{x : ((⊤ : (gadget G f).Subgraph).deleteVerts U).verts | P x.1} = #{a | a ∉ U ∧ P a} := by
+  apply card_bij (fun x _ => x.1)
+  · intro x hx
+    simp only [mem_filter, mem_univ, true_and] at hx ⊢
+    exact ⟨(mem_del_verts _).mp x.2, hx⟩
+  · intro x _ y _ h; exact Subtype.ext h
+  · intro a ha
+    simp only [mem_filter, mem_univ, true_and] at ha
+    exact ⟨⟨a, (mem_del_verts _).mpr ha.1⟩, by simpa using ha.2, rfl⟩
+
+open Classical in
+theorem card_inner_fiber (r : V) :
+    #{p : Σ v : V, Fin (G.degree v - f v) | p.1 = r} = G.degree r - f r := by
+  have : #(univ : Finset (Fin (G.degree r - f r))) =
+      #{p : Σ v : V, Fin (G.degree v - f v) | p.1 = r} := by
+    apply card_bij (fun (i : Fin (G.degree r - f r)) _ =>
+      (⟨r, i⟩ : Σ v : V, Fin (G.degree v - f v)))
+    · intro i _; simp
+    · intro i _ j _ h; exact eq_of_heq (Sigma.mk.inj h).2
+    · rintro ⟨r', j⟩ h
+      simp only [mem_filter, mem_univ, true_and] at h
+      subst h
+      exact ⟨j, mem_univ _, rfl⟩
+  rw [← this, card_univ, Fintype.card_fin]
+
+open Classical in
+theorem card_dart_snd_fst (r : V) (T : Finset V) :
+    #{d : G.Dart | d.fst ∈ T ∧ d.snd = r} = #{t ∈ T | G.Adj r t} := by
+  apply card_bij (fun d _ => d.fst)
+  · intro d hd
+    simp only [mem_filter, mem_univ, true_and] at hd ⊢
+    exact ⟨hd.1, hd.2 ▸ d.adj.symm⟩
+  · intro d _ d' _ h
+    simp only [mem_filter, mem_univ, true_and] at *
+    exact Dart.ext _ _ (Prod.ext h (by simp_all))
+  · intro t ht
+    simp only [mem_filter] at ht
+    exact ⟨⟨(t, r), ht.2.symm⟩, by simp [ht.1], rfl⟩
+
+open Classical in
+theorem card_home_fiber {r : V} (hr : r ∉ Tset G f U) :
+    #{a : GV G f | home G f U a = r} =
+      G.degree r + #{t ∈ Tset G f U | G.Adj r t} + (G.degree r - f r) := by
+  rw [card_filter_sum_type]
+  have e1 : #{b : Σ v : V, Fin (G.degree v - f v) | home G f U (.inr b) = r} =
+      G.degree r - f r := by
+    rw [← card_inner_fiber r]; congr 1
+  have e2 : #{d : G.Dart | home G f U (.inl d) = r} =
+      G.degree r + #{t ∈ Tset G f U | G.Adj r t} := by
+    rw [← card_dart_snd_fst r (Tset G f U), ← G.dart_fst_fiber_card_eq_degree r,
+      ← card_union_of_disjoint]
+    · congr 1
+      ext d
+      simp only [mem_filter, mem_univ, true_and, mem_union]
+      rw [home_inl]
+      split_ifs with h
+      · constructor
+        · intro h'; exact Or.inr ⟨h, h'⟩
+        · rintro (h' | h')
+          · exact absurd (h' ▸ h) hr
+          · exact h'.2
+      · constructor
+        · intro h'; exact Or.inl h'
+        · rintro (h' | h')
+          · exact h'
+          · exact absurd h'.1 h
+    · rw [Finset.disjoint_left]
+      intro d h1 h2
+      simp only [mem_filter, mem_univ, true_and] at h1 h2
+      exact hr (h1 ▸ h2.1)
+  rw [e1, e2]
+
+open Classical in
+theorem notMem_U_of_home {hmin : ∀ x ∈ U, ¬ TwoComp (gadget G f) U x} {a : GV G f}
+    (ha : home G f U a ∉ Sset G f U ∪ Tset G f U) : a ∉ U := by
+  have hT := notMem_T_of_notMem_union ha
+  have hS := notMem_S_of_notMem_union ha
+  rcases a with d | ⟨r, i⟩
+  · rw [home_inl] at hT hS
+    by_cases h : d.fst ∈ Tset G f U
+    · exact F2 hmin h rfl
+    · rw [ite_eq_right h] at hT hS
+      exact F3 hmin hT hS rfl
+  · exact F1 hmin hT i
+
+open Classical in
+theorem odd_fiber_iff (hmin : ∀ x ∈ U, ¬ TwoComp (gadget G f) U x)
+    (hf : ∀ v, f v ≤ G.degree v) (c : (Gr G f U).ConnectedComponent) :
+    Odd #{x : ((⊤ : (gadget G f).Subgraph).deleteVerts U).verts | lab G f U x.1 = .inl c} ↔
+    Odd (∑ w ∈ univ.filter (fun w : ↥(((Sset G f U ∪ Tset G f U : Finset V) : Set V)ᶜ) =>
+        (G.induce ((Sset G f U ∪ Tset G f U : Finset V) : Set V)ᶜ).connectedComponentMk w = c),
+      (f w + #{t ∈ Tset G f U | G.Adj w t})) := by
+  rw [card_filter_verts (U := U) (fun a => lab G f U a = .inl c)]
+  obtain ⟨Cs, hCs⟩ : ∃ Cs : Finset V, Cs = (univ.filter
+      (fun w : ↥(((Sset G f U ∪ Tset G f U : Finset V) : Set V)ᶜ) =>
+      (Gr G f U).connectedComponentMk w = c)).map (Function.Embedding.subtype _) := ⟨_, rfl⟩
+  have hmem : ∀ r, r ∈ Cs ↔ ∃ h : r ∉ Sset G f U ∪ Tset G f U,
+      (Gr G f U).connectedComponentMk ⟨r, h⟩ = c := by
+    intro r
+    simp only [hCs, mem_map, mem_filter, mem_univ, true_and, Function.Embedding.coe_subtype]
+    constructor
+    · rintro ⟨w, hw, rfl⟩; exact ⟨w.2, hw⟩
+    · rintro ⟨h, hc⟩; exact ⟨⟨r, h⟩, hc, rfl⟩
+  have hset : ∀ a, (a ∉ U ∧ lab G f U a = .inl c) ↔ home G f U a ∈ Cs := by
+    intro a
+    rw [hmem]
+    constructor
+    · rintro ⟨haU, hlab⟩
+      by_cases hh : home G f U a ∈ Sset G f U ∪ Tset G f U
+      · exfalso
+        rcases a with d | p
+        · rw [lab_inl_of_mem hh] at hlab; simp at hlab
+        · rw [lab_inr_of_mem hh] at hlab; simp at hlab
+      · rw [lab_of_notMem hh] at hlab
+        exact ⟨hh, Sum.inl_injective hlab⟩
+    · rintro ⟨hh, hc⟩
+      refine ⟨notMem_U_of_home (hmin := hmin) hh, ?_⟩
+      rw [lab_of_notMem hh, hc]
+  rw [card_filter_congr' _ _ hset, card_eq_sum_card_fiberwise (f := home G f U) (t := Cs)
+    (fun a ha => by simpa using ha)]
+  have hterm : ∀ r ∈ Cs, #{a ∈ ({a | home G f U a ∈ Cs} : Finset (GV G f)) | home G f U a = r} =
+      G.degree r + #{t ∈ Tset G f U | G.Adj r t} + (G.degree r - f r) := by
+    intro r hr
+    obtain ⟨h, -⟩ := (hmem r).mp hr
+    rw [← card_home_fiber (notMem_T_of_notMem_union h), filter_filter]
+    congr 1
+    ext a
+    simp only [mem_filter, mem_univ, true_and]
+    constructor
+    · exact fun h => h.2
+    · intro h'; exact ⟨h' ▸ hr, h'⟩
+  rw [sum_congr rfl hterm]
+  have hsum : ∑ r ∈ Cs, (G.degree r + #{t ∈ Tset G f U | G.Adj r t} + (G.degree r - f r)) =
+      ∑ w ∈ univ.filter (fun w : ↥(((Sset G f U ∪ Tset G f U : Finset V) : Set V)ᶜ) =>
+        (Gr G f U).connectedComponentMk w = c),
+      (G.degree w + #{t ∈ Tset G f U | G.Adj w t} + (G.degree w - f w)) := by
+    rw [hCs, sum_map]; rfl
+  rw [hsum]
+  have hsplit : ∀ w : ↥(((Sset G f U ∪ Tset G f U : Finset V) : Set V)ᶜ),
+      G.degree w + #{t ∈ Tset G f U | G.Adj w t} + (G.degree w - f w) =
+      (f w + #{t ∈ Tset G f U | G.Adj w t}) + 2 * (G.degree w - f w) := by
+    intro w; have := hf w; omega
+  rw [sum_congr rfl (fun w _ => hsplit w), sum_add_distrib, ← mul_sum]
+  have key : ∀ A B : ℕ, Odd (A + 2 * B) ↔ Odd A := fun A B => by
+    simp only [Nat.odd_iff]; omega
+  exact key _ _
+
+open Classical in
+theorem card_fiber_TT (hmin : ∀ x ∈ U, ¬ TwoComp (gadget G f) U x) {d : G.Dart}
+    (hd : (.inl d : GV G f) ∉ U) (h1 : d.fst ∈ Tset G f U) (h2 : d.snd ∈ Tset G f U) :
+    #{x : ((⊤ : (gadget G f).Subgraph).deleteVerts U).verts |
+      lab G f U x.1 = .inr (.inl d.edge)} = 2 := by
+  have hmemd : home G f U (.inl d) ∈ Sset G f U ∪ Tset G f U := by
+    simp [h1, h2]
+  have hds : (.inl d.symm : GV G f) ∉ U := F2 hmin h2 (d := d.symm) rfl
+  have hmemds : home G f U (.inl d.symm) ∈ Sset G f U ∪ Tset G f U := by
+    simp [h1, h2]
+  rw [card_filter_verts (U := U) (fun a => lab G f U a = .inr (.inl d.edge))]
+  rw [card_filter_congr' _ (fun a => a ∈ ({.inl d, .inl d.symm} : Finset (GV G f)))]
+  · rw [filter_univ_mem, card_pair]
+    intro h
+    exact d.symm_ne (Sum.inl_injective h).symm
+  · intro a
+    simp only [mem_insert, mem_singleton]
+    constructor
+    · rintro ⟨haU, hlab⟩
+      rcases a with d' | q
+      · by_cases hh : home G f U (.inl d') ∈ Sset G f U ∪ Tset G f U
+        · rw [lab_inl_of_mem hh] at hlab
+          simp only [Sum.inr.injEq, Sum.inl.injEq] at hlab
+          rcases (dart_edge_eq_iff _ _).mp hlab with h | h
+          · exact Or.inl (by rw [h])
+          · exact Or.inr (by rw [h])
+        · rw [lab_of_notMem hh] at hlab; simp at hlab
+      · by_cases hh : home G f U (.inr q) ∈ Sset G f U ∪ Tset G f U
+        · rw [lab_inr_of_mem hh] at hlab; simp at hlab
+        · rw [lab_of_notMem hh] at hlab; simp at hlab
+    · rintro (rfl | rfl)
+      · exact ⟨hd, lab_inl_of_mem hmemd⟩
+      · exact ⟨hds, by rw [lab_inl_of_mem hmemds, Dart.edge_symm]⟩
+
+open Classical in
+theorem ncard_odd_le (hmin : ∀ x ∈ U, ¬ TwoComp (gadget G f) U x)
+    (hf : ∀ v, f v ≤ G.degree v) :
+    (del (gadget G f) U).oddComponents.ncard ≤ oddCount G f (Sset G f U) (Tset G f U) +
+      #{d : G.Dart | d.fst ∈ Tset G f U ∧ d.snd ∈ Sset G f U} +
+      #{p : Σ v : V, Fin (G.degree v - f v) | p.1 ∈ Sset G f U} := by
+  let φ : ((⊤ : (gadget G f).Subgraph).deleteVerts U).verts →
+      (Gr G f U).ConnectedComponent ⊕ (Sym2 V ⊕ GV G f) := fun x => lab G f U x.1
+  rw [oddComponents_ncard_eq_of_label (del (gadget G f) U) φ
+    (fun x y h => lab_eq_of_adj _ _ ((mem_del_verts _).mp x.2) ((mem_del_verts _).mp y.2)
+      ((del_adj _).mp h))
+    (fun x y h => reach_of_lab_eq hmin x.1 y.1 ((mem_del_verts _).mp x.2)
+      ((mem_del_verts _).mp y.2) h)]
+  let A := (univ.filter (fun c : (Gr G f U).ConnectedComponent =>
+    Odd #{x | φ x = .inl c})).image
+    (fun c => (.inl c : (Gr G f U).ConnectedComponent ⊕ (Sym2 V ⊕ GV G f)))
+  let B := (univ.filter (fun d : G.Dart => d.fst ∈ Tset G f U ∧ d.snd ∈ Sset G f U)).image
+    (fun d => (.inr (.inl d.edge) : (Gr G f U).ConnectedComponent ⊕ (Sym2 V ⊕ GV G f)))
+  let C := (univ.filter (fun p : Σ v : V, Fin (G.degree v - f v) => p.1 ∈ Sset G f U)).image
+    (fun p => (.inr (.inr (.inr p)) : (Gr G f U).ConnectedComponent ⊕ (Sym2 V ⊕ GV G f)))
+  have hsub : ({l ∈ univ.image φ | Odd #{x | φ x = l}} :
+      Finset ((Gr G f U).ConnectedComponent ⊕ (Sym2 V ⊕ GV G f))) ⊆ A ∪ B ∪ C := by
+    intro l hl
+    simp only [mem_filter, mem_image, mem_univ, true_and] at hl
+    obtain ⟨⟨x, rfl⟩, hodd⟩ := hl
+    obtain ⟨a, ha⟩ := x
+    have haU : a ∉ U := (mem_del_verts _).mp ha
+    simp only [mem_union]
+    by_cases hh : home G f U a ∈ Sset G f U ∪ Tset G f U
+    · rcases a with d | p
+      · have hS := fst_notMem_S_of_notMem haU
+        have hT : d.fst ∈ Tset G f U := by
+          by_contra hT
+          rw [home_inl, ite_eq_right hT] at hh
+          rcases mem_union.mp hh with h | h
+          · exact hS h
+          · exact hT h
+        have hsnd : d.snd ∈ Sset G f U ∪ Tset G f U := by rwa [home_inl, ite_eq_left hT] at hh
+        have hφ : φ ⟨.inl d, ha⟩ = .inr (.inl d.edge) := lab_inl_of_mem hh
+        by_cases hsS : d.snd ∈ Sset G f U
+        · left; right
+          rw [hφ]
+          exact mem_image.mpr ⟨d, by simp [hT, hsS], rfl⟩
+        · exfalso
+          have hsT : d.snd ∈ Tset G f U := by
+            rcases mem_union.mp hsnd with h | h
+            · exact absurd h hsS
+            · exact h
+          rw [hφ] at hodd
+          have := card_fiber_TT hmin haU hT hsT
+          rw [this] at hodd
+          exact (Nat.not_odd_iff_even.mpr even_two) hodd
+      · right
+        have hφ : φ ⟨.inr p, ha⟩ = .inr (.inr (.inr p)) := lab_inr_of_mem hh
+        rw [hφ]
+        have hpT : p.1 ∉ Tset G f U := by
+          obtain ⟨v, i⟩ := p
+          exact notMem_T_of_inner_notMem haU
+        have hpS : p.1 ∈ Sset G f U := by
+          rcases mem_union.mp hh with h | h
+          · exact h
+          · exact absurd h hpT
+        exact mem_image.mpr ⟨p, by simp [hpS], rfl⟩
+    · left; left
+      have hφ : φ ⟨a, ha⟩ = .inl ((Gr G f U).connectedComponentMk ⟨home G f U a, hh⟩) :=
+        lab_of_notMem hh
+      rw [hφ] at hodd ⊢
+      exact mem_image.mpr ⟨_, by simpa using hodd, rfl⟩
+  have hA : #A ≤ oddCount G f (Sset G f U) (Tset G f U) := by
+    refine card_image_le.trans (le_of_eq ?_)
+    rw [oddCount, Nat.card_eq_fintype_card, Fintype.card_subtype]
+    exact card_filter_congr' _ _ (fun c => odd_fiber_iff hmin hf c)
+  have key : ∀ s : Finset ((Gr G f U).ConnectedComponent ⊕ (Sym2 V ⊕ GV G f)),
+      (∀ l ∈ s, l ∈ ({l ∈ univ.image φ | Odd #{x | φ x = l}} :
+        Finset ((Gr G f U).ConnectedComponent ⊕ (Sym2 V ⊕ GV G f)))) →
+      #s ≤ #(A ∪ B ∪ C) := fun s hs => card_le_card (fun l hl => hsub (hs l hl))
+  refine le_trans (key _ (fun l hl => by
+    simp only [mem_filter, mem_image] at hl ⊢
+    exact ⟨hl.1, by convert hl.2 using 2; ext; simp⟩)) ?_
+  have h2 := card_union_le (A ∪ B) C
+  have h3 := card_union_le A B
+  have h4 : #B ≤ #{d : G.Dart | d.fst ∈ Tset G f U ∧ d.snd ∈ Sset G f U} := card_image_le
+  have h5 : #C ≤ #{p : Σ v : V, Fin (G.degree v - f v) | p.1 ∈ Sset G f U} := card_image_le
+  omega
+
+open Classical in
+theorem card_dart_fst_mem (s0 : Finset V) :
+    #{d : G.Dart | d.fst ∈ s0} = ∑ v ∈ s0, G.degree v := by
+  rw [card_eq_sum_card_fiberwise (s := {d : G.Dart | d.fst ∈ s0}) (f := fun d : G.Dart => d.fst)
+    (t := s0) (fun d hd => (mem_filter.mp hd).2)]
+  refine sum_congr rfl (fun v hv => ?_)
+  rw [← G.dart_fst_fiber_card_eq_degree v, filter_filter]
+  congr 1
+  ext d
+  simp only [mem_filter, mem_univ, true_and]
+  constructor
+  · exact fun h => h.2
+  · intro h; exact ⟨h ▸ hv, h⟩
+
+open Classical in
+theorem card_inner_mem (s0 : Finset V) :
+    #{p : Σ v : V, Fin (G.degree v - f v) | p.1 ∈ s0} = ∑ v ∈ s0, (G.degree v - f v) := by
+  rw [card_eq_sum_card_fiberwise (s := {p : Σ v : V, Fin (G.degree v - f v) | p.1 ∈ s0})
+    (f := fun p : Σ v : V, Fin (G.degree v - f v) => p.1) (t := s0)
+    (fun p hp => (mem_filter.mp hp).2)]
+  refine sum_congr rfl (fun v hv => ?_)
+  rw [← card_inner_fiber (f := f) v, filter_filter]
+  congr 1
+  ext p
+  simp only [mem_filter, mem_univ, true_and]
+  constructor
+  · exact fun h => h.2
+  · intro h; exact ⟨h ▸ hv, h⟩
+
+open Classical in
+theorem card_dart_fst_snd_mem (T S : Finset V) :
+    #{d : G.Dart | d.fst ∈ T ∧ d.snd ∈ S} = ∑ t ∈ T, #{u | G.Adj t u ∧ u ∈ S} := by
+  rw [card_eq_sum_card_fiberwise (f := fun d : G.Dart => d.fst) (t := T)
+    (fun d hd => (mem_filter.mp hd).2.1)]
+  refine sum_congr rfl (fun t ht => ?_)
+  apply card_bij (fun d _ => d.snd)
+  · intro d hd
+    simp only [mem_filter, mem_univ, true_and] at hd ⊢
+    exact ⟨hd.2 ▸ d.adj, hd.1.2⟩
+  · intro d hd d' hd' h
+    simp only [mem_filter, mem_univ, true_and] at hd hd'
+    exact Dart.ext _ _ (Prod.ext (hd.2.trans hd'.2.symm) h)
+  · intro u hu
+    simp only [mem_filter, mem_univ, true_and] at hu
+    exact ⟨⟨(t, u), hu.1⟩, by simp [ht, hu.2], rfl⟩
+
+omit [DecidableEq V] in
+open Classical in
+theorem card_adj_eq_degree (v : V) : #{u | G.Adj v u} = G.degree v := by
+  rw [← card_neighborFinset_eq_degree]
+  congr 1
+  ext u
+  simp
+
+open Classical in
+theorem card_adj_split (t : V) (S : Finset V) :
+    #{u | G.Adj t u ∧ u ∈ S} + #{u | G.Adj t u ∧ u ∉ S} = G.degree t := by
+  rw [← card_adj_eq_degree, ← card_filter_add_card_filter_not (s := {u | G.Adj t u})
+    (fun u => u ∈ S), filter_filter, filter_filter]
+
+omit [DecidableEq V] in
+open Classical in
+theorem card_le_ncard_U :
+    ∑ v ∈ Sset G f U, G.degree v + ∑ v ∈ Tset G f U, (G.degree v - f v) ≤ U.ncard := by
+  let F : Finset (GV G f) := (univ.filter (fun d : G.Dart => d.fst ∈ Sset G f U)).disjSum
+    (univ.filter (fun p : Σ v : V, Fin (G.degree v - f v) => p.1 ∈ Tset G f U))
+  have hF : (F : Set (GV G f)) ⊆ U := by
+    rintro (d | p) h
+    · have h' := inl_mem_disjSum.mp (mem_coe.mp h)
+      exact F4 (mem_filter.mp h').2 rfl
+    · have h' := inr_mem_disjSum.mp (mem_coe.mp h)
+      obtain ⟨v, i⟩ := p
+      exact F5 (mem_filter.mp h').2 i
+  have := Set.ncard_le_ncard hF (Set.toFinite U)
+  rw [Set.ncard_coe_finset, card_disjSum, card_dart_fst_mem, card_inner_mem] at this
+  exact this
+
+omit [DecidableEq V] in
+open Classical in
+theorem not_isTutteViolator_iff_le {U' : Set (GV G f)} :
+    (gadget G f).IsTutteViolator U' ↔ U'.ncard < (del (gadget G f) U').oddComponents.ncard :=
+  Iff.rfl
+
+open Classical in
+variable (G f) in
+/-- Sufficiency in Tutte's f-factor theorem (classical formulation). -/
+theorem exists_factor_of_condition
+    (h : ∀ S T : Finset V, Disjoint S T → (oddCount G f S T : ℤ) ≤
+      ∑ v ∈ S, (f v : ℤ) - ∑ v ∈ T, (f v : ℤ) + ∑ v ∈ T, (#{u | G.Adj v u ∧ u ∉ S} : ℤ)) :
+    ∃ H : SimpleGraph V, H ≤ G ∧ ∀ v, #{u | H.Adj v u} = f v := by
+  have hf : ∀ v, f v ≤ G.degree v := by
+    intro v
+    have h1 := h ∅ {v} (disjoint_empty_left _)
+    have h2 := card_adj_split (G := G) v ∅
+    simp only [sum_empty, sum_singleton, zero_sub] at h1
+    have h3 : (#{u | G.Adj v u ∧ u ∈ (∅ : Finset V)}) = 0 := by simp
+    have h4 : (0 : ℤ) ≤ oddCount G f ∅ {v} := Nat.cast_nonneg _
+    omega
+  by_cases hM : ∃ M : (gadget G f).Subgraph, M.IsPerfectMatching
+  · obtain ⟨M, hM⟩ := hM
+    exact exists_factor_of_matching hf M hM
+  exfalso
+  have hviol : ∃ U, (gadget G f).IsTutteViolator U := by
+    by_contra hno
+    push Not at hno
+    exact hM (tutte.mpr hno)
+  obtain ⟨U, hU, hmin⟩ := exists_min_violator _ hviol
+  have hodd := ncard_odd_le hmin hf
+  have hUc := card_le_ncard_U (U := U)
+  have hU' := (not_isTutteViolator_iff_le).mp hU
+  have hyp := h (Sset G f U) (Tset G f U) disjoint_Sset_Tset
+  rw [card_dart_fst_snd_mem, card_inner_mem] at hodd
+  have hsplit : ∀ t, (#{u | G.Adj t u ∧ u ∈ Sset G f U} : ℤ) +
+      (#{u | G.Adj t u ∧ u ∉ Sset G f U} : ℤ) = G.degree t := by
+    intro t; exact_mod_cast card_adj_split t (Sset G f U)
+  have hsub : ∀ s : Finset V, ((∑ v ∈ s, (G.degree v - f v) : ℕ) : ℤ) =
+      ∑ v ∈ s, ((G.degree v : ℤ) - f v) := by
+    intro s
+    rw [Nat.cast_sum]
+    exact sum_congr rfl (fun v _ => Nat.cast_sub (hf v))
+  have hodd' : ((del (gadget G f) U).oddComponents.ncard : ℤ) ≤
+      oddCount G f (Sset G f U) (Tset G f U) +
+      ∑ t ∈ Tset G f U, (#{u | G.Adj t u ∧ u ∈ Sset G f U} : ℤ) +
+      ∑ v ∈ Sset G f U, ((G.degree v : ℤ) - f v) := by
+    rw [← hsub]; exact_mod_cast hodd
+  have hUc' : ∑ v ∈ Sset G f U, (G.degree v : ℤ) + ∑ v ∈ Tset G f U, ((G.degree v : ℤ) - f v) ≤
+      U.ncard := by
+    rw [← hsub]; exact_mod_cast hUc
+  have hU'' : (U.ncard : ℤ) < (del (gadget G f) U).oddComponents.ncard := by exact_mod_cast hU'
+  have hT : ∑ t ∈ Tset G f U, (#{u | G.Adj t u ∧ u ∈ Sset G f U} : ℤ) +
+      ∑ t ∈ Tset G f U, (#{u | G.Adj t u ∧ u ∉ Sset G f U} : ℤ) =
+      ∑ t ∈ Tset G f U, (G.degree t : ℤ) := by
+    rw [← sum_add_distrib]; exact sum_congr rfl (fun t _ => hsplit t)
+  simp only [sum_sub_distrib] at hodd' hUc'
+  linarith
+
+end FFactor
diff --git a/LeanPool/ClassicalMatchingFactors/Factors/Defs.lean b/LeanPool/ClassicalMatchingFactors/Factors/Defs.lean
new file mode 100644
index 000000000..1baffd527
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Factors/Defs.lean
@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Tutte
+public import Mathlib.Data.Finset.Max
+public import Mathlib.Data.Finset.Powerset
+public import Mathlib.Tactic.Choose
+public import Mathlib.Tactic.Convert
+public import Mathlib.Tactic.FinCases
+public import Mathlib.Tactic.GCongr
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Push
+public import Mathlib.Tactic.Tauto
+/-!
+
+Imported from [jtraverso/tutte-f-factor](https://github.com/jtraverso/tutte-f-factor/blob/dc3bbce463c80c499d3e9fa072d13f9145d907d0/FFactorLib/FFactorDefs.lean), registered as PALOMAR-2026-10-18-000005. The original proof is retained; module paths and imports are adapted for this collection.
+
+# The odd-component count in Tutte's f-factor criterion
+
+The necessity and sufficiency proofs use this same definition as the final criterion.
+-/
+
+@[expose] public section
+
+open Finset SimpleGraph
+
+namespace FFactor
+
+variable {V : Type*} [Fintype V] [DecidableEq V]
+
+open Classical in
+/-- Number of components of `G - (S ∪ T)` for which the degree sum plus the edges to `T` is odd. -/
+noncomputable def oddCount (G : SimpleGraph V) (f : V → ℕ) (S T : Finset V) : ℕ :=
+  Nat.card {c : (G.induce ((S ∪ T : Finset V) : Set V)ᶜ).ConnectedComponent //
+    Odd (∑ w ∈ univ.filter (fun w : ↥(((S ∪ T : Finset V) : Set V)ᶜ) =>
+        (G.induce ((S ∪ T : Finset V) : Set V)ᶜ).connectedComponentMk w = c),
+      (f w + #{t ∈ T | G.Adj w t}))}
+
+end FFactor
diff --git a/LeanPool/ClassicalMatchingFactors/Factors/Gadget.lean b/LeanPool/ClassicalMatchingFactors/Factors/Gadget.lean
new file mode 100644
index 000000000..15a5aab2d
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Factors/Gadget.lean
@@ -0,0 +1,155 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Tutte
+public import Mathlib.Data.Finset.Max
+public import Mathlib.Data.Finset.Powerset
+public import Mathlib.Tactic.Choose
+public import Mathlib.Tactic.Convert
+public import Mathlib.Tactic.FinCases
+public import Mathlib.Tactic.GCongr
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Push
+public import Mathlib.Tactic.Tauto
+/-!
+
+Imported from [jtraverso/tutte-f-factor](https://github.com/jtraverso/tutte-f-factor/blob/dc3bbce463c80c499d3e9fa072d13f9145d907d0/FFactorLib/FFactorGadget.lean), registered as PALOMAR-2026-10-18-000005. The original proof is retained; module paths and imports are adapted for this collection.
+
+# Tutte's gadget for the f-factor theorem
+
+For a graph `G` and `f : V → ℕ` we build the graph `FFactor.gadget G f` whose vertices are the
+darts of `G` ("outer" vertices) together with `deg v − f v` "inner" vertices for every `v`.
+A perfect matching of the gadget yields an f-factor of `G` (`FFactor.exists_factor_of_matching`).
+-/
+
+@[expose] public section
+
+open Finset SimpleGraph
+
+namespace FFactor
+
+variable {V : Type*} [Fintype V] (G : SimpleGraph V) (f : V → ℕ)
+
+open Classical in
+/-- Vertices of the gadget: darts of `G` and `deg v − f v` inner vertices for each `v`. -/
+abbrev GV := G.Dart ⊕ (Σ v : V, Fin (G.degree v - f v))
+
+/-- Adjacency in the gadget. -/
+def gadgetAdj : GV G f → GV G f → Prop
+  | .inl d, .inl d' => d' = d.symm
+  | .inl d, .inr p => d.fst = p.1
+  | .inr p, .inl d => d.fst = p.1
+  | .inr _, .inr _ => False
+
+/-- Tutte's gadget. -/
+noncomputable def gadget : SimpleGraph (GV G f) where
+  Adj := gadgetAdj G f
+  symm := ⟨by
+    intro x y h
+    rcases x with d | p <;> rcases y with d' | p' <;> simp only [gadgetAdj] at h ⊢
+    · rw [h, Dart.symm_symm]
+    · exact h
+    · exact h⟩
+  loopless := ⟨by
+    intro x h
+    rcases x with d | p <;> simp only [gadgetAdj] at h
+    exact Dart.symm_ne _ h.symm⟩
+
+@[simp] theorem gadget_adj_inl_inl {d d' : G.Dart} :
+    (gadget G f).Adj (.inl d) (.inl d') ↔ d' = d.symm := Iff.rfl
+open Classical in
+@[simp] theorem gadget_adj_inl_inr {d : G.Dart} {p : Σ v : V, Fin (G.degree v - f v)} :
+    (gadget G f).Adj (.inl d) (.inr p) ↔ d.fst = p.1 := Iff.rfl
+open Classical in
+@[simp] theorem gadget_adj_inr_inl {d : G.Dart} {p : Σ v : V, Fin (G.degree v - f v)} :
+    (gadget G f).Adj (.inr p) (.inl d) ↔ d.fst = p.1 := Iff.rfl
+open Classical in
+@[simp] theorem gadget_adj_inr_inr {p q : Σ v : V, Fin (G.degree v - f v)} :
+    ¬ (gadget G f).Adj (.inr p) (.inr q) := id
+
+variable {G f}
+
+open Classical in
+/-- A perfect matching of the gadget gives an f-factor of `G`. -/
+theorem exists_factor_of_matching (hf : ∀ v, f v ≤ G.degree v) (M : (gadget G f).Subgraph)
+    (hM : M.IsPerfectMatching) :
+    ∃ H : SimpleGraph V, H ≤ G ∧ ∀ v, #{u | H.Adj v u} = f v := by
+  classical
+  rw [Subgraph.isPerfectMatching_iff] at hM
+  obtain ⟨H, hH⟩ : ∃ H : SimpleGraph V, ∀ u w, H.Adj u w ↔
+      ∃ h : G.Adj u w, M.Adj (.inl ⟨(u, w), h⟩) (.inl ⟨(w, u), h.symm⟩) :=
+    ⟨{ Adj := fun u w => ∃ h : G.Adj u w, M.Adj (.inl ⟨(u, w), h⟩) (.inl ⟨(w, u), h.symm⟩)
+       symm := ⟨fun u w ⟨h, h'⟩ => ⟨h.symm, h'.symm⟩⟩
+       loopless := ⟨fun u ⟨h, _⟩ => G.loopless.irrefl u h⟩ }, fun _ _ => Iff.rfl⟩
+  refine ⟨H, fun u w h => ((hH u w).mp h).1, fun v => ?_⟩
+  have huniq : ∀ x y z, M.Adj x y → M.Adj x z → y = z := fun x y z h1 h2 =>
+    (hM x).unique h1 h2
+  set D : Finset G.Dart := {d | d.fst = v}
+  have hD : #D = G.degree v := G.dart_fst_fiber_card_eq_degree v
+  have hsplit := card_filter_add_card_filter_not
+    (s := D) (fun d => M.Adj (.inl d) (.inl d.symm))
+  -- darts matched to their reverse correspond to the `H`-neighbours of `v`
+  have h1 : #{d ∈ D | M.Adj (.inl d) (.inl d.symm)} = #{u | H.Adj v u} := by
+    apply card_bij (fun d _ => d.snd)
+    · rintro ⟨⟨a, b⟩, hab⟩ hd
+      simp only [D, mem_filter, mem_univ, true_and] at hd ⊢
+      obtain ⟨rfl, hd2⟩ := hd
+      exact (hH _ _).mpr ⟨hab, hd2⟩
+    · intro d1 hd1 d2 hd2 h
+      simp only [D, mem_filter, mem_univ, true_and] at hd1 hd2
+      exact Dart.ext _ _ (Prod.ext (hd1.1.trans hd2.1.symm) h)
+    · intro u hu
+      simp only [mem_filter, mem_univ, true_and] at hu
+      obtain ⟨h, hM'⟩ := (hH _ _).mp hu
+      exact ⟨⟨(v, u), h⟩, mem_filter.mpr ⟨mem_filter.mpr ⟨mem_univ _, rfl⟩, hM'⟩, rfl⟩
+  -- the other darts correspond to the inner vertices of `v`
+  have hex : ∀ i : Fin (G.degree v - f v), ∃ d : G.Dart, M.Adj (.inr ⟨v, i⟩) (.inl d) := by
+    intro i
+    obtain ⟨y, hy, -⟩ := hM (.inr ⟨v, i⟩)
+    rcases y with d | q
+    · exact ⟨d, hy⟩
+    · exact absurd (M.adj_sub hy) (gadget_adj_inr_inr G f)
+  have h2 : #(univ : Finset (Fin (G.degree v - f v))) =
+      #{d ∈ D | ¬ M.Adj (.inl d) (.inl d.symm)} := by
+    apply card_bij (fun i _ => Classical.choose (hex i))
+    · intro i _
+      have hi := Classical.choose_spec (hex i)
+      have hfst : (Classical.choose (hex i)).fst = v := M.adj_sub hi
+      simp only [D, mem_filter, mem_univ, true_and]
+      refine ⟨hfst, fun h => ?_⟩
+      have := huniq _ _ _ hi.symm h
+      cases this
+    · intro i _ j _ hij
+      have hi := Classical.choose_spec (hex i)
+      have hj := Classical.choose_spec (hex j)
+      rw [hij] at hi
+      have := huniq _ _ _ hi.symm hj.symm
+      simp only [Sum.inr.injEq, Sigma.mk.inj_iff, heq_eq_eq, true_and] at this
+      exact this
+    · intro d hd
+      simp only [D, mem_filter, mem_univ, true_and] at hd
+      obtain ⟨y, hy, -⟩ := hM (.inl d)
+      rcases y with d' | ⟨w, i⟩
+      · have : d' = d.symm := M.adj_sub hy
+        subst this
+        exact absurd hy hd.2
+      · have hw : d.fst = w := M.adj_sub hy
+        have hvw : v = w := hd.1.symm.trans hw
+        subst hvw
+        refine ⟨i, mem_univ _, ?_⟩
+        have hi := Classical.choose_spec (hex i)
+        have := huniq _ _ _ hi hy.symm
+        simpa using this
+  rw [card_univ, Fintype.card_fin] at h2
+  have := hf v
+  have hs : #{d ∈ D | M.Adj (.inl d) (.inl d.symm)} + #{d ∈ D | ¬ M.Adj (.inl d) (.inl d.symm)} =
+      #D := hsplit
+  rw [h1, ← h2, hD] at hs
+  omega
+
+end FFactor
diff --git a/LeanPool/ClassicalMatchingFactors/Factors/Nec.lean b/LeanPool/ClassicalMatchingFactors/Factors/Nec.lean
new file mode 100644
index 000000000..1b461fda9
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Factors/Nec.lean
@@ -0,0 +1,267 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Tutte
+public import Mathlib.Data.Finset.Max
+public import Mathlib.Data.Finset.Powerset
+public import Mathlib.Tactic.Choose
+public import Mathlib.Tactic.Convert
+public import Mathlib.Tactic.FinCases
+public import Mathlib.Tactic.GCongr
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Push
+public import Mathlib.Tactic.Ring
+public import Mathlib.Tactic.Tauto
+public import LeanPool.ClassicalMatchingFactors.Factors.Defs
+
+/-!
+
+Imported from [jtraverso/tutte-f-factor](https://github.com/jtraverso/tutte-f-factor/blob/dc3bbce463c80c499d3e9fa072d13f9145d907d0/FFactorLib/FFactorNec.lean), registered as PALOMAR-2026-10-18-000005. The original proof is retained; module paths and imports are adapted for this collection.
+
+# Necessity in Tutte's f-factor theorem
+
+* `FFactor.oddCnt_le_of_factor`: if `H ≤ G` is an f-factor, then for all disjoint `S, T`,
+  `q(S, T) ≤ ∑_S f − ∑_T f + ∑_T deg_{G − S}`.
+-/
+
+@[expose] public section
+
+open Finset SimpleGraph
+
+namespace FFactor
+
+variable {V : Type*} [Fintype V] [DecidableEq V]
+
+omit [Fintype V] [DecidableEq V] in
+/-- Handshake lemma inside a finset. -/
+theorem even_sum_card_adj (H : SimpleGraph V) [DecidableRel H.Adj] (s : Finset V) :
+    Even (∑ w ∈ s, #{u ∈ s | H.Adj w u}) := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp
+  | insert a s ha ih =>
+    rw [sum_insert ha]
+    have h1 : #{u ∈ insert a s | H.Adj a u} = #{u ∈ s | H.Adj a u} := by
+      rw [filter_insert, ite_eq_right (H.loopless.irrefl a)]
+    have h2 : ∀ w ∈ s, #{u ∈ insert a s | H.Adj w u} =
+        #{u ∈ s | H.Adj w u} + if H.Adj w a then 1 else 0 := by
+      intro w hw
+      rw [filter_insert]
+      split_ifs with h
+      · rw [card_insert_of_notMem (by simp [ha])]
+      · simp
+    rw [sum_congr rfl h2, sum_add_distrib, ← card_filter]
+    have h3 : #{w ∈ s | H.Adj w a} = #{u ∈ s | H.Adj a u} := by
+      congr 1; ext; simp [H.adj_comm]
+    rw [h1, h3]
+    obtain ⟨k, hk⟩ := ih
+    exact ⟨k + #{u ∈ s | H.Adj a u}, by omega⟩
+
+omit [Fintype V] in
+/-- Membership in the complement of `S ∪ T`. -/
+theorem mem_compl_union_iff {S T : Finset V} {u : V} :
+    u ∈ ((S ∪ T : Finset V) : Set V)ᶜ ↔ u ∉ S ∧ u ∉ T := by
+  simp
+
+open Classical in
+/-- Every component counted by `q(S, T)` has a witness vertex: an `H`-edge to `S` or a
+`G`-edge to `T` which is not in `H`. -/
+theorem exists_witness (G H : SimpleGraph V) (hHG : H ≤ G) (f : V → ℕ)
+    (hdeg : ∀ v, #{u | H.Adj v u} = f v) (S T : Finset V)
+    (c : (G.induce ((S ∪ T : Finset V) : Set V)ᶜ).ConnectedComponent)
+    (hc : Odd (∑ w ∈ univ.filter (fun w : ↥(((S ∪ T : Finset V) : Set V)ᶜ) =>
+        (G.induce ((S ∪ T : Finset V) : Set V)ᶜ).connectedComponentMk w = c),
+      (f w + #{t ∈ T | G.Adj w t}))) :
+    ∃ w : ↥(((S ∪ T : Finset V) : Set V)ᶜ),
+      (G.induce ((S ∪ T : Finset V) : Set V)ᶜ).connectedComponentMk w = c ∧
+      ((∃ z ∈ S, H.Adj w z) ∨ (∃ t ∈ T, G.Adj w t ∧ ¬H.Adj w t)) := by
+  by_contra hne
+  push Not at hne
+  let Cset : Finset V := (univ.filter (fun w : ↥(((S ∪ T : Finset V) : Set V)ᶜ) =>
+      (G.induce ((S ∪ T : Finset V) : Set V)ᶜ).connectedComponentMk w = c)).map
+      (Function.Embedding.subtype _)
+  have hmem : ∀ u (hu : u ∈ ((S ∪ T : Finset V) : Set V)ᶜ),
+      u ∈ Cset ↔ (G.induce ((S ∪ T : Finset V) : Set V)ᶜ).connectedComponentMk ⟨u, hu⟩ = c := by
+    intro u hu
+    simp only [Cset, mem_map, mem_filter, mem_univ, true_and, Function.Embedding.coe_subtype]
+    constructor
+    · rintro ⟨w, hw, rfl⟩; exact hw
+    · intro h; exact ⟨⟨u, hu⟩, h, rfl⟩
+  have hmem' : ∀ u ∈ Cset, ∃ hu : u ∈ ((S ∪ T : Finset V) : Set V)ᶜ,
+      (G.induce ((S ∪ T : Finset V) : Set V)ᶜ).connectedComponentMk ⟨u, hu⟩ = c := by
+    intro u hu
+    simp only [Cset, mem_map, mem_filter, mem_univ, true_and,
+      Function.Embedding.coe_subtype] at hu
+    obtain ⟨w, hw, rfl⟩ := hu
+    exact ⟨w.2, hw⟩
+  have hCsum : ∑ w ∈ Cset, (f w + #{t ∈ T | G.Adj w t}) =
+      ∑ w ∈ univ.filter (fun w : ↥(((S ∪ T : Finset V) : Set V)ᶜ) =>
+        (G.induce ((S ∪ T : Finset V) : Set V)ᶜ).connectedComponentMk w = c),
+      (f w + #{t ∈ T | G.Adj w t}) := sum_map _ _ _
+  rw [← hCsum] at hc
+  have hsplit : ∀ w ∈ Cset, f w + #{t ∈ T | G.Adj w t} =
+      #{u ∈ Cset | H.Adj w u} + 2 * #{t ∈ T | G.Adj w t} := by
+    intro w hw
+    obtain ⟨hwc, hwcc⟩ := hmem' w hw
+    have hne' := hne ⟨w, hwc⟩ hwcc
+    rw [← hdeg w]
+    have heq : ({u | H.Adj w u} : Finset V) =
+        {t ∈ T | G.Adj w t} ∪ {u ∈ Cset | H.Adj w u} := by
+      ext u
+      simp only [mem_filter, mem_univ, true_and, mem_union]
+      constructor
+      · intro hu
+        by_cases huT : u ∈ T
+        · exact Or.inl ⟨huT, hHG hu⟩
+        · have huS : u ∉ S := fun h => hne'.1 u h hu
+          have hu' : u ∈ ((S ∪ T : Finset V) : Set V)ᶜ := mem_compl_union_iff.mpr ⟨huS, huT⟩
+          refine Or.inr ⟨(hmem u hu').mpr ?_, hu⟩
+          rw [← hwcc]
+          exact (ConnectedComponent.connectedComponentMk_eq_of_adj
+            (by simpa using hHG hu)).symm
+      · rintro (⟨huT, hu⟩ | ⟨_, hu⟩)
+        · exact hne'.2 u huT hu
+        · exact hu
+    rw [heq, card_union_of_disjoint]
+    · ring
+    · rw [Finset.disjoint_left]
+      intro u hu hu'
+      obtain ⟨hu'', _⟩ := hmem' u (mem_filter.mp hu').1
+      exact (mem_compl_union_iff.mp hu'').2 (mem_filter.mp hu).1
+  rw [sum_congr rfl hsplit, sum_add_distrib, ← mul_sum] at hc
+  exact (Nat.not_even_iff_odd.mpr hc) ((even_sum_card_adj H Cset).add (even_two_mul _))
+
+open Classical in
+/-- `q(S, T)` is at most the number of witnesses. -/
+theorem oddCnt_le_card_witness (G H : SimpleGraph V) (hHG : H ≤ G) (f : V → ℕ)
+    (hdeg : ∀ v, #{u | H.Adj v u} = f v) (S T : Finset V) :
+    oddCount G f S T ≤ #{p ∈ (univ \ (S ∪ T)) ×ˢ (univ : Finset V) |
+      (p.2 ∈ S ∧ H.Adj p.1 p.2) ∨ (p.2 ∈ T ∧ G.Adj p.1 p.2 ∧ ¬H.Adj p.1 p.2)} := by
+  set G' := G.induce ((S ∪ T : Finset V) : Set V)ᶜ
+  set Z := ({p ∈ (univ \ (S ∪ T)) ×ˢ (univ : Finset V) |
+      (p.2 ∈ S ∧ H.Adj p.1 p.2) ∨ (p.2 ∈ T ∧ G.Adj p.1 p.2 ∧ ¬H.Adj p.1 p.2)} : Finset (V × V))
+  have hex : ∀ c : {c : G'.ConnectedComponent // Odd (∑ w ∈ univ.filter
+      (fun w : ↥(((S ∪ T : Finset V) : Set V)ᶜ) => G'.connectedComponentMk w = c),
+        (f w + #{t ∈ T | G.Adj w t}))},
+      ∃ p ∈ Z, ∃ h : p.1 ∈ ((S ∪ T : Finset V) : Set V)ᶜ,
+        G'.connectedComponentMk ⟨p.1, h⟩ = c.1 := by
+    intro c
+    obtain ⟨w, hw, hwit⟩ := exists_witness G H hHG f hdeg S T c.1 c.2
+    have hw2 := mem_compl_union_iff.mp w.2
+    rcases hwit with ⟨z, hz, hHz⟩ | ⟨t, ht, hGt, hHt⟩
+    · refine ⟨(w.1, z), ?_, w.2, hw⟩
+      simp only [Z, mem_filter, mem_product, mem_sdiff, mem_univ, mem_union, true_and]
+      exact ⟨by tauto, Or.inl ⟨hz, hHz⟩⟩
+    · refine ⟨(w.1, t), ?_, w.2, hw⟩
+      simp only [Z, mem_filter, mem_product, mem_sdiff, mem_univ, mem_union, true_and]
+      exact ⟨by tauto, Or.inr ⟨ht, hGt, hHt⟩⟩
+  let g : {c : G'.ConnectedComponent // Odd (∑ w ∈ univ.filter
+      (fun w : ↥(((S ∪ T : Finset V) : Set V)ᶜ) => G'.connectedComponentMk w = c),
+        (f w + #{t ∈ T | G.Adj w t}))} → Z :=
+    fun c => ⟨Classical.choose (hex c), (Classical.choose_spec (hex c)).1⟩
+  have hg : Function.Injective g := by
+    intro c d hcd
+    have hc := (Classical.choose_spec (hex c)).2
+    have hd := (Classical.choose_spec (hex d)).2
+    have e : Classical.choose (hex c) = Classical.choose (hex d) := congrArg Subtype.val hcd
+    obtain ⟨h1, h1'⟩ := hc
+    obtain ⟨h2, h2'⟩ := hd
+    apply Subtype.ext
+    rw [← h1', ← h2']
+    congr 2
+    rw [e]
+  have := Nat.card_le_card_of_injective g hg
+  simpa [Nat.card_eq_fintype_card, oddCount] using this
+
+/-- Splitting a sum over `V` along the disjoint sets `S`, `T` and `V \ (S ∪ T)`. -/
+theorem sum_split3 {S T : Finset V} (hST : Disjoint S T) (F : V → ℤ) :
+    ∑ u, F u = ∑ u ∈ S, F u + ∑ u ∈ T, F u + ∑ u ∈ univ \ (S ∪ T), F u := by
+  rw [← sum_union hST, ← sum_union disjoint_sdiff, union_sdiff_of_subset (subset_univ _)]
+
+open Classical in
+/-- The number of witnesses is bounded by the right-hand side of the f-factor condition. -/
+theorem card_witness_le (G H : SimpleGraph V) (hHG : H ≤ G) (f : V → ℕ)
+    (hdeg : ∀ v, #{u | H.Adj v u} = f v) (S T : Finset V) (hST : Disjoint S T) :
+    (#{p ∈ (univ \ (S ∪ T)) ×ˢ (univ : Finset V) |
+      (p.2 ∈ S ∧ H.Adj p.1 p.2) ∨ (p.2 ∈ T ∧ G.Adj p.1 p.2 ∧ ¬H.Adj p.1 p.2)} : ℤ) ≤
+      ∑ v ∈ S, (f v : ℤ) - ∑ v ∈ T, (f v : ℤ) + ∑ v ∈ T, (#{u | G.Adj v u ∧ u ∉ S} : ℤ) := by
+  set R := univ \ (S ∪ T) with hR
+  let A : V → V → ℤ := fun x y => if H.Adj x y then 1 else 0
+  let B : V → V → ℤ := fun x y => if G.Adj x y then 1 else 0
+  have hAsymm : ∀ x y, A x y = A y x := fun x y => by simp only [A, H.adj_comm]
+  have hBsymm : ∀ x y, B x y = B y x := fun x y => by simp only [B, G.adj_comm]
+  have hA0 : ∀ x y, 0 ≤ A x y := fun x y => by simp only [A]; split_ifs <;> norm_num
+  have hAB : ∀ x y, A x y ≤ B x y := fun x y => by
+    by_cases h1 : H.Adj x y
+    · simp [A, B, h1, hHG h1]
+    · by_cases h2 : G.Adj x y <;> simp [A, B, h1, h2]
+  have hmemR : ∀ u, u ∈ R ↔ u ∉ S ∧ u ∉ T := fun u => by simp [hR]
+  have hf : ∀ v, (f v : ℤ) = ∑ u, A v u := fun v => by
+    rw [← hdeg v, card_filter]; push_cast; rfl
+  have hN : ∀ t, (#{u | G.Adj t u ∧ u ∉ S} : ℤ) = ∑ u ∈ T, B t u + ∑ u ∈ R, B t u := by
+    intro t
+    rw [card_filter]; push_cast
+    rw [sum_split3 hST]
+    have h1 : ∑ u ∈ S, (if G.Adj t u ∧ u ∉ S then (1 : ℤ) else 0) = 0 :=
+      sum_eq_zero (fun u hu => by simp [hu])
+    have h2 : ∑ u ∈ T, (if G.Adj t u ∧ u ∉ S then (1 : ℤ) else 0) = ∑ u ∈ T, B t u :=
+      sum_congr rfl (fun u hu => by
+        have : u ∉ S := fun h => disjoint_left.mp hST h hu
+        simp [B, this])
+    have h3 : ∑ u ∈ R, (if G.Adj t u ∧ u ∉ S then (1 : ℤ) else 0) = ∑ u ∈ R, B t u :=
+      sum_congr rfl (fun u hu => by simp [B, ((hmemR u).mp hu).1])
+    rw [h1, h2, h3, zero_add]
+  have hZ : (#{p ∈ R ×ˢ (univ : Finset V) |
+      (p.2 ∈ S ∧ H.Adj p.1 p.2) ∨ (p.2 ∈ T ∧ G.Adj p.1 p.2 ∧ ¬H.Adj p.1 p.2)} : ℤ) =
+      ∑ w ∈ R, (∑ u ∈ S, A w u + ∑ u ∈ T, (B w u - A w u)) := by
+    rw [card_filter]; push_cast
+    rw [sum_product]
+    refine sum_congr rfl (fun w _ => ?_)
+    rw [sum_split3 hST]
+    have h1 : ∑ u ∈ S, (if (u ∈ S ∧ H.Adj w u) ∨ (u ∈ T ∧ G.Adj w u ∧ ¬H.Adj w u)
+        then (1 : ℤ) else 0) = ∑ u ∈ S, A w u :=
+      sum_congr rfl (fun u hu => by
+        have : u ∉ T := fun h => disjoint_left.mp hST hu h
+        simp [A, hu, this])
+    have h2 : ∑ u ∈ T, (if (u ∈ S ∧ H.Adj w u) ∨ (u ∈ T ∧ G.Adj w u ∧ ¬H.Adj w u)
+        then (1 : ℤ) else 0) = ∑ u ∈ T, (B w u - A w u) :=
+      sum_congr rfl (fun u hu => by
+        have : u ∉ S := fun h => disjoint_left.mp hST h hu
+        simp only [this, hu, false_and, true_and, false_or, A, B]
+        by_cases h1 : H.Adj w u
+        · simp [h1, hHG h1]
+        · by_cases h2 : G.Adj w u <;> simp [h1, h2])
+    have h3 : ∑ u ∈ R, (if (u ∈ S ∧ H.Adj w u) ∨ (u ∈ T ∧ G.Adj w u ∧ ¬H.Adj w u)
+        then (1 : ℤ) else 0) = 0 :=
+      sum_eq_zero (fun u hu => by simp [((hmemR u).mp hu).1, ((hmemR u).mp hu).2])
+    rw [h1, h2, h3, add_zero]
+  rw [hZ]
+  simp only [hf, hN, sum_split3 hST]
+  have e1 : ∑ w ∈ R, ∑ u ∈ S, A w u = ∑ s ∈ S, ∑ u ∈ R, A s u := by
+    rw [sum_comm]; exact sum_congr rfl (fun _ _ => sum_congr rfl (fun _ _ => hAsymm _ _))
+  have e2 : ∑ w ∈ R, ∑ u ∈ T, (B w u - A w u) = ∑ t ∈ T, ∑ u ∈ R, (B t u - A t u) := by
+    rw [sum_comm]
+    exact sum_congr rfl (fun _ _ => sum_congr rfl (fun _ _ => by rw [hAsymm, hBsymm]))
+  have e3 : ∑ s ∈ S, ∑ u ∈ T, A s u = ∑ t ∈ T, ∑ u ∈ S, A t u := by
+    rw [sum_comm]; exact sum_congr rfl (fun _ _ => sum_congr rfl (fun _ _ => hAsymm _ _))
+  have p1 : 0 ≤ ∑ s ∈ S, ∑ u ∈ S, A s u := sum_nonneg (fun _ _ => sum_nonneg (fun _ _ => hA0 _ _))
+  have p2 : 0 ≤ ∑ t ∈ T, ∑ u ∈ T, (B t u - A t u) :=
+    sum_nonneg (fun _ _ => sum_nonneg (fun _ _ => sub_nonneg.mpr (hAB _ _)))
+  simp only [sum_add_distrib, sum_sub_distrib] at e2 p2 ⊢
+  linarith
+
+open Classical in
+/-- Necessity in Tutte's f-factor theorem (classical formulation). -/
+theorem oddCnt_le_of_factor (G H : SimpleGraph V) (hHG : H ≤ G) (f : V → ℕ)
+    (hdeg : ∀ v, #{u | H.Adj v u} = f v) (S T : Finset V) (hST : Disjoint S T) :
+    (oddCount G f S T : ℤ) ≤
+      ∑ v ∈ S, (f v : ℤ) - ∑ v ∈ T, (f v : ℤ) + ∑ v ∈ T, (#{u | G.Adj v u ∧ u ∉ S} : ℤ) :=
+  (Nat.cast_le.mpr (oddCnt_le_card_witness G H hHG f hdeg S T)).trans
+    (card_witness_le G H hHG f hdeg S T hST)
+
+end FFactor
diff --git a/LeanPool/ClassicalMatchingFactors/Factors/Suff.lean b/LeanPool/ClassicalMatchingFactors/Factors/Suff.lean
new file mode 100644
index 000000000..99a616fa0
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Factors/Suff.lean
@@ -0,0 +1,415 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Tutte
+public import Mathlib.Data.Finset.Max
+public import Mathlib.Data.Finset.Powerset
+public import Mathlib.Tactic.Choose
+public import Mathlib.Tactic.Convert
+public import Mathlib.Tactic.FinCases
+public import Mathlib.Tactic.GCongr
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Push
+public import Mathlib.Tactic.Tauto
+public import LeanPool.ClassicalMatchingFactors.Factors.Comp
+public import LeanPool.ClassicalMatchingFactors.Factors.Gadget
+
+/-!
+
+Imported from [jtraverso/tutte-f-factor](https://github.com/jtraverso/tutte-f-factor/blob/dc3bbce463c80c499d3e9fa072d13f9145d907d0/FFactorLib/FFactorSuff.lean), registered as PALOMAR-2026-10-18-000005. The original proof is retained; module paths and imports are adapted for this collection.
+
+# Normal form of a minimal Tutte violator of the gadget
+
+For a Tutte violator `U` of `FFactor.gadget G f` such that no vertex of `U` satisfies
+`FFactor.TwoComp`, we show that for every vertex `v` of `G`, `U` contains either all inner
+vertices of `v` and no outer vertex of `v` (`v ∈ Tset`), or all outer vertices of `v` and no
+inner vertex of `v` (`v ∈ Sset`), or no vertex of `v` at all.
+-/
+
+@[expose] public section
+
+open Finset SimpleGraph
+
+namespace FFactor
+
+variable {V : Type*} [Fintype V] {G : SimpleGraph V} {f : V → ℕ}
+
+section Normal
+
+variable {U : Set (GV G f)}
+
+open Classical in
+theorem inner_mem_of_inner_mem (hmin : ∀ x ∈ U, ¬ TwoComp (gadget G f) U x) {v : V}
+    {i j : Fin (G.degree v - f v)} (hi : (.inr ⟨v, i⟩ : GV G f) ∈ U) :
+    (.inr ⟨v, j⟩ : GV G f) ∈ U := by
+  by_contra hj
+  apply hmin _ hi
+  intro a b c ha hb hc
+  let y0 : ((⊤ : (gadget G f).Subgraph).deleteVerts U).verts :=
+    ⟨.inr ⟨v, j⟩, (mem_del_verts _).mpr hj⟩
+  have key : ∀ a : ((⊤ : (gadget G f).Subgraph).deleteVerts U).verts,
+      (gadget G f).Adj (.inr ⟨v, i⟩) a → (del (gadget G f) U).Reachable a y0 := by
+    rintro ⟨a | q, haU⟩ ha
+    · exact Adj.reachable ((del_adj _).mpr (show (gadget G f).Adj (.inl a) (.inr ⟨v, j⟩) from ha))
+    · exact absurd ha (gadget_adj_inr_inr _ _)
+  exact Or.inl ((key a ha).trans (key b hb).symm)
+
+open Classical in
+theorem outer_notMem_of_inner_all (hmin : ∀ x ∈ U, ¬ TwoComp (gadget G f) U x) {v : V}
+    (hT : ∀ i, (.inr ⟨v, i⟩ : GV G f) ∈ U) {d : G.Dart} (hd : d.fst = v) :
+    (.inl d : GV G f) ∉ U := by
+  intro hdU
+  apply hmin _ hdU
+  intro a b c ha hb hc
+  have key : ∀ a : ((⊤ : (gadget G f).Subgraph).deleteVerts U).verts,
+      (gadget G f).Adj (.inl d) a → a.val = .inl d.symm := by
+    rintro ⟨a | ⟨w, i⟩, haU⟩ ha
+    · simp only [gadget_adj_inl_inl] at ha
+      simp [ha]
+    · have hw : d.fst = w := ha
+      obtain rfl : w = v := hw.symm.trans hd
+      exact absurd (hT i) ((mem_del_verts _).mp haU)
+  have : a = b := Subtype.ext ((key a ha).trans (key b hb).symm)
+  exact Or.inl (this ▸ Reachable.refl _)
+
+open Classical in
+theorem outer_notMem_of_outer_notMem (hmin : ∀ x ∈ U, ¬ TwoComp (gadget G f) U x) {v : V}
+    {z : G.Dart} (hz : z.fst = v)
+    (hzU : (.inl z : GV G f) ∉ U) {d : G.Dart} (hd : d.fst = v) :
+    (.inl d : GV G f) ∉ U := by
+  intro hdU
+  apply hmin _ hdU
+  intro a b c ha hb hc
+  let zv : ((⊤ : (gadget G f).Subgraph).deleteVerts U).verts :=
+    ⟨.inl z, (mem_del_verts _).mpr hzU⟩
+  have key : ∀ a : ((⊤ : (gadget G f).Subgraph).deleteVerts U).verts,
+      (gadget G f).Adj (.inl d) a → a.val = .inl d.symm ∨ (del (gadget G f) U).Reachable a zv := by
+    rintro ⟨a | ⟨w, i⟩, haU⟩ ha
+    · left
+      simp only [gadget_adj_inl_inl] at ha
+      simp [ha]
+    · right
+      have hw : d.fst = w := ha
+      obtain rfl : w = v := hw.symm.trans hd
+      exact Adj.reachable ((del_adj _).mpr (show (gadget G f).Adj (.inr ⟨_, i⟩) (.inl z) from hz))
+  have eqR : ∀ a b : ((⊤ : (gadget G f).Subgraph).deleteVerts U).verts, a.val = b.val →
+      (del (gadget G f) U).Reachable a b := fun a b h => by rw [Subtype.ext h]
+  have zR : ∀ a b : ((⊤ : (gadget G f).Subgraph).deleteVerts U).verts,
+      (del (gadget G f) U).Reachable a zv → (del (gadget G f) U).Reachable b zv →
+      (del (gadget G f) U).Reachable a b := fun _ _ h h' => h.trans h'.symm
+  rcases key a ha with h1 | h1 <;> rcases key b hb with h2 | h2 <;>
+    rcases key c hc with h3 | h3 <;>
+    first
+    | exact Or.inl (eqR _ _ (h1.trans h2.symm))
+    | exact Or.inl (zR _ _ h1 h2)
+    | exact Or.inr (Or.inl (eqR _ _ (h1.trans h3.symm)))
+    | exact Or.inr (Or.inl (zR _ _ h1 h3))
+    | exact Or.inr (Or.inr (eqR _ _ (h2.trans h3.symm)))
+    | exact Or.inr (Or.inr (zR _ _ h2 h3))
+
+open Classical in
+variable (G f U) in
+/-- `T`: vertices all of whose inner vertices lie in `U`. -/
+noncomputable def Tset : Finset V :=
+  {v | ∀ i : Fin (G.degree v - f v), (.inr ⟨v, i⟩ : GV G f) ∈ U}
+
+open Classical in
+variable (G f U) in
+/-- `S`: vertices not in `T` all of whose outer vertices lie in `U`. -/
+noncomputable def Sset : Finset V :=
+  {v | v ∉ Tset G f U ∧ ∀ d : G.Dart, d.fst = v → (.inl d : GV G f) ∈ U}
+
+open Classical in
+theorem disjoint_Sset_Tset : Disjoint (Sset G f U) (Tset G f U) := by
+  rw [Finset.disjoint_left]
+  intro v hv
+  simp only [Sset, mem_filter, mem_univ, true_and] at hv
+  exact hv.1
+
+open Classical in
+theorem mem_Tset {v : V} : v ∈ Tset G f U ↔ ∀ i, (.inr ⟨v, i⟩ : GV G f) ∈ U := by
+  simp [Tset]
+
+open Classical in
+theorem mem_Sset {v : V} : v ∈ Sset G f U ↔
+    v ∉ Tset G f U ∧ ∀ d : G.Dart, d.fst = v → (.inl d : GV G f) ∈ U := by
+  simp [Sset]
+
+open Classical in
+theorem F1 (hmin : ∀ x ∈ U, ¬ TwoComp (gadget G f) U x) {v : V} (hv : v ∉ Tset G f U)
+    (i : Fin (G.degree v - f v)) : (.inr ⟨v, i⟩ : GV G f) ∉ U := by
+  intro hi
+  exact hv (mem_Tset.mpr (fun j => inner_mem_of_inner_mem hmin hi))
+
+open Classical in
+theorem F2 (hmin : ∀ x ∈ U, ¬ TwoComp (gadget G f) U x) {v : V} (hv : v ∈ Tset G f U)
+    {d : G.Dart} (hd : d.fst = v) : (.inl d : GV G f) ∉ U :=
+  outer_notMem_of_inner_all hmin (mem_Tset.mp hv) hd
+
+open Classical in
+theorem F3 (hmin : ∀ x ∈ U, ¬ TwoComp (gadget G f) U x) {v : V} (hvT : v ∉ Tset G f U)
+    (hvS : v ∉ Sset G f U) {d : G.Dart} (hd : d.fst = v) : (.inl d : GV G f) ∉ U := by
+  have : ¬ ∀ d : G.Dart, d.fst = v → (.inl d : GV G f) ∈ U := fun h =>
+    hvS (mem_Sset.mpr ⟨hvT, h⟩)
+  push Not at this
+  obtain ⟨z, hz, hzU⟩ := this
+  exact outer_notMem_of_outer_notMem hmin hz hzU hd
+
+open Classical in
+theorem F4 {v : V} (hv : v ∈ Sset G f U) {d : G.Dart} (hd : d.fst = v) :
+    (.inl d : GV G f) ∈ U :=
+  (mem_Sset.mp hv).2 d hd
+
+open Classical in
+theorem F5 {v : V} (hv : v ∈ Tset G f U) (i : Fin (G.degree v - f v)) :
+    (.inr ⟨v, i⟩ : GV G f) ∈ U :=
+  mem_Tset.mp hv i
+
+open Classical in
+theorem exists_inner_of_notMem_Tset {v : V} (hv : v ∉ Tset G f U) :
+    ∃ _ : Fin (G.degree v - f v), True := by
+  by_contra h
+  push Not at h
+  exact hv (mem_Tset.mpr (fun i => (h i).elim))
+
+open Classical in
+theorem exists_dart_of_notMem_Tset {v : V} (hv : v ∉ Tset G f U) :
+    ∃ d : G.Dart, d.fst = v := by
+  obtain ⟨i, -⟩ := exists_inner_of_notMem_Tset hv
+  have : 0 < G.degree v := by have := i.2; omega
+  obtain ⟨u, hu⟩ := G.degree_pos_iff_exists_adj v |>.mp this
+  exact ⟨⟨(v, u), hu⟩, rfl⟩
+
+end Normal
+
+section Label
+
+variable [DecidableEq V] {U : Set (GV G f)}
+
+open Classical in
+variable (G f U) in
+/-- The vertex of `G` a vertex of the gadget "belongs to" after removing `U`. -/
+noncomputable def home : GV G f → V
+  | .inl d => if d.fst ∈ Tset G f U then d.snd else d.fst
+  | .inr p => p.1
+
+open Classical in
+@[simp] theorem home_inl (d : G.Dart) :
+    home G f U (.inl d) = if d.fst ∈ Tset G f U then d.snd else d.fst := rfl
+open Classical in
+@[simp] theorem home_inr (p : Σ v : V, Fin (G.degree v - f v)) :
+    home G f U (.inr p) = p.1 := rfl
+
+open Classical in
+variable (G f U) in
+/-- The graph `G - (S ∪ T)`. -/
+abbrev Gr : SimpleGraph ↥(((Sset G f U ∪ Tset G f U : Finset V) : Set V)ᶜ) :=
+  G.induce (((Sset G f U ∪ Tset G f U : Finset V) : Set V)ᶜ)
+
+open Classical in
+variable (G f U) in
+/-- The labelling of the vertices of the gadget whose fibres are the components of
+`gadget - U`. -/
+noncomputable def lab (a : GV G f) : (Gr G f U).ConnectedComponent ⊕ (Sym2 V ⊕ GV G f) :=
+  if h : home G f U a ∉ Sset G f U ∪ Tset G f U then
+    .inl ((Gr G f U).connectedComponentMk ⟨home G f U a, h⟩)
+  else match a with
+    | .inl d => .inr (.inl d.edge)
+    | .inr _ => .inr (.inr a)
+
+open Classical in
+theorem lab_of_notMem {a : GV G f} (h : home G f U a ∉ Sset G f U ∪ Tset G f U) :
+    lab G f U a = .inl ((Gr G f U).connectedComponentMk ⟨home G f U a, h⟩) := by
+  simp only [lab, dite_eq_left h]
+
+open Classical in
+theorem lab_inl_of_mem {d : G.Dart} (h : home G f U (.inl d) ∈ Sset G f U ∪ Tset G f U) :
+    lab G f U (.inl d) = .inr (.inl d.edge) := by
+  simp only [lab, h, not_true_eq_false, dite_false]
+
+open Classical in
+theorem lab_inr_of_mem {p : Σ v : V, Fin (G.degree v - f v)}
+    (h : home G f U (.inr p) ∈ Sset G f U ∪ Tset G f U) :
+    lab G f U (.inr p) = .inr (.inr (.inr p)) := by
+  simp only [lab, h, not_true_eq_false, dite_false]
+
+open Classical in
+theorem lab_eq_of_home_eq {a b : GV G f} (hab : home G f U a = home G f U b)
+    (h : home G f U a ∉ Sset G f U ∪ Tset G f U) : lab G f U a = lab G f U b := by
+  rw [lab_of_notMem h, lab_of_notMem (hab ▸ h)]
+  congr 2
+  exact Subtype.ext hab
+
+omit [DecidableEq V] in
+open Classical in
+theorem fst_notMem_S_of_notMem {d : G.Dart} (hd : (.inl d : GV G f) ∉ U) :
+    d.fst ∉ Sset G f U := fun h => hd (F4 h rfl)
+
+omit [DecidableEq V] in
+open Classical in
+theorem notMem_T_of_inner_notMem {v : V} {i : Fin (G.degree v - f v)}
+    (h : (.inr ⟨v, i⟩ : GV G f) ∉ U) : v ∉ Tset G f U := fun hv => h (F5 hv i)
+
+open Classical in
+theorem lab_eq_of_adj_inl_inr {d : G.Dart} {p : Σ v : V, Fin (G.degree v - f v)}
+    (ha : (.inl d : GV G f) ∉ U) (hb : (.inr p : GV G f) ∉ U) (hadj : d.fst = p.1) :
+    lab G f U (.inl d) = lab G f U (.inr p) := by
+  obtain ⟨v, i⟩ := p
+  simp only at hadj
+  subst hadj
+  have hT := notMem_T_of_inner_notMem hb
+  have hS := fst_notMem_S_of_notMem ha
+  apply lab_eq_of_home_eq
+  · simp [hT]
+  · simp [hT, hS]
+
+open Classical in
+theorem lab_eq_of_adj (a b : GV G f) (ha : a ∉ U) (hb : b ∉ U) (hadj : (gadget G f).Adj a b) :
+    lab G f U a = lab G f U b := by
+  rcases a with d | p <;> rcases b with d' | p'
+  · simp only [gadget_adj_inl_inl] at hadj
+    subst hadj
+    have hS1 := fst_notMem_S_of_notMem ha
+    have hS2 : d.snd ∉ Sset G f U := fst_notMem_S_of_notMem (d := d.symm) hb
+    by_cases ht1 : d.fst ∈ Tset G f U <;> by_cases ht2 : d.snd ∈ Tset G f U
+    · rw [lab_inl_of_mem (by simp [ht1, ht2]), lab_inl_of_mem (by simp [ht1, ht2]),
+        Dart.edge_symm]
+    · apply lab_eq_of_home_eq
+      · simp [ht1, ht2]
+      · simp [ht1, ht2, hS2]
+    · apply lab_eq_of_home_eq
+      · simp [ht1, ht2]
+      · simp [ht1, hS1]
+    · rw [lab_of_notMem (by simp [ht1, hS1]), lab_of_notMem (by simp [ht2, hS2])]
+      congr 1
+      apply ConnectedComponent.connectedComponentMk_eq_of_adj
+      simp [ht1, ht2, d.adj]
+  · exact lab_eq_of_adj_inl_inr ha hb hadj
+  · exact (lab_eq_of_adj_inl_inr hb ha hadj).symm
+  · exact absurd hadj (gadget_adj_inr_inr _ _)
+
+omit [DecidableEq V] in
+open Classical in
+theorem reach_adj {a b : GV G f} (ha : a ∉ U) (hb : b ∉ U) (h : (gadget G f).Adj a b) :
+    (del (gadget G f) U).Reachable ⟨a, (mem_del_verts _).mpr ha⟩
+      ⟨b, (mem_del_verts _).mpr hb⟩ :=
+  Adj.reachable ((del_adj _).mpr h)
+
+open Classical in
+theorem notMem_T_of_notMem_union {r : V} (hr : r ∉ Sset G f U ∪ Tset G f U) :
+    r ∉ Tset G f U := fun h => hr (mem_union_right _ h)
+
+open Classical in
+theorem notMem_S_of_notMem_union {r : V} (hr : r ∉ Sset G f U ∪ Tset G f U) :
+    r ∉ Sset G f U := fun h => hr (mem_union_left _ h)
+
+open Classical in
+theorem reach_inner (hmin : ∀ x ∈ U, ¬ TwoComp (gadget G f) U x) {r : V}
+    (hr : r ∉ Sset G f U ∪ Tset G f U) (x : GV G f) (hx : x ∉ U)
+    (hxr : home G f U x = r) (i : Fin (G.degree r - f r)) :
+    (del (gadget G f) U).Reachable ⟨x, (mem_del_verts _).mpr hx⟩
+      ⟨.inr ⟨r, i⟩, (mem_del_verts _).mpr (F1 hmin (notMem_T_of_notMem_union hr) i)⟩ := by
+  have hrT := notMem_T_of_notMem_union hr
+  have hrS := notMem_S_of_notMem_union hr
+  rcases x with d | ⟨r', j⟩
+  · simp only [home_inl] at hxr
+    by_cases ht : d.fst ∈ Tset G f U
+    · rw [ite_eq_left ht] at hxr
+      have hs : (.inl d.symm : GV G f) ∉ U := F3 hmin hrT hrS (d := d.symm) hxr
+      exact (reach_adj hx hs rfl).trans (reach_adj hs (F1 hmin hrT i) hxr)
+    · rw [ite_eq_right ht] at hxr
+      exact reach_adj hx (F1 hmin hrT i) hxr
+  · simp only [home_inr] at hxr
+    subst hxr
+    obtain ⟨z, hz⟩ := exists_dart_of_notMem_Tset hrT
+    have hzU : (.inl z : GV G f) ∉ U := F3 hmin hrT hrS hz
+    exact (reach_adj hx hzU hz).trans (reach_adj hzU (F1 hmin hrT i) hz)
+
+open Classical in
+theorem reach_inner_inner (hmin : ∀ x ∈ U, ¬ TwoComp (gadget G f) U x) {r r' : V}
+    (hr : r ∉ Sset G f U ∪ Tset G f U) (hr' : r' ∉ Sset G f U ∪ Tset G f U)
+    (hadj : G.Adj r r') (i : Fin (G.degree r - f r)) (i' : Fin (G.degree r' - f r')) :
+    (del (gadget G f) U).Reachable
+      ⟨.inr ⟨r, i⟩, (mem_del_verts _).mpr (F1 hmin (notMem_T_of_notMem_union hr) i)⟩
+      ⟨.inr ⟨r', i'⟩, (mem_del_verts _).mpr (F1 hmin (notMem_T_of_notMem_union hr') i')⟩ := by
+  let d : G.Dart := ⟨(r, r'), hadj⟩
+  have hd : (.inl d : GV G f) ∉ U :=
+    F3 hmin (notMem_T_of_notMem_union hr) (notMem_S_of_notMem_union hr) (d := d) rfl
+  have hd' : (.inl d.symm : GV G f) ∉ U :=
+    F3 hmin (notMem_T_of_notMem_union hr') (notMem_S_of_notMem_union hr') (d := d.symm) rfl
+  have h1 := reach_inner hmin hr (.inl d) hd
+    (by simp [d, notMem_T_of_notMem_union hr]) i
+  have h2 := reach_inner hmin hr' (.inl d.symm) hd'
+    (by simp [d, notMem_T_of_notMem_union hr']) i'
+  exact h1.symm.trans ((reach_adj hd hd' rfl).trans h2)
+
+open Classical in
+theorem reach_inner_of_reachable (hmin : ∀ x ∈ U, ¬ TwoComp (gadget G f) U x)
+    {u w : ↥(((Sset G f U ∪ Tset G f U : Finset V) : Set V)ᶜ)} (p : (Gr G f U).Walk u w) :
+    ∀ (i : Fin (G.degree u.1 - f u.1)) (i' : Fin (G.degree w.1 - f w.1)),
+    (del (gadget G f) U).Reachable
+      ⟨.inr ⟨u.1, i⟩, (mem_del_verts _).mpr (F1 hmin (notMem_T_of_notMem_union u.2) i)⟩
+      ⟨.inr ⟨w.1, i'⟩, (mem_del_verts _).mpr (F1 hmin (notMem_T_of_notMem_union w.2) i')⟩ := by
+  induction p with
+  | @nil x =>
+    intro i i'
+    exact reach_inner hmin x.2 (.inr ⟨_, i⟩) (F1 hmin (notMem_T_of_notMem_union x.2) i) rfl i'
+  | @cons a b c hadj p ih =>
+    intro i i'
+    obtain ⟨i'', -⟩ := exists_inner_of_notMem_Tset (notMem_T_of_notMem_union b.2)
+    exact (reach_inner_inner hmin a.2 b.2 hadj i i'').trans (ih i'' i')
+
+open Classical in
+theorem reach_of_lab_eq (hmin : ∀ x ∈ U, ¬ TwoComp (gadget G f) U x) (a b : GV G f)
+    (ha : a ∉ U) (hb : b ∉ U) (hab : lab G f U a = lab G f U b) :
+    (del (gadget G f) U).Reachable ⟨a, (mem_del_verts _).mpr ha⟩
+      ⟨b, (mem_del_verts _).mpr hb⟩ := by
+  by_cases hha : home G f U a ∈ Sset G f U ∪ Tset G f U
+  · rcases a with d | p <;> rcases b with d' | q
+    · by_cases hhb : home G f U (.inl d') ∈ Sset G f U ∪ Tset G f U
+      · rw [lab_inl_of_mem hha, lab_inl_of_mem hhb] at hab
+        simp only [Sum.inr.injEq, Sum.inl.injEq] at hab
+        rcases (dart_edge_eq_iff _ _).mp hab with h | h
+        · subst h; rfl
+        · subst h
+          exact reach_adj ha hb (by simp)
+      · rw [lab_inl_of_mem hha, lab_of_notMem hhb] at hab
+        simp at hab
+    · by_cases hhb : home G f U (.inr q) ∈ Sset G f U ∪ Tset G f U
+      · rw [lab_inl_of_mem hha, lab_inr_of_mem hhb] at hab
+        simp at hab
+      · rw [lab_inl_of_mem hha, lab_of_notMem hhb] at hab
+        simp at hab
+    · by_cases hhb : home G f U (.inl d') ∈ Sset G f U ∪ Tset G f U
+      · rw [lab_inr_of_mem hha, lab_inl_of_mem hhb] at hab
+        simp at hab
+      · rw [lab_inr_of_mem hha, lab_of_notMem hhb] at hab
+        simp at hab
+    · by_cases hhb : home G f U (.inr q) ∈ Sset G f U ∪ Tset G f U
+      · rw [lab_inr_of_mem hha, lab_inr_of_mem hhb] at hab
+        simp only [Sum.inr.injEq] at hab
+        subst hab; rfl
+      · rw [lab_inr_of_mem hha, lab_of_notMem hhb] at hab
+        simp at hab
+  · by_cases hhb : home G f U b ∈ Sset G f U ∪ Tset G f U
+    · exfalso
+      rw [lab_of_notMem hha] at hab
+      rcases b with d' | q
+      · rw [lab_inl_of_mem hhb] at hab; simp at hab
+      · rw [lab_inr_of_mem hhb] at hab; simp at hab
+    · rw [lab_of_notMem hha, lab_of_notMem hhb] at hab
+      simp only [Sum.inl.injEq] at hab
+      obtain ⟨p⟩ := ConnectedComponent.exact hab
+      obtain ⟨i, -⟩ := exists_inner_of_notMem_Tset (notMem_T_of_notMem_union hha)
+      obtain ⟨i', -⟩ := exists_inner_of_notMem_Tset (notMem_T_of_notMem_union hhb)
+      exact (reach_inner hmin hha a ha rfl i).trans
+        ((reach_inner_of_reachable hmin p i i').trans (reach_inner hmin hhb b hb rfl i').symm)
+
+end Label
+
+end FFactor
diff --git a/LeanPool/ClassicalMatchingFactors/Factors/Tutte.lean b/LeanPool/ClassicalMatchingFactors/Factors/Tutte.lean
new file mode 100644
index 000000000..c72a80d3b
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Factors/Tutte.lean
@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Tutte
+public import Mathlib.Data.Finset.Max
+public import Mathlib.Data.Finset.Powerset
+public import Mathlib.Tactic.Choose
+public import Mathlib.Tactic.Convert
+public import Mathlib.Tactic.FinCases
+public import Mathlib.Tactic.GCongr
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Push
+public import Mathlib.Tactic.Tauto
+public import LeanPool.ClassicalMatchingFactors.Factors.Nec
+public import LeanPool.ClassicalMatchingFactors.Factors.Count
+
+/-!
+
+Imported from [jtraverso/tutte-f-factor](https://github.com/jtraverso/tutte-f-factor/blob/dc3bbce463c80c499d3e9fa072d13f9145d907d0/FFactorLib/FFactor.lean), registered as PALOMAR-2026-10-18-000005. The original proof is retained; module paths and imports are adapted for this collection.
+
+# Tutte's f-factor theorem
+
+Let `G` be a finite simple graph and `f : V → ℕ`. An *f-factor* of `G` is a spanning subgraph
+`H ≤ G` with `deg_H v = f v` for every vertex `v`.
+
+For disjoint vertex sets `S` and `T`, let `q(S, T)` (`FFactor.oddCount`) be the number of connected
+components `C` of `G − (S ∪ T)` such that `∑_{v ∈ C} f v + e(C, T)` is odd, where `e(C, T)` is the
+number of edges between `C` and `T`.
+
+* `FFactor.tutte_f_factor`: **Tutte (1952, 1954).** `G` has an f-factor if and only if, for all
+  disjoint `S, T`,
+  `q(S, T) ≤ ∑_{v ∈ S} f v − ∑_{v ∈ T} f v + ∑_{v ∈ T} deg_{G − S} v`,
+  where `deg_{G − S} v` is the number of neighbours of `v` outside `S`.
+-/
+
+@[expose] public section
+
+open Finset SimpleGraph
+
+namespace FFactor
+
+variable {V : Type*} [Fintype V] [DecidableEq V]
+
+/-- **Tutte's f-factor theorem.** A finite simple graph `G` has a spanning subgraph `H` with
+`deg_H v = f v` for every vertex `v` if and only if, for all disjoint vertex sets `S` and `T`,
+`q(S, T) ≤ ∑_{v ∈ S} f v − ∑_{v ∈ T} f v + ∑_{v ∈ T} deg_{G − S} v`. -/
+theorem tutte_f_factor (G : SimpleGraph V) [DecidableRel G.Adj] (f : V → ℕ) :
+    (∃ H : SimpleGraph V, ∃ _ : DecidableRel H.Adj, H ≤ G ∧ ∀ v, H.degree v = f v) ↔
+      ∀ S T : Finset V, Disjoint S T →
+        (oddCount G f S T : ℤ) ≤ ∑ v ∈ S, (f v : ℤ) - ∑ v ∈ T, (f v : ℤ) +
+          ∑ v ∈ T, (#{u ∈ G.neighborFinset v | u ∉ S} : ℤ) := by
+  have hD : ∀ (H : SimpleGraph V) [DecidableRel H.Adj] v, H.degree v =
+      @Finset.card V (@Finset.filter V (fun u => H.Adj v u)
+        (fun _ => Classical.propDecidable _) univ) := by
+    intro H _ v
+    rw [← card_neighborFinset_eq_degree]
+    congr 1
+    ext u
+    simp
+  constructor
+  · rintro ⟨H, _, hHG, hdeg⟩ S T hST
+    have := oddCnt_le_of_factor G H hHG f (fun v => (hD H v).symm.trans (hdeg v)) S T hST
+    convert this using 4 with v
+    congr 1
+    ext u
+    simp
+  · intro h
+    obtain ⟨H, hHG, hdeg⟩ := exists_factor_of_condition G f (fun S T hST => by
+      have := h S T hST
+      convert this using 4 with v
+      congr 1
+      ext u
+      simp)
+    classical
+    exact ⟨H, inferInstance, hHG, fun v => (hD H v).trans (hdeg v)⟩
+
+end FFactor
diff --git a/LeanPool/ClassicalMatchingFactors/Imports.lean b/LeanPool/ClassicalMatchingFactors/Imports.lean
new file mode 100644
index 000000000..c4fbc6684
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Imports.lean
@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Lean Pool contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean Pool contributors
+-/
+module  -- shake: keep-all --deprecated_module: ignore
+
+-- Generated project imports; run `lake exe mk_all`.
+public import LeanPool.ClassicalMatchingFactors
+public import LeanPool.ClassicalMatchingFactors.Bipartite.MatchingCover
+public import LeanPool.ClassicalMatchingFactors.Factors.Comp
+public import LeanPool.ClassicalMatchingFactors.Factors.Count
+public import LeanPool.ClassicalMatchingFactors.Factors.Defs
+public import LeanPool.ClassicalMatchingFactors.Factors.Gadget
+public import LeanPool.ClassicalMatchingFactors.Factors.Nec
+public import LeanPool.ClassicalMatchingFactors.Factors.Suff
+public import LeanPool.ClassicalMatchingFactors.Factors.Tutte
+public import LeanPool.ClassicalMatchingFactors.Matching.Berge
+public import LeanPool.ClassicalMatchingFactors.Matching.Certificates
+public import LeanPool.ClassicalMatchingFactors.Matching.Petersen
+public import LeanPool.ClassicalMatchingFactors.Order.ChainPartitions
+public import LeanPool.ClassicalMatchingFactors.Regular.BalancedOrientation
+public import LeanPool.ClassicalMatchingFactors.Regular.EulerCircuit
+public import LeanPool.ClassicalMatchingFactors.Regular.EulerTrail
+public import LeanPool.ClassicalMatchingFactors.Regular.TwoFactors
diff --git a/LeanPool/ClassicalMatchingFactors/Matching/Berge.lean b/LeanPool/ClassicalMatchingFactors/Matching/Berge.lean
new file mode 100644
index 000000000..35880cd8e
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Matching/Berge.lean
@@ -0,0 +1,644 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Tutte
+public import Mathlib.Basic.Finite.Sum
+public import Mathlib.Data.Fintype.Lattice
+public import Mathlib.Data.Finset.Max
+public import Mathlib.Data.Finset.Powerset
+public import Mathlib.Tactic.Choose
+public import Mathlib.Tactic.Convert
+public import Mathlib.Tactic.FinCases
+public import Mathlib.Tactic.GCongr
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Push
+public import Mathlib.Tactic.Tauto
+/-!
+
+Imported from [jtraverso/berge-matching](https://github.com/jtraverso/berge-matching/blob/b9c91bfbbe08ee7266ee3cb3543dff4e4ca8bc8c/BergeLib/Berge.lean), registered as PALOMAR-2026-10-16-000011. The original proof is retained; module paths and imports are adapted for this collection.
+
+# Berge's augmenting path theorem and the Tutte–Berge formula
+
+For a finite simple graph `G` and a matching `M` (Mathlib's `Subgraph.IsMatching`):
+
+* `BergeMatching.isMaximum_iff_not_exists_augmenting`: **Berge (1957).** `M` has maximum size
+  among all matchings if and only if there is no `M`-augmenting path: a path whose two distinct
+  end vertices are not covered by `M` and whose edges alternate between edges outside `M` and
+  edges of `M`, starting with an edge outside `M`.
+* `BergeMatching.two_mul_card_add_le`: weak Tutte–Berge inequality: for every matching `M` and
+  every vertex set `U`, `2 |M| + odd(G − U) ≤ |V| + |U|`, where `odd(G − U)` is the number of
+  connected components of odd order of `G − U`.
+* `BergeMatching.exists_tutte_berge`: **Tutte–Berge formula (Berge 1958).** There are a matching
+  `M` and a vertex set `U` with `2 |M| + odd(G − U) = |V| + |U|`; so the maximum size of a
+  matching is the minimum of `(|V| + |U| - odd(G - U)) / 2`.
+-/
+
+@[expose] public section
+
+open SimpleGraph
+
+namespace BergeMatching
+
+variable {V : Type*}
+
+/-- The number of connected components of odd order of `G − U` (as in Mathlib's
+`SimpleGraph.IsTutteViolator`). -/
+noncomputable def oddCount (G : SimpleGraph V) (U : Set V) : ℕ :=
+  ((⊤ : G.Subgraph).deleteVerts U).coe.oddComponents.ncard
+
+/-- `p` is an `M`-augmenting path: a path between two distinct vertices not covered by `M`, whose
+`i`-th edge lies in `M` exactly when `i` is odd. -/
+def IsAugmentingPath {G : SimpleGraph V} (M : G.Subgraph) {u v : V} (p : G.Walk u v) : Prop :=
+  p.IsPath ∧ u ≠ v ∧ u ∉ M.verts ∧ v ∉ M.verts ∧
+    ∀ i < p.length, (s(p.getVert i, p.getVert (i + 1)) ∈ M.edgeSet ↔ Odd i)
+
+private lemma ncard_oddComponents_congr {W W' : Type*} {H : SimpleGraph W} {H' : SimpleGraph W'}
+    (e : H ≃g H') : H.oddComponents.ncard = H'.oddComponents.ncard := by
+  rw [← Nat.card_coe_set_eq, ← Nat.card_coe_set_eq]
+  refine Nat.card_congr (e.connectedComponentEquiv.subtypeEquiv fun c => ?_)
+  simp only [Set.mem_ofPred_eq]
+  rw [← Nat.card_coe_set_eq, ← Nat.card_coe_set_eq,
+    Nat.card_congr (ConnectedComponent.isoEquivSupp e c)]
+
+open Finset in
+private lemma ncard_verts_eq_two_mul [Finite V] {G : SimpleGraph V} {M : G.Subgraph}
+    (hM : M.IsMatching) : M.verts.ncard = 2 * M.edgeSet.ncard := by
+  classical
+  have := Fintype.ofFinite V
+  have h := M.spanningCoe.sum_degrees_eq_twice_card_edges
+  have hdeg : ∀ v, M.spanningCoe.degree v = if v ∈ M.verts then 1 else 0 := by
+    intro v
+    rw [Subgraph.degree_spanningCoe]
+    split_ifs with hv
+    · exact (Subgraph.isMatching_iff_forall_degree.1 hM) v hv
+    · exact Subgraph.degree_of_notMem_verts hv
+  simp only [hdeg, Finset.sum_boole, Nat.cast_id] at h
+  have e1 : M.verts.ncard = #{x | x ∈ M.verts} := by
+    rw [← Set.ncard_coe_finset]; congr; ext; simp
+  have e2 : M.edgeSet.ncard = #M.spanningCoe.edgeFinset := by
+    rw [← Set.ncard_coe_finset, coe_edgeFinset, Subgraph.edgeSet_spanningCoe]
+  rw [e1, e2, h]
+
+/-- The graph `G` with `d` extra universal vertices. -/
+private def aug (G : SimpleGraph V) (d : ℕ) : SimpleGraph (V ⊕ Fin d) where
+  Adj x y := x ≠ y ∧ ∀ a b, x = .inl a → y = .inl b → G.Adj a b
+  symm := ⟨fun _ _ h => ⟨h.1.symm, fun a b hx hy => (h.2 b a hy hx).symm⟩⟩
+  loopless := ⟨fun _ h => h.1 rfl⟩
+
+@[simp] private lemma aug_adj_inl_inl {G : SimpleGraph V} {d : ℕ} {a b : V} :
+    (aug G d).Adj (.inl a) (.inl b) ↔ G.Adj a b := by
+  change _ ∧ _ ↔ _
+  refine ⟨fun h => h.2 a b rfl rfl, fun h => ⟨fun h' => h.ne (Sum.inl_injective h'), ?_⟩⟩
+  rintro a' b' ha hb
+  cases ha; cases hb; exact h
+
+@[simp] private lemma aug_adj_inl_inr {G : SimpleGraph V} {d : ℕ} {a : V} {i : Fin d} :
+    (aug G d).Adj (.inl a) (.inr i) :=
+  show _ ∧ _ from ⟨Sum.inl_ne_inr, fun _ _ _ h => by cases h⟩
+
+@[simp] private lemma aug_adj_inr_inl {G : SimpleGraph V} {d : ℕ} {a : V} {i : Fin d} :
+    (aug G d).Adj (.inr i) (.inl a) :=
+  aug_adj_inl_inr.symm
+
+/-- The set of vertices of `aug G d` corresponding to `U` together with all new vertices. -/
+private def augSet (U : Set V) (d : ℕ) : Set (V ⊕ Fin d) := Sum.inl '' U ∪ Set.range Sum.inr
+
+@[simp] private lemma inl_mem_augSet {U : Set V} {d : ℕ} {a : V} :
+    (Sum.inl a : V ⊕ Fin d) ∈ augSet U d ↔ a ∈ U := by
+  simp [augSet]
+
+@[simp] private lemma inr_mem_augSet {U : Set V} {d : ℕ} {i : Fin d} :
+    (Sum.inr i : V ⊕ Fin d) ∈ augSet U d := by
+  simp [augSet]
+
+private lemma ncard_augSet [Finite V] (U : Set V) (d : ℕ) : (augSet U d).ncard = U.ncard + d := by
+  rw [augSet, Set.ncard_union_eq, Set.ncard_image_of_injective _ Sum.inl_injective,
+    Set.ncard_range_of_injective Sum.inr_injective, Nat.card_eq_fintype_card, Fintype.card_fin]
+  rw [Set.disjoint_left]
+  rintro _ ⟨a, _, rfl⟩ ⟨i, hi⟩
+  cases hi
+
+private lemma oddCount_aug_augSet (G : SimpleGraph V) (U : Set V) (d : ℕ) :
+    oddCount (aug G d) (augSet U d) = oddCount G U := by
+  let f : ((⊤ : G.Subgraph).deleteVerts U).verts →
+      ((⊤ : (aug G d).Subgraph).deleteVerts (augSet U d)).verts :=
+    fun a => ⟨Sum.inl a.1, by
+      have := a.2
+      simp only [Subgraph.deleteVerts_verts, Subgraph.verts_top, Set.mem_sdiff, Set.mem_univ,
+        true_and, augSet, Set.mem_union, Set.mem_image, Sum.inl.injEq, exists_eq_right,
+        Set.mem_range, reduceCtorEq, exists_false, or_false] at this ⊢
+      exact this⟩
+  have hf : Function.Bijective f := by
+    refine ⟨fun a b h => Subtype.ext (Sum.inl_injective (congrArg Subtype.val h)), ?_⟩
+    rintro ⟨x, hx⟩
+    simp only [Subgraph.deleteVerts_verts, Subgraph.verts_top, Set.mem_sdiff, Set.mem_univ,
+      true_and, augSet, Set.mem_union, Set.mem_image, Set.mem_range, not_or] at hx
+    rcases x with a | i
+    · refine ⟨⟨a, ?_⟩, rfl⟩
+      simp only [Subgraph.deleteVerts_verts, Subgraph.verts_top, Set.mem_sdiff, Set.mem_univ,
+        true_and]
+      exact fun ha => hx.1 ⟨a, ha, rfl⟩
+    · exact absurd ⟨i, rfl⟩ hx.2
+  let e : ((⊤ : G.Subgraph).deleteVerts U).coe ≃g
+      ((⊤ : (aug G d).Subgraph).deleteVerts (augSet U d)).coe :=
+    { Equiv.ofBijective f hf with
+      map_rel_iff' := by
+        intro a b
+        simp [f, inl_mem_augSet] }
+  exact (ncard_oddComponents_congr e).symm
+
+/-- The copy of a subgraph `M` of `G` inside `aug G d`. -/
+private def liftSub {G : SimpleGraph V} (M : G.Subgraph) (d : ℕ) : (aug G d).Subgraph where
+  verts := Sum.inl '' M.verts
+  Adj x y := ∃ a b, x = .inl a ∧ y = .inl b ∧ M.Adj a b
+  adj_sub := by
+    rintro _ _ ⟨a, b, rfl, rfl, h⟩
+    exact aug_adj_inl_inl.2 (M.adj_sub h)
+  edge_vert := by
+    rintro _ _ ⟨a, b, rfl, rfl, h⟩
+    exact ⟨a, M.edge_vert h, rfl⟩
+  symm := ⟨by
+    rintro _ _ ⟨a, b, rfl, rfl, h⟩
+    exact ⟨b, a, rfl, rfl, h.symm⟩⟩
+
+private lemma liftSub_isMatching {G : SimpleGraph V} {M : G.Subgraph} (hM : M.IsMatching) (d : ℕ) :
+    (liftSub M d).IsMatching := by
+  rintro _ ⟨a, ha, rfl⟩
+  obtain ⟨b, hb, hu⟩ := hM ha
+  refine ⟨.inl b, ⟨a, b, rfl, rfl, hb⟩, ?_⟩
+  rintro _ ⟨a', b', h1, rfl, h⟩
+  cases h1
+  rw [hu b' h]
+
+private lemma card_deleteVerts_add [Finite V] (G : SimpleGraph V) (U : Set V) :
+    Nat.card ((⊤ : G.Subgraph).deleteVerts U).verts + U.ncard = Nat.card V := by
+  have : ((⊤ : G.Subgraph).deleteVerts U).verts = Uᶜ := by ext; simp
+  rw [this, Nat.card_coe_set_eq, add_comm, Set.ncard_add_ncard_compl]
+
+private lemma aug_no_tutteViolator [Finite V] (G : SimpleGraph V) (d : ℕ)
+    (hd : ∀ U : Set V, oddCount G U ≤ U.ncard + d) (hpar : Even (Nat.card V + d))
+    (W : Set (V ⊕ Fin d)) : ¬ (aug G d).IsTutteViolator W := by
+  intro hW
+  rw [IsTutteViolator] at hW
+  by_cases h : ∀ i, Sum.inr i ∈ W
+  · have hWeq : W = augSet (Sum.inl ⁻¹' W) d := by
+      ext x
+      rcases x with a | i
+      · simp
+      · simp [h i]
+    have h1 : oddCount (aug G d) W ≤ W.ncard := by
+      rw [hWeq, oddCount_aug_augSet, ncard_augSet]
+      exact hd _
+    exact absurd hW (not_lt.2 h1)
+  · push Not at h
+    obtain ⟨i, hi⟩ := h
+    set H := ((⊤ : (aug G d).Subgraph).deleteVerts W).coe
+    have hj : (Sum.inr i : V ⊕ Fin d) ∈ ((⊤ : (aug G d).Subgraph).deleteVerts W).verts := by
+      simpa using hi
+    have hconn : ∀ x : ((⊤ : (aug G d).Subgraph).deleteVerts W).verts,
+        H.connectedComponentMk x = H.connectedComponentMk ⟨_, hj⟩ := by
+      rintro ⟨x, hx⟩
+      by_cases hxi : x = Sum.inr i
+      · subst hxi; rfl
+      · apply ConnectedComponent.connectedComponentMk_eq_of_adj
+        have hx' : x ∉ W := by simpa using hx
+        simp only [H, Subgraph.coe_adj, Subgraph.deleteVerts_adj, Subgraph.verts_top,
+          Set.mem_univ, true_and, Subgraph.top_adj]
+        refine ⟨hx', hi, ?_⟩
+        rcases x with a | i'
+        · exact aug_adj_inl_inr
+        · refine ⟨hxi, fun _ _ h _ => by cases h⟩
+    have hle : H.oddComponents.ncard ≤ 1 := by
+      refine (Set.ncard_le_one (Set.toFinite _)).2 fun c _ c' _ => ?_
+      induction c using ConnectedComponent.ind
+      induction c' using ConnectedComponent.ind
+      exact (hconn _).trans (hconn _).symm
+    have hW0 : W.ncard = 0 := by
+      change W.ncard < H.oddComponents.ncard at hW
+      omega
+    have hodd : Odd H.oddComponents.ncard := by
+      change W.ncard < H.oddComponents.ncard at hW
+      have : H.oddComponents.ncard = 1 := by omega
+      rw [this]; exact odd_one
+    rw [odd_ncard_oddComponents] at hodd
+    have := card_deleteVerts_add (aug G d) W
+    rw [hW0, Nat.card_sum, Nat.card_eq_fintype_card (α := Fin d), Fintype.card_fin] at this
+    rw [Nat.add_zero] at this
+    change Odd (Nat.card ((⊤ : (aug G d).Subgraph).deleteVerts W).verts) at hodd
+    rw [this] at hodd
+    exact (Nat.not_even_iff_odd.2 hodd) hpar
+
+section BergeHelpers
+
+variable {G : SimpleGraph V}
+
+/-- Deleting a matched pair from a matching. -/
+private lemma deleteVerts_pair_isMatching {M : G.Subgraph} (hM : M.IsMatching) {a b : V}
+    (hab : M.Adj a b) : (M.deleteVerts {a, b}).IsMatching := by
+  intro x hx
+  simp only [Subgraph.deleteVerts_verts, Set.mem_sdiff, Set.mem_insert_iff,
+    Set.mem_singleton_iff, not_or] at hx
+  obtain ⟨y, hy, hu⟩ := hM hx.1
+  have hya : y ≠ a := by
+    rintro rfl
+    exact hx.2.2 (hM.eq_of_adj_left hy.symm hab)
+  have hyb : y ≠ b := by
+    rintro rfl
+    exact hx.2.1 (hM.eq_of_adj_right hy hab)
+  refine ⟨y, ?_, fun z hz => hu z (Subgraph.deleteVerts_adj.1 hz).2.2.2.2⟩
+  simp only [Subgraph.deleteVerts_adj, Set.mem_insert_iff, Set.mem_singleton_iff, not_or]
+  exact ⟨hx.1, hx.2, M.edge_vert hy.symm, ⟨hya, hyb⟩, hy⟩
+
+private lemma deleteVerts_pair_adj_iff {M : G.Subgraph} (hM : M.IsMatching) {a b x y : V}
+    (hab : M.Adj a b) (hx : x ≠ a) (hy : y ≠ a) :
+    (M.deleteVerts {a, b}).Adj x y ↔ M.Adj x y := by
+  simp only [Subgraph.deleteVerts_adj, Set.mem_insert_iff, Set.mem_singleton_iff, not_or]
+  refine ⟨fun h => h.2.2.2.2, fun h => ⟨M.edge_vert h, ⟨hx, ?_⟩, M.edge_vert h.symm, ⟨hy, ?_⟩, h⟩⟩
+  · rintro rfl; exact hy (hM.eq_of_adj_left h hab.symm)
+  · rintro rfl; exact hx (hM.eq_of_adj_right h hab)
+
+private lemma edgeSet_deleteVerts_pair {M : G.Subgraph} (hM : M.IsMatching) {a b : V}
+    (hab : M.Adj a b) : (M.deleteVerts {a, b}).edgeSet = M.edgeSet \ {s(a, b)} := by
+  ext e
+  induction e using Sym2.ind with
+  | h x y =>
+  simp only [Subgraph.mem_edgeSet, Subgraph.deleteVerts_adj, Set.mem_insert_iff,
+    Set.mem_singleton_iff, not_or, Set.mem_sdiff]
+  constructor
+  · rintro ⟨_, ⟨hxa, hxb⟩, _, _, h⟩
+    refine ⟨h, fun he => ?_⟩
+    rcases Sym2.eq_iff.1 he with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
+    · exact hxa rfl
+    · exact hxb rfl
+  · rintro ⟨h, hne⟩
+    have hxa : x ≠ a := by
+      rintro rfl; exact hne (by rw [hM.eq_of_adj_left h hab])
+    have hxb : x ≠ b := by
+      rintro rfl; exact hne (by rw [hM.eq_of_adj_left h hab.symm, Sym2.eq_swap])
+    have hya : y ≠ a := by
+      rintro rfl; exact hne (by rw [hM.eq_of_adj_right h hab.symm, Sym2.eq_swap])
+    have hyb : y ≠ b := by
+      rintro rfl; exact hne (by rw [hM.eq_of_adj_right h hab])
+    exact ⟨M.edge_vert h, ⟨hxa, hxb⟩, M.edge_vert h.symm, ⟨hya, hyb⟩, h⟩
+
+private lemma ncard_edgeSet_deleteVerts_pair {M : G.Subgraph} (hM : M.IsMatching)
+    {a b : V}
+    (hab : M.Adj a b) : (M.deleteVerts {a, b}).edgeSet.ncard = M.edgeSet.ncard - 1 := by
+  rw [edgeSet_deleteVerts_pair hM hab,
+    Set.ncard_sdiff_singleton_of_mem (show s(a, b) ∈ M.edgeSet from hab)]
+
+private lemma not_mem_edgeSet_of_not_mem_verts {M : G.Subgraph} {a b : V} (ha : a ∉ M.verts) :
+    s(a, b) ∉ M.edgeSet := fun h => ha (M.edge_vert h)
+
+private lemma IsAugmentingPath.odd_length {M : G.Subgraph} {u v : V} {p : G.Walk u v}
+    (hp : IsAugmentingPath M p) : Odd p.length := by
+  have hL : p.length ≠ 0 := fun h => hp.2.1 (Walk.eq_of_length_eq_zero h)
+  have := hp.2.2.2.2 (p.length - 1) (by omega)
+  rw [show p.length - 1 + 1 = p.length by omega, Walk.getVert_length] at this
+  have h2 : ¬ Odd (p.length - 1) := fun h => by
+    rw [← this, Sym2.eq_swap] at h
+    exact not_mem_edgeSet_of_not_mem_verts hp.2.2.2.1 h
+  rcases Nat.even_or_odd p.length with h | h
+  · exfalso; apply h2
+    obtain ⟨k, hk⟩ := h
+    exact ⟨k - 1, by omega⟩
+  · exact h
+
+private lemma IsAugmentingPath.reverse {M : G.Subgraph} {u v : V} {p : G.Walk u v}
+    (hp : IsAugmentingPath M p) : IsAugmentingPath M p.reverse := by
+  have hodd := hp.odd_length
+  refine ⟨hp.1.reverse, hp.2.1.symm, hp.2.2.2.1, hp.2.2.1, fun i hi => ?_⟩
+  rw [Walk.length_reverse] at hi
+  rw [Walk.getVert_reverse, Walk.getVert_reverse]
+  have := hp.2.2.2.2 (p.length - (i + 1)) (by omega)
+  rw [show p.length - (i + 1) + 1 = p.length - i by omega, Sym2.eq_swap] at this
+  rw [this]
+  obtain ⟨k, hk⟩ := hodd
+  rw [Nat.odd_iff, Nat.odd_iff]
+  omega
+
+private lemma IsMatching.sup_subgraphOfAdj_deleteVerts {M : G.Subgraph} (hM : M.IsMatching)
+    {u w1 w2 : V}
+    (h : G.Adj u w1) (hu : u ∉ M.verts) (e1 : M.Adj w1 w2) :
+    (M.deleteVerts {w1, w2} ⊔ G.subgraphOfAdj h).IsMatching := by
+  refine (deleteVerts_pair_isMatching hM e1).sup (Subgraph.IsMatching.subgraphOfAdj h) ?_
+  rw [(deleteVerts_pair_isMatching hM e1).support_eq_verts,
+    (Subgraph.IsMatching.subgraphOfAdj h).support_eq_verts, subgraphOfAdj_verts,
+    Set.disjoint_left]
+  intro x hx hx'
+  simp only [Subgraph.deleteVerts_verts, Set.mem_sdiff, Set.mem_insert_iff,
+    Set.mem_singleton_iff, not_or] at hx hx'
+  rcases hx' with rfl | rfl
+  · exact hu hx.1
+  · exact hx.2.1 rfl
+
+private theorem exists_larger_of_augmenting [Finite V] :
+    ∀ {u v : V} (p : G.Walk u v) (M : G.Subgraph), M.IsMatching → IsAugmentingPath M p →
+      ∃ M' : G.Subgraph, M'.IsMatching ∧ M.edgeSet.ncard < M'.edgeSet.ncard
+  | _, _, .nil, _, _, hp => absurd rfl hp.2.1
+  | _, _, .cons h .nil, M, hM, hp => by
+    refine ⟨M ⊔ G.subgraphOfAdj h, hM.sup (Subgraph.IsMatching.subgraphOfAdj h) ?_, ?_⟩
+    · rw [hM.support_eq_verts, (Subgraph.IsMatching.subgraphOfAdj h).support_eq_verts,
+        subgraphOfAdj_verts, Set.disjoint_left]
+      intro x hx hx'
+      rcases hx' with rfl | rfl
+      · exact hp.2.2.1 hx
+      · exact hp.2.2.2.1 hx
+    · rw [Subgraph.edgeSet_sup, edgeSet_subgraphOfAdj, Set.union_singleton,
+        Set.ncard_insert_of_notMem (not_mem_edgeSet_of_not_mem_verts hp.2.2.1)]
+      omega
+  | u, v, .cons (v := w1) h (.cons (v := w2) h2 r), M, hM, hp => by
+    obtain ⟨hpath, huv, hu, hv, he⟩ := hp
+    have e1 : M.Adj w1 w2 := by
+      have := (he 1 (by simp)).2 odd_one
+      simpa using this
+    rw [Walk.cons_isPath_iff, Walk.cons_isPath_iff, Walk.support_cons, List.mem_cons,
+      not_or] at hpath
+    obtain ⟨⟨hr, hw1⟩, huw1, hur⟩ := hpath
+    set M1 := M.deleteVerts {w1, w2} ⊔ G.subgraphOfAdj h with hM1def
+    have hM1 : M1.IsMatching := IsMatching.sup_subgraphOfAdj_deleteVerts hM h hu e1
+    have hcount : M1.edgeSet.ncard = M.edgeSet.ncard := by
+      have hpos : 0 < M.edgeSet.ncard :=
+        (Set.ncard_pos (Set.toFinite _)).2 ⟨_, show s(w1, w2) ∈ M.edgeSet from e1⟩
+      rw [hM1def, Subgraph.edgeSet_sup, edgeSet_deleteVerts_pair hM e1, edgeSet_subgraphOfAdj,
+        Set.union_singleton, Set.ncard_insert_of_notMem
+          (fun hm => not_mem_edgeSet_of_not_mem_verts hu hm.1),
+        Set.ncard_sdiff_singleton_of_mem (show s(w1, w2) ∈ M.edgeSet from e1)]
+      omega
+    have hadj : ∀ a b, a ∈ r.support → b ∈ r.support → (M1.Adj a b ↔ M.Adj a b) := by
+      intro a b ha hb
+      have hau : a ≠ u := fun h' => hur (h' ▸ ha)
+      have haw : a ≠ w1 := fun h' => hw1 (h' ▸ ha)
+      have hbw : b ≠ w1 := fun h' => hw1 (h' ▸ hb)
+      rw [hM1def, Subgraph.sup_adj, subgraphOfAdj_adj, deleteVerts_pair_adj_iff hM e1 haw hbw]
+      refine ⟨fun h' => h'.elim id fun he' => ?_, Or.inl⟩
+      rcases Sym2.eq_iff.1 he' with ⟨h1, _⟩ | ⟨_, h1⟩
+      · exact absurd h1.symm hau
+      · exact absurd h1.symm haw
+    have hr' : IsAugmentingPath M1 r := by
+      refine ⟨hr, ?_, ?_, ?_, fun i hi => ?_⟩
+      · rintro rfl; exact hv (M.edge_vert e1.symm)
+      · have h2u : w2 ≠ u := fun h' => hur (h' ▸ r.start_mem_support)
+        have h2w : w2 ≠ w1 := fun h' => hw1 (h' ▸ r.start_mem_support)
+        rw [hM1def, Subgraph.verts_sup, subgraphOfAdj_verts]
+        simp [h2u, h2w]
+      · have hvu : v ≠ u := fun h' => hur (h' ▸ r.end_mem_support)
+        have hvw : v ≠ w1 := fun h' => hw1 (h' ▸ r.end_mem_support)
+        rw [hM1def, Subgraph.verts_sup, subgraphOfAdj_verts]
+        simp [hv, hvu, hvw]
+      · have := he (i + 2) (by simp; omega)
+        simp only [Walk.getVert_cons_succ] at this
+        rw [Subgraph.mem_edgeSet, hadj _ _ (r.getVert_mem_support _) (r.getVert_mem_support _),
+          ← Subgraph.mem_edgeSet, this, Nat.odd_iff, Nat.odd_iff]
+        omega
+    obtain ⟨M2, hM2, hlt⟩ := exists_larger_of_augmenting r M1 hM1 hr'
+    exact ⟨M2, hM2, hcount ▸ hlt⟩
+
+private lemma IsAugmentingPath.of_deleteVerts_pair {M : G.Subgraph} (hM : M.IsMatching)
+    {x1 x2 a b : V}
+    (hx12 : M.Adj x1 x2) {Q : G.Walk a b} (hQ : IsAugmentingPath (M.deleteVerts {x1, x2}) Q)
+    (hQx1 : ∀ w ∈ Q.support, w ≠ x1) (ha : a ≠ x2) (hb : b ≠ x2) : IsAugmentingPath M Q := by
+  obtain ⟨hpath, hab, ha0, hb0, he⟩ := hQ
+  refine ⟨hpath, hab, fun h => ha0 ?_, fun h => hb0 ?_, fun i hi => ?_⟩
+  · simp [h, hQx1 a Q.start_mem_support, ha]
+  · simp [h, hQx1 b Q.end_mem_support, hb]
+  · rw [← he i hi, Subgraph.mem_edgeSet, Subgraph.mem_edgeSet,
+      deleteVerts_pair_adj_iff hM hx12 (hQx1 _ (Q.getVert_mem_support _))
+        (hQx1 _ (Q.getVert_mem_support _))]
+
+private lemma IsAugmentingPath.cons_cons_deleteVerts_pair {M : G.Subgraph} (hM : M.IsMatching)
+    {x x1 x2 b : V} (hx12 : M.Adj x1 x2) (h : G.Adj x x1) (hx : x ∉ M.verts) {Q : G.Walk x2 b}
+    (hQ : IsAugmentingPath (M.deleteVerts {x1, x2}) Q)
+    (hQx : ∀ w ∈ Q.support, w ≠ x ∧ w ≠ x1) :
+    IsAugmentingPath M (.cons h (.cons (M.adj_sub hx12) Q)) := by
+  obtain ⟨hpath, hab, ha0, hb0, he⟩ := hQ
+  have hxx1 : x ≠ x1 := h.ne
+  refine ⟨?_, fun h' => (hQx b Q.end_mem_support).1 h'.symm, hx, fun h' => hb0 ?_,
+    fun i hi => ?_⟩
+  · rw [Walk.cons_isPath_iff, Walk.cons_isPath_iff, Walk.support_cons, List.mem_cons, not_or]
+    exact ⟨⟨hpath, fun h' => (hQx _ h').2 rfl⟩, hxx1, fun h' => (hQx _ h').1 rfl⟩
+  · simp [h', (hQx b Q.end_mem_support).2, hab.symm]
+  · rcases i with _ | _ | j
+    · simp only [Walk.getVert_zero, zero_add, Walk.getVert_cons_succ]
+      simp only [Nat.not_odd_zero, iff_false]
+      exact not_mem_edgeSet_of_not_mem_verts hx
+    · simp only [zero_add, Walk.getVert_cons_succ, Walk.getVert_zero, odd_one, iff_true]
+      exact hx12
+    · simp only [Walk.getVert_cons_succ, Walk.length_cons] at hi ⊢
+      rw [Subgraph.mem_edgeSet, ← deleteVerts_pair_adj_iff hM hx12
+        (hQx _ (Q.getVert_mem_support _)).2 (hQx _ (Q.getVert_mem_support _)).2,
+        ← Subgraph.mem_edgeSet, he j (by omega), Nat.odd_iff, Nat.odd_iff]
+      omega
+
+private theorem exists_augmenting_aux [Finite V] (n : ℕ) :
+    ∀ (F : Set V) (M M' : G.Subgraph), M.IsMatching → M'.IsMatching →
+      M'.edgeSet.ncard = n → M.edgeSet.ncard < n → Disjoint M'.verts F →
+      ∃ (u v : V) (p : G.Walk u v), IsAugmentingPath M p ∧ ∀ w ∈ p.support, w ∉ F := by
+  induction n with
+  | zero => intros; omega
+  | succ n ih =>
+    intro F M M' hM hM' hn hlt hF
+    obtain ⟨x, hxM', hxM⟩ : ∃ x, x ∈ M'.verts ∧ x ∉ M.verts := by
+      by_contra hcon
+      push Not at hcon
+      have := Set.ncard_le_ncard hcon
+      rw [ncard_verts_eq_two_mul hM, ncard_verts_eq_two_mul hM'] at this
+      omega
+    obtain ⟨x1, hx1, -⟩ := hM' hxM'
+    have hxF : x ∉ F := Set.disjoint_left.1 hF hxM'
+    have hx1F : x1 ∉ F := Set.disjoint_left.1 hF (M'.edge_vert hx1.symm)
+    have hxx1 : x ≠ x1 := (M'.adj_sub hx1).ne
+    by_cases hx1M : x1 ∉ M.verts
+    · refine ⟨x, x1, .cons (M'.adj_sub hx1) .nil, ⟨?_, hxx1, hxM, hx1M, ?_⟩, ?_⟩
+      · simp [Walk.cons_isPath_iff, hxx1]
+      · intro i hi
+        simp only [Walk.length_cons, Walk.length_nil, zero_add, Nat.lt_one_iff] at hi
+        subst hi
+        simp only [Walk.getVert_zero, zero_add, Walk.getVert_cons_succ, Nat.not_odd_zero,
+          iff_false]
+        exact not_mem_edgeSet_of_not_mem_verts hxM
+      · simp [hxF, hx1F]
+    · push Not at hx1M
+      obtain ⟨x2, hx12, -⟩ := hM hx1M
+      have hM0 := deleteVerts_pair_isMatching hM hx12
+      have hM0' := deleteVerts_pair_isMatching hM' hx1
+      have hn0 : (M'.deleteVerts {x, x1}).edgeSet.ncard = n := by
+        rw [ncard_edgeSet_deleteVerts_pair hM' hx1]; omega
+      have hlt0 : (M.deleteVerts {x1, x2}).edgeSet.ncard < n := by
+        have hpos : 0 < M.edgeSet.ncard :=
+          (Set.ncard_pos (Set.toFinite _)).2 ⟨_, show s(x1, x2) ∈ M.edgeSet from hx12⟩
+        rw [ncard_edgeSet_deleteVerts_pair hM hx12]; omega
+      have hF0 : Disjoint (M'.deleteVerts {x, x1}).verts (insert x (insert x1 F)) := by
+        rw [Set.disjoint_left]
+        intro a ha
+        simp only [Subgraph.deleteVerts_verts, Set.mem_sdiff, Set.mem_insert_iff,
+          Set.mem_singleton_iff, not_or] at ha ⊢
+        exact ⟨ha.2.1, ha.2.2, Set.disjoint_left.1 hF ha.1⟩
+      obtain ⟨y, z, P, hP, hPF⟩ := ih _ _ _ hM0 hM0' hn0 hlt0 hF0
+      have hPx : ∀ w ∈ P.support, w ≠ x ∧ w ≠ x1 ∧ w ∉ F := by
+        intro w hw
+        have := hPF w hw
+        simp only [Set.mem_insert_iff, not_or] at this
+        exact this
+      by_cases hy : y = x2
+      · subst hy
+        refine ⟨x, z, _, hP.cons_cons_deleteVerts_pair hM hx12 (M'.adj_sub hx1) hxM
+          fun w hw => ⟨(hPx w hw).1, (hPx w hw).2.1⟩, ?_⟩
+        intro w hw
+        simp only [Walk.support_cons, List.mem_cons] at hw
+        rcases hw with rfl | rfl | hw
+        · exact hxF
+        · exact hx1F
+        · exact (hPx w hw).2.2
+      · by_cases hz : z = x2
+        · subst hz
+          have hPx' : ∀ w ∈ P.reverse.support, w ≠ x ∧ w ≠ x1 ∧ w ∉ F := by
+            intro w hw
+            rw [Walk.support_reverse, List.mem_reverse] at hw
+            exact hPx w hw
+          refine ⟨x, y, _, hP.reverse.cons_cons_deleteVerts_pair hM hx12 (M'.adj_sub hx1) hxM
+            fun w hw => ⟨(hPx' w hw).1, (hPx' w hw).2.1⟩, ?_⟩
+          intro w hw
+          simp only [Walk.support_cons, List.mem_cons] at hw
+          rcases hw with rfl | rfl | hw
+          · exact hxF
+          · exact hx1F
+          · exact (hPx' w hw).2.2
+        · exact ⟨y, z, P, hP.of_deleteVerts_pair hM hx12 (fun w hw => (hPx w hw).2.1) hy hz,
+            fun w hw => (hPx w hw).2.2⟩
+
+end BergeHelpers
+
+/-- **Berge's theorem (1957).** A matching of a finite graph is maximum if and only if there is no
+augmenting path. -/
+theorem isMaximum_iff_not_exists_augmenting [Finite V] {G : SimpleGraph V} {M : G.Subgraph}
+    (hM : M.IsMatching) :
+    (∀ M' : G.Subgraph, M'.IsMatching → M'.edgeSet.ncard ≤ M.edgeSet.ncard) ↔
+      ¬ ∃ (u v : V) (p : G.Walk u v), IsAugmentingPath M p := by
+  constructor
+  · rintro hmax ⟨u, v, p, hp⟩
+    obtain ⟨M', hM', hlt⟩ := exists_larger_of_augmenting p M hM hp
+    exact absurd (hmax M' hM') (not_le.2 hlt)
+  · intro hno M' hM'
+    by_contra hlt
+    push Not at hlt
+    obtain ⟨u, v, p, hp, -⟩ := exists_augmenting_aux _ ∅ M M' hM hM' rfl hlt
+      (Set.disjoint_empty _)
+    exact hno ⟨u, v, p, hp⟩
+
+/-- **Weak Tutte–Berge inequality.** For every matching `M` and vertex set `U` of a finite graph,
+`2 |M| + odd(G − U) ≤ |V| + |U|`. -/
+theorem two_mul_card_add_le [Finite V] {G : SimpleGraph V} {M : G.Subgraph} (hM : M.IsMatching)
+    (U : Set V) : 2 * M.edgeSet.ncard + oddCount G U ≤ Nat.card V + U.ncard := by
+  classical
+  set d := (M.vertsᶜ).ncard with hd
+  let s : Set (V ⊕ Fin d) := Sum.inl '' M.vertsᶜ
+  let t : Set (V ⊕ Fin d) := Set.range Sum.inr
+  have hst : Disjoint s t := by
+    rw [Set.disjoint_left]
+    rintro _ ⟨a, _, rfl⟩ ⟨i, hi⟩
+    cases hi
+  have hcard : Nat.card s = Nat.card t := by
+    rw [Nat.card_coe_set_eq, Nat.card_coe_set_eq, Set.ncard_image_of_injective _ Sum.inl_injective,
+      Set.ncard_range_of_injective Sum.inr_injective, Nat.card_eq_fintype_card, Fintype.card_fin]
+  obtain ⟨f⟩ := Finite.card_eq.1 hcard
+  have hadj : ∀ v : s, (aug G d).Adj v (f v) := by
+    rintro ⟨_, a, _, rfl⟩
+    generalize f _ = y
+    obtain ⟨_, i, rfl⟩ := y
+    exact aug_adj_inl_inr
+  obtain ⟨M2, hM2v, hM2⟩ := Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv hst f hadj
+  have hM1 := liftSub_isMatching hM d
+  have hdisj : Disjoint (liftSub M d).support M2.support := by
+    rw [hM1.support_eq_verts, hM2.support_eq_verts, hM2v, Set.disjoint_union_right]
+    refine ⟨?_, ?_⟩
+    · rw [Set.disjoint_left]
+      rintro _ ⟨a, ha, rfl⟩ ⟨b, hb, hab⟩
+      cases hab
+      exact hb ha
+    · rw [Set.disjoint_left]
+      rintro _ ⟨a, _, rfl⟩ ⟨i, hi⟩
+      cases hi
+  have hperf : (liftSub M d ⊔ M2).IsPerfectMatching := by
+    refine ⟨hM1.sup hM2 hdisj, fun x => ?_⟩
+    rw [Subgraph.verts_sup, hM2v]
+    rcases x with a | i
+    · by_cases ha : a ∈ M.verts
+      · exact Or.inl ⟨a, ha, rfl⟩
+      · exact Or.inr (Or.inl ⟨a, ha, rfl⟩)
+    · exact Or.inr (Or.inr ⟨i, rfl⟩)
+  have h1 := not_isTutteViolator_of_isPerfectMatching hperf (augSet U d)
+  rw [IsTutteViolator, not_lt] at h1
+  have h2 : oddCount (aug G d) (augSet U d) ≤ U.ncard + d := by
+    rw [← ncard_augSet]; exact h1
+  rw [oddCount_aug_augSet] at h2
+  have h3 := Set.ncard_add_ncard_compl M.verts
+  rw [ncard_verts_eq_two_mul hM] at h3
+  omega
+
+/-- **The Tutte–Berge formula.** A finite graph has a matching `M` and a vertex set `U` with
+`2 |M| + odd(G − U) = |V| + |U|`. -/
+theorem exists_tutte_berge [Finite V] (G : SimpleGraph V) :
+    ∃ (M : G.Subgraph) (U : Set V), M.IsMatching ∧
+      2 * M.edgeSet.ncard + oddCount G U = Nat.card V + U.ncard := by
+  classical
+  obtain ⟨U0, hU0⟩ := Finite.exists_max (fun U : Set V => (oddCount G U : ℤ) - U.ncard)
+  have hge : U0.ncard ≤ oddCount G U0 := by
+    have := hU0 ∅
+    simp only [Set.ncard_empty, Nat.cast_zero, sub_zero] at this
+    omega
+  set d := oddCount G U0 - U0.ncard with hd
+  have hdU : ∀ U : Set V, oddCount G U ≤ U.ncard + d := by
+    intro U
+    have := hU0 U
+    omega
+  have hpar : Even (Nat.card V + d) := by
+    have h1 := (odd_ncard_oddComponents (G := ((⊤ : G.Subgraph).deleteVerts U0).coe))
+    have h2 := card_deleteVerts_add G U0
+    change Odd (oddCount G U0) ↔ _ at h1
+    rw [← h2]
+    rcases Nat.even_or_odd (oddCount G U0) with he | ho
+    · have : Even (Nat.card ((⊤ : G.Subgraph).deleteVerts U0).verts) := by
+        rw [← Nat.not_odd_iff_even, ← h1, Nat.not_odd_iff_even]; exact he
+      have : Nat.card ((⊤ : G.Subgraph).deleteVerts U0).verts + U0.ncard + d =
+          Nat.card ((⊤ : G.Subgraph).deleteVerts U0).verts + oddCount G U0 := by omega
+      rw [this]; exact Even.add (by assumption) he
+    · have h3 := h1.1 ho
+      have : Nat.card ((⊤ : G.Subgraph).deleteVerts U0).verts + U0.ncard + d =
+          Nat.card ((⊤ : G.Subgraph).deleteVerts U0).verts + oddCount G U0 := by omega
+      rw [this]; exact Odd.add_odd h3 ho
+  obtain ⟨M', hM'⟩ := tutte.2 (aug_no_tutteViolator G d hdU hpar)
+  let M : G.Subgraph :=
+    { verts := {a | ∃ b, M'.Adj (.inl a) (.inl b)}
+      Adj a b := M'.Adj (.inl a) (.inl b)
+      adj_sub := fun h => aug_adj_inl_inl.1 (M'.adj_sub h)
+      edge_vert := fun h => ⟨_, h⟩
+      symm := ⟨fun _ _ h => h.symm⟩ }
+  have hM : M.IsMatching := by
+    rintro a ⟨b, hb⟩
+    exact ⟨b, hb, fun c hc => Sum.inl_injective (hM'.1.eq_of_adj_left hc hb)⟩
+  have hp : ∀ a : V, ∃ y, M'.Adj (.inl a) y := fun a => (hM'.1 (hM'.2 (.inl a))).exists
+  choose p hp using hp
+  have hcompl : (M.vertsᶜ).ncard ≤ d := by
+    have := Set.ncard_le_ncard_of_injOn (s := M.vertsᶜ)
+      (t := Set.range (Sum.inr : Fin d → V ⊕ Fin d)) p ?_ ?_
+    · rwa [Set.ncard_range_of_injective Sum.inr_injective, Nat.card_eq_fintype_card,
+        Fintype.card_fin] at this
+    · intro a ha
+      rcases hpa : p a with b | i
+      · exact absurd ⟨b, hpa ▸ hp a⟩ ha
+      · exact ⟨i, rfl⟩
+    · intro a _ a' _ h
+      have := hM'.1.eq_of_adj_right (hp a) (h ▸ hp a')
+      exact Sum.inl_injective this
+  have hweak := two_mul_card_add_le hM U0
+  have h3 := Set.ncard_add_ncard_compl M.verts
+  rw [ncard_verts_eq_two_mul hM] at h3
+  exact ⟨M, U0, hM, by omega⟩
+
+end BergeMatching
diff --git a/LeanPool/ClassicalMatchingFactors/Matching/Certificates.lean b/LeanPool/ClassicalMatchingFactors/Matching/Certificates.lean
new file mode 100644
index 000000000..61001384e
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Matching/Certificates.lean
@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import LeanPool.ClassicalMatchingFactors.Matching.Berge
+public import LeanPool.ClassicalMatchingFactors.Bipartite.MatchingCover
+
+/-!
+# Optimality certificates for finite graph matchings
+
+An odd-component barrier certifies a maximum matching by the weak Tutte–Berge inequality.
+In a bipartite graph, a vertex cover of the same size certifies both sides of the minimax theorem.
+These interfaces consume the actual matching and vertex-cover predicates of Mathlib.
+-/
+
+@[expose] public section
+
+namespace ClassicalMatchingFactors
+
+open SimpleGraph
+
+/-- Equality in the Tutte–Berge bound certifies that the matching is maximum. -/
+theorem isMaximum_of_barrier {V : Type*} [Finite V] {G : SimpleGraph V}
+    {M : G.Subgraph} (hM : M.IsMatching) (U : Set V)
+    (heq : 2 * M.edgeSet.ncard + BergeMatching.oddCount G U = Nat.card V + U.ncard) :
+    M.IsMatching ∧
+      ∀ M' : G.Subgraph, M'.IsMatching → M'.edgeSet.ncard ≤ M.edgeSet.ncard := by
+  refine ⟨hM, ?_⟩
+  intro M' hM'
+  have hbound := BergeMatching.two_mul_card_add_le hM' U
+  omega
+
+/-- A maximum matching has both an odd-component barrier and no augmenting path. -/
+theorem exists_matching_with_barrier_and_no_augmenting {V : Type*} [Finite V]
+    (G : SimpleGraph V) :
+    ∃ (M : G.Subgraph) (U : Set V), M.IsMatching ∧
+      (¬ ∃ (u v : V) (p : G.Walk u v), BergeMatching.IsAugmentingPath M p) ∧
+      2 * M.edgeSet.ncard + BergeMatching.oddCount G U = Nat.card V + U.ncard := by
+  obtain ⟨M, U, hM, heq⟩ := BergeMatching.exists_tutte_berge G
+  exact ⟨M, U, hM, (BergeMatching.isMaximum_iff_not_exists_augmenting hM).mp
+    (isMaximum_of_barrier hM U heq).2, heq⟩
+
+/-- A bipartite graph admits a matching-cover pair certifying both optima. -/
+theorem exists_optimal_matching_cover_pair {V : Type*} [Finite V] (G : SimpleGraph V)
+    (hG : G.Colorable 2) :
+    ∃ (M : G.Subgraph) (C : Set V), M.IsMatching ∧ G.IsVertexCover C ∧
+      M.edgeSet.ncard = C.ncard ∧
+      (∀ M' : G.Subgraph, M'.IsMatching → M'.edgeSet.ncard ≤ M.edgeSet.ncard) ∧
+      ∀ C' : Set V, G.IsVertexCover C' → C.ncard ≤ C'.ncard := by
+  obtain ⟨M, C, hM, hC, heq⟩ := Konig.Egervary.exists_matching_card_eq_vertexCover G hG
+  refine ⟨M, C, hM, hC, heq, ?_, ?_⟩
+  · intro M' hM'
+    exact (Konig.Egervary.card_matching_le_card_vertexCover hM' hC).trans heq.ge
+  · intro C' hC'
+    exact heq.ge.trans (Konig.Egervary.card_matching_le_card_vertexCover hM hC')
+
+end ClassicalMatchingFactors
diff --git a/LeanPool/ClassicalMatchingFactors/Matching/Petersen.lean b/LeanPool/ClassicalMatchingFactors/Matching/Petersen.lean
new file mode 100644
index 000000000..2365f4a8c
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Matching/Petersen.lean
@@ -0,0 +1,373 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Tutte
+public import Mathlib.Data.Finset.Max
+public import Mathlib.Data.Finset.Powerset
+public import Mathlib.Tactic.Choose
+public import Mathlib.Tactic.Convert
+public import Mathlib.Tactic.FinCases
+public import Mathlib.Tactic.GCongr
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Push
+public import Mathlib.Tactic.Tauto
+/-!
+
+Imported from [jtraverso/petersen-matching](https://github.com/jtraverso/petersen-matching/blob/77630d6771d3f5a3da2185db2ff451f6c6ed5190/PetersenLib/Petersen.lean), registered as PALOMAR-2026-10-16-000004. The original proof is retained; module paths and imports are adapted for this collection.
+
+# Petersen's theorem on perfect matchings in cubic graphs
+
+For a finite simple graph that is 3-regular (`IsRegularOfDegree 3`) and has no bridge (no edge
+of the graph is a bridge, `IsBridge`):
+
+* `PetersenTheorem.exists_isPerfectMatching`: **Petersen (1891).** The graph has a perfect
+  matching.
+* `PetersenTheorem.exists_isPerfectMatching_mem`: moreover, every edge lies in some perfect
+  matching.
+
+Both follow from Tutte's theorem (Mathlib's `SimpleGraph.tutte`) by counting the edges leaving the
+odd components.
+-/
+
+@[expose] public section
+
+open SimpleGraph
+
+namespace PetersenTheorem
+
+variable {V : Type*}
+
+section Counting
+
+variable [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
+
+/-- Number of darts leaving a vertex set `C`. -/
+def outDarts (C : Finset V) : ℕ := ∑ x ∈ C, (G.neighborFinset x \ C).card
+
+/-- Number of darts inside a vertex set `C`. -/
+def innDarts (C : Finset V) : ℕ := ∑ x ∈ C, (G.neighborFinset x ∩ C).card
+
+lemma even_innDarts (C : Finset V) : Even (innDarts G C) := by
+  classical
+  let H : SimpleGraph V :=
+    { Adj := fun x y => G.Adj x y ∧ x ∈ C ∧ y ∈ C
+      symm := ⟨fun x y h => ⟨h.1.symm, h.2.2, h.2.1⟩⟩
+      loopless := ⟨fun x h => G.loopless.irrefl x h.1⟩ }
+  have hdeg : ∀ x, H.degree x = if x ∈ C then (G.neighborFinset x ∩ C).card else 0 := by
+    intro x
+    rw [← card_neighborFinset_eq_degree]
+    split_ifs with hx
+    · congr 1
+      ext y
+      simp [H, hx]
+    · rw [Finset.card_eq_zero]
+      ext y
+      simp [H, hx]
+  have hsum := H.sum_degrees_eq_twice_card_edges
+  simp only [hdeg] at hsum
+  rw [Finset.sum_ite_mem, Finset.univ_inter] at hsum
+  unfold innDarts
+  rw [hsum]
+  exact even_two_mul _
+
+lemma outDarts_add_innDarts (h3 : G.IsRegularOfDegree 3) (C : Finset V) :
+    outDarts G C + innDarts G C = 3 * C.card := by
+  unfold outDarts innDarts
+  rw [← Finset.sum_add_distrib, Finset.card_eq_sum_ones, Finset.mul_sum]
+  refine Finset.sum_congr rfl fun x _ => ?_
+  rw [Finset.card_sdiff_add_card_inter, card_neighborFinset_eq_degree, h3 x]
+  rfl
+
+lemma outDarts_ne_one (hb : ∀ e ∈ G.edgeSet, ¬ G.IsBridge e) (C : Finset V) :
+    outDarts G C ≠ 1 := by
+  intro h1
+  have hcard : (C.sigma fun x => G.neighborFinset x \ C).card = 1 := by
+    rw [Finset.card_sigma]; exact h1
+  obtain ⟨⟨x, y⟩, hD⟩ := Finset.card_eq_one.mp hcard
+  have hxy : (⟨x, y⟩ : Σ _ : V, V) ∈ C.sigma fun x => G.neighborFinset x \ C := by
+    rw [hD]; exact Finset.mem_singleton_self _
+  simp only [Finset.mem_sigma, Finset.mem_sdiff, mem_neighborFinset] at hxy
+  obtain ⟨hx, hadj, hy⟩ := hxy
+  apply hb s(x, y) hadj
+  rw [isBridge_iff]
+  rintro ⟨p⟩
+  obtain ⟨d, -, hd1, hd2⟩ := p.exists_boundary_dart (C : Set V) hx hy
+  have hdadj := d.adj
+  rw [deleteEdges_adj] at hdadj
+  have hmem : (⟨d.fst, d.snd⟩ : Σ _ : V, V) ∈ C.sigma fun x => G.neighborFinset x \ C := by
+    simp only [Finset.mem_sigma, Finset.mem_sdiff, mem_neighborFinset]
+    exact ⟨hd1, hdadj.1, hd2⟩
+  rw [hD, Finset.mem_singleton] at hmem
+  simp only [Sigma.mk.injEq, heq_eq_eq] at hmem
+  apply hdadj.2
+  rw [hmem.1, hmem.2]
+  rfl
+
+lemma three_le_outDarts (h3 : G.IsRegularOfDegree 3) (hb : ∀ e ∈ G.edgeSet, ¬ G.IsBridge e)
+    (C : Finset V) (hC : Odd C.card) : 3 ≤ outDarts G C := by
+  have h1 := outDarts_add_innDarts G h3 C
+  have h2 := even_innDarts G C
+  have h4 := outDarts_ne_one G hb C
+  obtain ⟨a, ha⟩ := h2
+  obtain ⟨b, hb⟩ := hC
+  omega
+
+lemma three_mul_card_le {ι : Type*} (h3 : G.IsRegularOfDegree 3)
+    (hb : ∀ e ∈ G.edgeSet, ¬ G.IsBridge e) (O : Finset ι) (f : ι → Finset V) (T : Finset V)
+    (hdisj : (O : Set ι).PairwiseDisjoint f) (hT : ∀ i ∈ O, Disjoint (f i) T)
+    (hclosed : ∀ i ∈ O, ∀ x ∈ f i, ∀ y, G.Adj x y → y ∉ T → y ∈ f i)
+    (hodd : ∀ i ∈ O, Odd (f i).card) :
+    3 * O.card ≤ ∑ y ∈ T, (G.neighborFinset y \ T).card := by
+  have step1 : 3 * O.card ≤ ∑ i ∈ O, ∑ x ∈ f i, (G.neighborFinset x ∩ T).card := by
+    rw [mul_comm, ← smul_eq_mul, ← Finset.sum_const]
+    refine Finset.sum_le_sum fun i hi => ?_
+    refine (three_le_outDarts G h3 hb _ (hodd i hi)).trans (le_of_eq ?_)
+    refine Finset.sum_congr rfl fun x hx => ?_
+    congr 1
+    ext y
+    simp only [Finset.mem_sdiff, Finset.mem_inter, mem_neighborFinset]
+    constructor
+    · rintro ⟨hxy, hy⟩
+      refine ⟨hxy, ?_⟩
+      by_contra hyT
+      exact hy (hclosed i hi x hx y hxy hyT)
+    · rintro ⟨hxy, hy⟩
+      exact ⟨hxy, fun hyi => Finset.disjoint_left.mp (hT i hi) hyi hy⟩
+  rw [← Finset.sum_biUnion hdisj] at step1
+  refine step1.trans ?_
+  set U := O.biUnion f with hU
+  have hUT : Disjoint U T := by
+    rw [hU, Finset.disjoint_biUnion_left]; exact hT
+  have e1 : ∀ x, (G.neighborFinset x ∩ T).card = ∑ y ∈ T, if G.Adj x y then 1 else 0 := by
+    intro x
+    rw [Finset.sum_boole, Nat.cast_id]
+    congr 1
+    ext y; simp [mem_neighborFinset, and_comm]
+  simp only [e1]
+  rw [Finset.sum_comm]
+  refine Finset.sum_le_sum fun y hy => ?_
+  rw [Finset.sum_boole, Nat.cast_id]
+  refine Finset.card_le_card fun x hx => ?_
+  simp only [Finset.mem_filter] at hx
+  simp only [Finset.mem_sdiff, mem_neighborFinset]
+  exact ⟨hx.2.symm, fun hxT => Finset.disjoint_left.mp hUT hx.1 hxT⟩
+
+end Counting
+
+lemma three_mul_oddComponents_le [Fintype V] [DecidableEq V] (G : SimpleGraph V)
+    [DecidableRel G.Adj] (h3 : G.IsRegularOfDegree 3) (hb : ∀ e ∈ G.edgeSet, ¬ G.IsBridge e)
+    {W : Type*} [Finite W] (H : SimpleGraph W) (S : Set W) (e : W ↪ V) (T : Finset V)
+    (hdisjT : ∀ w, w ∉ S → e w ∉ T)
+    (hclosed : ∀ w, w ∉ S → ∀ y, G.Adj (e w) y → y ∉ T → ∃ w', e w' = y ∧ H.Adj w w' ∧ w' ∉ S) :
+    3 * ((⊤ : H.Subgraph).deleteVerts S).coe.oddComponents.ncard ≤
+      ∑ y ∈ T, (G.neighborFinset y \ T).card := by
+  classical
+  have := Fintype.ofFinite W
+  set K := ((⊤ : H.Subgraph).deleteVerts S).coe with hK
+  have hfin : K.oddComponents.Finite := Set.toFinite _
+  rw [Set.ncard_eq_toFinset_card _ hfin]
+  let f : K.ConnectedComponent → Finset V := fun c =>
+    (c.supp.toFinset.map (Function.Embedding.subtype _)).map e
+  have hmem : ∀ c y, y ∈ f c ↔ ∃ w, ∃ hw : w ∈ ((⊤ : H.Subgraph).deleteVerts S).verts,
+      K.connectedComponentMk ⟨w, hw⟩ = c ∧ e w = y := by
+    intro c y
+    simp [f, ConnectedComponent.mem_supp_iff]
+  apply three_mul_card_le G h3 hb hfin.toFinset f T
+  · intro c _ c' _ hcc'
+    rw [Function.onFun, Finset.disjoint_left]
+    intro y hy hy'
+    obtain ⟨w, hw, rfl, rfl⟩ := (hmem _ _).mp hy
+    obtain ⟨w', hw', rfl, he⟩ := (hmem _ _).mp hy'
+    obtain rfl := e.injective he
+    exact hcc' rfl
+  · intro c _
+    rw [Finset.disjoint_left]
+    intro y hy
+    obtain ⟨w, hw, rfl, rfl⟩ := (hmem _ _).mp hy
+    exact hdisjT w (by simpa using hw)
+  · intro c _ x hx y hadj hyT
+    obtain ⟨w, hw, rfl, rfl⟩ := (hmem _ _).mp hx
+    have hwS : w ∉ S := by simpa using hw
+    obtain ⟨w', rfl, hadj', hw'S⟩ := hclosed w hwS y hadj hyT
+    have hw' : w' ∈ ((⊤ : H.Subgraph).deleteVerts S).verts := by simpa using hw'S
+    rw [hmem]
+    refine ⟨w', hw', ?_, rfl⟩
+    have hKadj : K.Adj ⟨w, hw⟩ ⟨w', hw'⟩ := by
+      simp [hK, hwS, hw'S, hadj']
+    exact (ConnectedComponent.connectedComponentMk_eq_of_adj hKadj).symm
+  · intro c hc
+    rw [Set.Finite.mem_toFinset] at hc
+    simp only [f, Finset.card_map]
+    rw [← Set.ncard_eq_toFinset_card']
+    exact hc
+
+
+lemma sum_card_neighborFinset_sdiff_le [Fintype V] [DecidableEq V] (G : SimpleGraph V)
+    [DecidableRel G.Adj] (h3 : G.IsRegularOfDegree 3) (T : Finset V) :
+    ∑ y ∈ T, (G.neighborFinset y \ T).card ≤ 3 * T.card := by
+  rw [mul_comm, ← smul_eq_mul, ← Finset.sum_const]
+  refine Finset.sum_le_sum fun y _ => (Finset.card_le_card Finset.sdiff_subset).trans ?_
+  rw [card_neighborFinset_eq_degree, h3 y]
+
+
+/-- **Petersen's theorem (1891).** A finite bridgeless cubic graph has a perfect matching. -/
+theorem exists_isPerfectMatching [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]
+    (h3 : G.IsRegularOfDegree 3) (hb : ∀ e ∈ G.edgeSet, ¬ G.IsBridge e) :
+    ∃ M : G.Subgraph, M.IsPerfectMatching := by
+  classical
+  rw [tutte]
+  intro S hS
+  rw [IsTutteViolator] at hS
+  have h := three_mul_oddComponents_le G h3 hb G S (Function.Embedding.refl V) S.toFinset
+    (fun w hw => by simpa using hw)
+    (fun w hw y hadj hy => ⟨y, rfl, hadj, by simpa using hy⟩)
+  have h' := sum_card_neighborFinset_sdiff_le G h3 S.toFinset
+  rw [← Set.ncard_eq_toFinset_card'] at h'
+  omega
+
+/-- In a finite bridgeless cubic graph every edge lies in some perfect matching. -/
+theorem exists_isPerfectMatching_mem [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]
+    (h3 : G.IsRegularOfDegree 3) (hb : ∀ e ∈ G.edgeSet, ¬ G.IsBridge e) :
+    ∀ e ∈ G.edgeSet, ∃ M : G.Subgraph, M.IsPerfectMatching ∧ e ∈ M.edgeSet := by
+  classical
+  intro e he
+  induction e using Sym2.ind with
+  | _ u v =>
+  have huv : G.Adj u v := he
+  have hne : u ≠ v := huv.ne
+  let W : Set V := ({u, v} : Set V)ᶜ
+  let G' : SimpleGraph W := G.induce W
+  obtain ⟨M', hM'⟩ : ∃ M : G'.Subgraph, M.IsPerfectMatching := by
+    rw [tutte]
+    intro S hS
+    rw [IsTutteViolator] at hS
+    have hWuv : ∀ w : W, (w : V) ≠ u ∧ (w : V) ≠ v := by
+      intro w
+      have h : (w : V) ∉ ({u, v} : Set V) := w.2
+      simp only [Set.mem_insert_iff, Set.mem_singleton_iff, not_or] at h
+      exact h
+    let T : Finset V := S.toFinset.map (Function.Embedding.subtype _) ∪ {u, v}
+    have hdisjT : ∀ w, w ∉ S → (Function.Embedding.subtype _ w : V) ∉ T := by
+      intro w hw hwT
+      rcases Finset.mem_union.mp hwT with h | h
+      · obtain ⟨w', hw', hww'⟩ := Finset.mem_map.mp h
+        obtain rfl := Subtype.val_injective hww'
+        exact hw (Set.mem_toFinset.mp hw')
+      · have := hWuv w
+        simp only [Finset.mem_insert, Finset.mem_singleton] at h
+        rcases h with h | h
+        · exact this.1 h
+        · exact this.2 h
+    have hclosed : ∀ w, w ∉ S → ∀ y, G.Adj (Function.Embedding.subtype _ w) y → y ∉ T →
+        ∃ w', Function.Embedding.subtype _ w' = y ∧ G'.Adj w w' ∧ w' ∉ S := by
+      intro w hw y hadj hy
+      have hyu : y ≠ u := by
+        rintro rfl; exact hy (Finset.mem_union_right _ (by simp))
+      have hyv : y ≠ v := by
+        rintro rfl; exact hy (Finset.mem_union_right _ (by simp))
+      have hyW : y ∈ W := by simp [W, hyu, hyv]
+      refine ⟨⟨y, hyW⟩, rfl, hadj, fun hS' => hy ?_⟩
+      exact Finset.mem_union_left _ (Finset.mem_map_of_mem _ (Set.mem_toFinset.mpr hS'))
+    have h := three_mul_oddComponents_le G h3 hb G' S (Function.Embedding.subtype _) T
+      hdisjT hclosed
+    have hle3 : ∀ y, (G.neighborFinset y \ T).card ≤ 3 := fun y =>
+      (Finset.card_le_card Finset.sdiff_subset).trans (by rw [card_neighborFinset_eq_degree, h3 y])
+    have hle2 : ∀ a b, G.Adj a b → b ∈ T → (G.neighborFinset a \ T).card ≤ 2 := by
+      intro a b hab hbT
+      have hsub : G.neighborFinset a \ T ⊆ (G.neighborFinset a).erase b := by
+        intro x hx
+        rw [Finset.mem_sdiff] at hx
+        exact Finset.mem_erase.mpr ⟨fun h => hx.2 (h ▸ hbT), hx.1⟩
+      refine (Finset.card_le_card hsub).trans ?_
+      rw [Finset.card_erase_of_mem ((mem_neighborFinset _ _ _).mpr hab),
+        card_neighborFinset_eq_degree, h3 a]
+    have hdisj : Disjoint (S.toFinset.map (Function.Embedding.subtype _)) ({u, v} : Finset V) := by
+      rw [Finset.disjoint_left]
+      intro x hx hx'
+      obtain ⟨w, -, rfl⟩ := Finset.mem_map.mp hx
+      have := hWuv w
+      simp only [Finset.mem_insert, Finset.mem_singleton] at hx'
+      rcases hx' with h | h
+      · exact this.1 h
+      · exact this.2 h
+    have key : ∀ g : V → ℕ, (∀ y, g y ≤ 3) → g u ≤ 2 → g v ≤ 2 →
+        ∑ y ∈ T, g y ≤ 3 * S.ncard + 4 := by
+      intro g hg hgu hgv
+      simp only [T]
+      rw [Finset.sum_union hdisj, Finset.sum_pair hne]
+      have h1 : ∑ x ∈ S.toFinset.map (Function.Embedding.subtype _), g x ≤ S.ncard * 3 := by
+        rw [Set.ncard_eq_toFinset_card', ← Finset.card_map (Function.Embedding.subtype _)]
+        have h := Finset.sum_le_card_nsmul (S.toFinset.map (Function.Embedding.subtype _)) g 3
+          (fun y _ => hg y)
+        rw [smul_eq_mul] at h
+        exact h
+      omega
+    have hsum : ∑ y ∈ T, (G.neighborFinset y \ T).card ≤ 3 * S.ncard + 4 :=
+      key _ hle3 (hle2 u v huv (Finset.mem_union_right _ (by simp)))
+        (hle2 v u huv.symm (Finset.mem_union_right _ (by simp)))
+    -- parity
+    have hpar := odd_ncard_oddComponents (G := ((⊤ : G'.Subgraph).deleteVerts S).coe)
+    have hdiff : Nat.card ↥((⊤ : G'.Subgraph).deleteVerts S).verts + S.ncard = W.ncard := by
+      rw [Nat.card_coe_set_eq, Subgraph.deleteVerts_verts, Subgraph.verts_top,
+        Set.ncard_sdiff_add_ncard_of_subset (Set.subset_univ S), Set.ncard_univ,
+        Nat.card_coe_set_eq]
+    have hW : 2 + W.ncard = Nat.card V := by
+      rw [← Set.ncard_pair hne]; exact Set.ncard_add_ncard_compl _
+    have hV : Even (Nat.card V) := by
+      have hs := G.sum_degrees_eq_twice_card_edges
+      simp only [h3.degree_eq, Finset.sum_const, smul_eq_mul, Finset.card_univ] at hs
+      rw [Nat.card_eq_fintype_card]
+      exact Nat.even_iff.mpr (by omega)
+    rw [Nat.odd_iff, Nat.odd_iff] at hpar
+    rw [Nat.even_iff] at hV
+    omega
+  rw [Subgraph.isPerfectMatching_iff] at hM'
+  let M : G.Subgraph :=
+    { verts := Set.univ
+      Adj := fun a b => s(a, b) = s(u, v) ∨
+        ∃ (ha : a ∈ W) (hb : b ∈ W), M'.Adj ⟨a, ha⟩ ⟨b, hb⟩
+      adj_sub := by
+        rintro a b (h | ⟨ha, hb, h⟩)
+        · rcases Sym2.eq_iff.mp h with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
+          · exact huv
+          · exact huv.symm
+        · exact M'.adj_sub h
+      edge_vert := fun _ => Set.mem_univ _
+      symm := ⟨by
+        rintro a b (h | ⟨ha, hb, h⟩)
+        · left; rw [Sym2.eq_swap]; exact h
+        · exact Or.inr ⟨hb, ha, h.symm⟩⟩ }
+  have hWuv : ∀ a, a ∈ W ↔ a ≠ u ∧ a ≠ v := by
+    intro a; simp [W, not_or]
+  refine ⟨M, ?_, Or.inl rfl⟩
+  rw [Subgraph.isPerfectMatching_iff]
+  intro a
+  by_cases hau : a = u
+  · subst hau
+    refine ⟨v, Or.inl rfl, ?_⟩
+    rintro b (h | ⟨ha, -, -⟩)
+    · exact Sym2.congr_right.mp h
+    · exact absurd rfl ((hWuv a).mp ha).1
+  by_cases hav : a = v
+  · subst hav
+    refine ⟨u, Or.inl Sym2.eq_swap, ?_⟩
+    rintro b (h | ⟨ha, -, -⟩)
+    · rcases Sym2.eq_iff.mp h with ⟨h1, -⟩ | ⟨-, h2⟩
+      · exact absurd h1.symm hne
+      · exact h2
+    · exact absurd rfl ((hWuv a).mp ha).2
+  have ha : a ∈ W := (hWuv a).mpr ⟨hau, hav⟩
+  obtain ⟨w, hw, huniq⟩ := hM' ⟨a, ha⟩
+  refine ⟨w, Or.inr ⟨ha, w.2, hw⟩, ?_⟩
+  rintro b (h | ⟨_, hb, h⟩)
+  · rcases Sym2.eq_iff.mp h with ⟨h1, -⟩ | ⟨h1, -⟩
+    · exact absurd h1 hau
+    · exact absurd h1 hav
+  · exact congrArg Subtype.val (huniq ⟨b, hb⟩ h)
+
+end PetersenTheorem
diff --git a/LeanPool/ClassicalMatchingFactors/Order/ChainPartitions.lean b/LeanPool/ClassicalMatchingFactors/Order/ChainPartitions.lean
new file mode 100644
index 000000000..36df2b329
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Order/ChainPartitions.lean
@@ -0,0 +1,329 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import Mathlib.Order.Antichain
+public import Mathlib.Order.Preorder.Finite
+public import Mathlib.Data.Fintype.EquivFin
+public import Mathlib.Data.Fintype.Powerset
+public import Mathlib.Data.Finset.Max
+public import Mathlib.Data.Finset.Powerset
+public import Mathlib.Tactic.Choose
+public import Mathlib.Tactic.Convert
+public import Mathlib.Tactic.FinCases
+public import Mathlib.Tactic.GCongr
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Push
+public import Mathlib.Tactic.Tauto
+/-!
+
+Imported from [jtraverso/konig-edge-colouring](https://github.com/jtraverso/konig-edge-colouring/blob/7c60f7efb69c1747aaf39e5dfa7a89d907cd84ef/Konig/Dilworth.lean), registered as PALOMAR-2026-10-15-000019. The original proof is retained; module paths and imports are adapted for this collection.
+
+# Dilworth's and Mirsky's theorems
+
+For a finite partially ordered set:
+
+* `dilworth`: **Dilworth (1950).** There are an antichain `A` and a partition of the poset into
+  `|A|` chains; hence the maximum size of an antichain equals the minimum number of chains
+  covering the poset.
+* `mirsky`: **Mirsky (1971).** There are a chain `C` and a partition of the poset into `|C|`
+  antichains; hence the maximum size of a chain equals the minimum number of antichains covering
+  the poset.
+
+A partition into `m` parts is a map to `Fin m`, whose fibres are the parts (some may be empty).
+-/
+
+@[expose] public section
+
+namespace Konig.Poset
+
+open Classical in
+/-- The width of a finite set: the maximum size of an antichain contained in it. -/
+noncomputable def antichainWidth {α : Type*} [PartialOrder α] (S : Finset α) : ℕ :=
+  (S.powerset.filter (fun A : Finset α => IsAntichain (· ≤ ·) (A : Set α))).sup Finset.card
+
+section
+variable {α : Type*} [PartialOrder α]
+
+lemma card_le_antichainWidth {S A : Finset α} (hAS : A ⊆ S)
+    (hA : IsAntichain (· ≤ ·) (A : Set α)) : A.card ≤ antichainWidth S := by
+  classical
+  unfold antichainWidth
+  exact Finset.le_sup (f := Finset.card) (Finset.mem_filter.2 ⟨Finset.mem_powerset.2 hAS, hA⟩)
+
+lemma exists_card_eq_antichainWidth (S : Finset α) :
+    ∃ A ⊆ S, IsAntichain (· ≤ ·) (A : Set α) ∧ A.card = antichainWidth S := by
+  classical
+  obtain ⟨A, hA, hAeq⟩ := Finset.exists_mem_eq_sup
+    (S.powerset.filter (fun A : Finset α => IsAntichain (· ≤ ·) (A : Set α)))
+    ⟨∅, Finset.mem_filter.2 ⟨Finset.empty_mem_powerset S, by simp⟩⟩ Finset.card
+  rw [Finset.mem_filter, Finset.mem_powerset] at hA
+  refine ⟨A, hA.1, hA.2, ?_⟩
+  unfold antichainWidth
+  convert hAeq.symm
+
+lemma antichainWidth_mono {S T : Finset α} (h : S ⊆ T) :
+    antichainWidth S ≤ antichainWidth T := by
+  obtain ⟨A, hAS, hA, hAc⟩ := exists_card_eq_antichainWidth S
+  exact hAc ▸ card_le_antichainWidth (hAS.trans h) hA
+
+/-- An antichain of size `k` meets every one of `k` chains covering the set. -/
+lemma exists_mem_label {S : Finset α} {c : α → ℕ} {k : ℕ} (hc : ∀ x ∈ S, c x < k)
+    (hch : ∀ i, IsChain (· ≤ ·) {x | x ∈ S ∧ c x = i}) {A : Finset α} (hAS : A ⊆ S)
+    (hA : IsAntichain (· ≤ ·) (A : Set α)) (hAk : A.card = k) :
+    ∀ i < k, ∃ y ∈ A, c y = i := by
+  classical
+  have hinj : Set.InjOn c A := by
+    intro x hx y hy hxy
+    by_contra hne
+    rcases hch (c x) ⟨hAS hx, rfl⟩ ⟨hAS hy, hxy.symm⟩ hne with h | h
+    · exact hA hx hy hne h
+    · exact hA hy hx (Ne.symm hne) h
+  have himg : A.image c = Finset.range k := by
+    refine Finset.eq_of_subset_of_card_le ?_ ?_
+    · intro z hz
+      rw [Finset.mem_image] at hz
+      obtain ⟨x, hx, rfl⟩ := hz
+      exact Finset.mem_range.2 (hc x (hAS hx))
+    · rw [Finset.card_image_of_injOn hinj, Finset.card_range, hAk]
+  intro i hi
+  have : i ∈ A.image c := himg ▸ Finset.mem_range.2 hi
+  simpa using this
+
+/-- Dilworth's theorem for a finite set `S`, in labelling form (Galvin's proof): `S` is covered by
+`antichainWidth S` chains, the `i`-th chain being the elements of `S` labelled `i`. -/
+theorem dilworth_finset (S : Finset α) : ∃ c : α → ℕ, (∀ x ∈ S, c x < antichainWidth S) ∧
+    ∀ i, IsChain (· ≤ ·) {x | x ∈ S ∧ c x = i} := by
+  classical
+  induction S using Finset.strongInduction with
+  | H S ih =>
+  rcases S.eq_empty_or_nonempty with rfl | hne
+  · refine ⟨fun _ => 0, by simp, fun i => ?_⟩
+    simp [IsChain]
+  obtain ⟨a, haS, hamax⟩ := Finset.exists_maximal hne
+  have hamax' : ∀ x ∈ S, a ≤ x → x = a := fun x hx hax => le_antisymm (hamax hx hax) hax
+  have : Nonempty α := ⟨a⟩
+  set S' := S.erase a with hS'
+  have hS'S : S' ⊆ S := Finset.erase_subset a S
+  obtain ⟨c', hc'lt, hc'ch⟩ := ih S' (Finset.erase_ssubset haS)
+  set k := antichainWidth S' with hk
+  have hD : ∀ i < k, ∃ x, (x ∈ S' ∧ c' x = i ∧ ∃ A ⊆ S', IsAntichain (· ≤ ·) (A : Set α) ∧
+      A.card = k ∧ x ∈ A) ∧ ∀ y, (y ∈ S' ∧ c' y = i ∧ ∃ A ⊆ S',
+        IsAntichain (· ≤ ·) (A : Set α) ∧ A.card = k ∧ y ∈ A) → y ≤ x := by
+    intro i hi
+    set D := S'.filter (fun y => c' y = i ∧ ∃ A ⊆ S', IsAntichain (· ≤ ·) (A : Set α) ∧
+      A.card = k ∧ y ∈ A) with hD
+    have hDne : D.Nonempty := by
+      obtain ⟨A, hAS, hA, hAk⟩ := exists_card_eq_antichainWidth S'
+      obtain ⟨y, hyA, hy⟩ := exists_mem_label hc'lt hc'ch hAS hA hAk i hi
+      exact ⟨y, Finset.mem_filter.2 ⟨hAS hyA, hy, A, hAS, hA, hAk, hyA⟩⟩
+    obtain ⟨x, hxD, hxmax⟩ := Finset.exists_maximal hDne
+    have hx := Finset.mem_filter.1 hxD
+    refine ⟨x, ⟨hx.1, hx.2⟩, fun y hy => ?_⟩
+    by_cases hxy : y = x
+    · exact le_of_eq hxy
+    rcases hc'ch i ⟨hy.1, hy.2.1⟩ ⟨hx.1, hx.2.1⟩ hxy with h | h
+    · exact h
+    · exact absurd (le_antisymm (hxmax (Finset.mem_filter.2 ⟨hy.1, hy.2⟩) h) h) hxy
+  choose! x hxD hxmax using hD
+  have hxinc : ∀ i < k, ∀ j < k, i ≠ j → ¬ x i ≤ x j := by
+    intro i hi j hj hij hle
+    obtain ⟨A, hAS, hA, hAk, hxjA⟩ := (hxD j hj).2.2
+    obtain ⟨y, hyA, hyi⟩ := exists_mem_label hc'lt hc'ch hAS hA hAk i hi
+    have hyx : y ≤ x i := hxmax i hi y ⟨hAS hyA, hyi, A, hAS, hA, hAk, hyA⟩
+    have hyne : y ≠ x j := by
+      intro h
+      apply hij
+      rw [← hyi, h, (hxD j hj).2.1]
+    exact hA hyA hxjA hyne (hyx.trans hle)
+  have hwS : k ≤ antichainWidth S := antichainWidth_mono hS'S
+  by_cases hcase : ∃ i < k, x i ≤ a
+  · obtain ⟨i, hi, hxa⟩ := hcase
+    set K := insert a (S'.filter (fun z => c' z = i ∧ z ≤ x i)) with hK
+    set T := S \ K with hT
+    have hTS' : T ⊆ S' := by
+      intro z hz
+      rw [hT, Finset.mem_sdiff, hK, Finset.mem_insert, not_or] at hz
+      exact Finset.mem_erase.2 ⟨hz.2.1, hz.1⟩
+    obtain ⟨c'', hc''lt, hc''ch⟩ := ih T (lt_of_le_of_lt hTS' (Finset.erase_ssubset haS))
+    have hwT : antichainWidth T < k := by
+      obtain ⟨B, hBT, hB, hBw⟩ := exists_card_eq_antichainWidth T
+      by_contra hge
+      push Not at hge
+      have hBS' : B ⊆ S' := hBT.trans hTS'
+      have hBk : B.card = k := le_antisymm (card_le_antichainWidth hBS' hB) (hBw ▸ hge)
+      obtain ⟨y, hyB, hyi⟩ := exists_mem_label hc'lt hc'ch hBS' hB hBk i hi
+      have hyx : y ≤ x i := hxmax i hi y ⟨hBS' hyB, hyi, B, hBS', hB, hBk, hyB⟩
+      have hyK : y ∈ K := Finset.mem_insert_of_mem (Finset.mem_filter.2 ⟨hBS' hyB, hyi, hyx⟩)
+      exact (Finset.mem_sdiff.1 (hBT hyB)).2 hyK
+    have hKch : ∀ z ∈ K, ∀ w ∈ K, z ≤ w ∨ w ≤ z := by
+      have hfil : ∀ z ∈ S'.filter (fun z => c' z = i ∧ z ≤ x i), z ≤ a := fun z hz =>
+        (Finset.mem_filter.1 hz).2.2.trans hxa
+      intro z hz w hw
+      rw [hK, Finset.mem_insert] at hz hw
+      rcases hz with rfl | hz <;> rcases hw with rfl | hw
+      · exact Or.inl le_rfl
+      · exact Or.inr (hfil w hw)
+      · exact Or.inl (hfil z hz)
+      · by_cases hzw : z = w
+        · exact Or.inl (le_of_eq hzw)
+        have hz' := Finset.mem_filter.1 hz
+        have hw' := Finset.mem_filter.1 hw
+        exact hc'ch i ⟨hz'.1, hz'.2.1⟩ ⟨hw'.1, hw'.2.1⟩ hzw
+    refine ⟨fun z => if z ∈ K then k - 1 else c'' z, ?_, ?_⟩
+    · intro z hz
+      by_cases hzK : z ∈ K
+      · simp only [hzK, ite_true]
+        omega
+      · simp only [hzK, ite_false]
+        have := hc''lt z (Finset.mem_sdiff.2 ⟨hz, hzK⟩)
+        omega
+    · intro j z hz w hw hne
+      simp only [Set.mem_ofPred_eq] at hz hw
+      by_cases hzK : z ∈ K <;> by_cases hwK : w ∈ K
+      · exact hKch z hzK w hwK
+      · simp only [hzK, hwK, ite_true, ite_false] at hz hw
+        have := hc''lt w (Finset.mem_sdiff.2 ⟨hw.1, hwK⟩)
+        omega
+      · simp only [hzK, hwK, ite_true, ite_false] at hz hw
+        have := hc''lt z (Finset.mem_sdiff.2 ⟨hz.1, hzK⟩)
+        omega
+      · simp only [hzK, hwK, ite_false] at hz hw
+        exact hc''ch j ⟨Finset.mem_sdiff.2 ⟨hz.1, hzK⟩, hz.2⟩
+          ⟨Finset.mem_sdiff.2 ⟨hw.1, hwK⟩, hw.2⟩ hne
+  · push Not at hcase
+    have hxS' : ∀ i < k, x i ∈ S' := fun i hi => (hxD i hi).1
+    set A := insert a ((Finset.range k).image x) with hA
+    have hinj : Set.InjOn x (Finset.range k) := by
+      intro i hi j hj hij
+      have hi' := Finset.mem_range.1 hi
+      have hj' := Finset.mem_range.1 hj
+      rw [← (hxD i hi').2.1, ← (hxD j hj').2.1, hij]
+    have haimg : a ∉ (Finset.range k).image x := by
+      intro h
+      rw [Finset.mem_image] at h
+      obtain ⟨i, hi, hia⟩ := h
+      have := hxS' i (Finset.mem_range.1 hi)
+      rw [hia, hS'] at this
+      simp at this
+    have hAcard : A.card = k + 1 := by
+      rw [hA, Finset.card_insert_of_notMem haimg, Finset.card_image_of_injOn hinj,
+        Finset.card_range]
+    have hAS : A ⊆ S := by
+      intro z hz
+      rw [hA, Finset.mem_insert, Finset.mem_image] at hz
+      rcases hz with rfl | ⟨i, hi, rfl⟩
+      · exact haS
+      · exact hS'S (hxS' i (Finset.mem_range.1 hi))
+    have hAanti : IsAntichain (· ≤ ·) (A : Set α) := by
+      rw [hA, Finset.coe_insert]
+      refine IsAntichain.insert ?_ ?_ ?_
+      · intro z hz w hw hne
+        simp only [Finset.coe_image, Finset.coe_range, Set.mem_image, Set.mem_Iio] at hz hw
+        obtain ⟨i, hi, rfl⟩ := hz
+        obtain ⟨j, hj, rfl⟩ := hw
+        exact hxinc i hi j hj (fun h => hne (h ▸ rfl))
+      · intro z hz _
+        simp only [Finset.coe_image, Finset.coe_range, Set.mem_image, Set.mem_Iio] at hz
+        obtain ⟨i, hi, rfl⟩ := hz
+        exact hcase i hi
+      · intro z hz hne hle
+        simp only [Finset.coe_image, Finset.coe_range, Set.mem_image, Set.mem_Iio] at hz
+        obtain ⟨i, hi, rfl⟩ := hz
+        exact hne (hamax' _ (hS'S (hxS' i hi)) hle).symm
+    have hwA : k + 1 ≤ antichainWidth S := hAcard ▸ card_le_antichainWidth hAS hAanti
+    refine ⟨fun z => if z = a then k else c' z, ?_, ?_⟩
+    · intro z hz
+      by_cases hza : z = a
+      · simp only [hza, ite_true]
+        omega
+      · simp only [hza, ite_false]
+        have := hc'lt z (Finset.mem_erase.2 ⟨hza, hz⟩)
+        omega
+    · intro j z hz w hw hne
+      simp only [Set.mem_ofPred_eq] at hz hw
+      by_cases hza : z = a <;> by_cases hwa : w = a
+      · exact absurd (hza.trans hwa.symm) hne
+      · simp only [hza, hwa, ite_true, ite_false] at hz hw
+        have := hc'lt w (Finset.mem_erase.2 ⟨hwa, hw.1⟩)
+        omega
+      · simp only [hza, hwa, ite_true, ite_false] at hz hw
+        have := hc'lt z (Finset.mem_erase.2 ⟨hza, hz.1⟩)
+        omega
+      · simp only [hza, hwa, ite_false] at hz hw
+        exact hc'ch j ⟨Finset.mem_erase.2 ⟨hza, hz.1⟩, hz.2⟩
+          ⟨Finset.mem_erase.2 ⟨hwa, hw.1⟩, hw.2⟩ hne
+
+end
+
+/-- **Dilworth's theorem (1950).** A finite poset has an antichain `A` and a partition into `|A|`
+chains. -/
+theorem dilworth {α : Type*} [PartialOrder α] [Finite α] :
+    ∃ A : Finset α, IsAntichain (· ≤ ·) (A : Set α) ∧
+      ∃ c : α → Fin A.card, ∀ i, IsChain (· ≤ ·) {x | c x = i} := by
+  classical
+  have := Fintype.ofFinite α
+  obtain ⟨c, hclt, hcch⟩ := dilworth_finset (Finset.univ : Finset α)
+  obtain ⟨A, -, hA, hAc⟩ := exists_card_eq_antichainWidth (Finset.univ : Finset α)
+  refine ⟨A, hA, fun x => ⟨c x, hAc ▸ hclt x (Finset.mem_univ x)⟩, fun i => ?_⟩
+  refine (hcch i).mono ?_
+  intro x hx
+  simp only [Set.mem_ofPred_eq, Fin.ext_iff] at hx ⊢
+  exact ⟨Finset.mem_univ x, hx⟩
+
+/-- **Mirsky's theorem (1971).** A finite poset has a chain `C` and a partition into `|C|`
+antichains. -/
+theorem mirsky {α : Type*} [PartialOrder α] [Finite α] :
+    ∃ C : Finset α, IsChain (· ≤ ·) (C : Set α) ∧
+      ∃ c : α → Fin C.card, ∀ i, IsAntichain (· ≤ ·) {x | c x = i} := by
+  classical
+  have := Fintype.ofFinite α
+  set chains : Finset (Finset α) :=
+    Finset.univ.filter (fun C : Finset α => IsChain (· ≤ ·) (C : Set α)) with hchains
+  obtain ⟨C₀, hC₀, hmax⟩ := chains.exists_max_image Finset.card
+    ⟨∅, Finset.mem_filter.2 ⟨Finset.mem_univ _, by simp⟩⟩
+  set top : α → Finset (Finset α) :=
+    fun x => chains.filter (fun C => x ∈ C ∧ ∀ y ∈ C, y ≤ x) with htop
+  set h : α → ℕ := fun x => (top x).sup Finset.card with hh
+  have hsing : ∀ x, {x} ∈ top x := fun x => by
+    simp [htop, hchains]
+  have h_ge : ∀ x, 1 ≤ h x := fun x => by
+    have := Finset.le_sup (f := Finset.card) (hsing x)
+    rw [Finset.card_singleton] at this
+    exact this
+  have h_le : ∀ x, h x ≤ C₀.card := fun x =>
+    Finset.sup_le fun C hC => hmax C (Finset.mem_filter.1 hC).1
+  have h_mono : ∀ x y, x < y → h x < h y := by
+    intro x y hxy
+    obtain ⟨C, hC, hCc⟩ := Finset.exists_mem_eq_sup (top x) ⟨{x}, hsing x⟩ Finset.card
+    have hC' := Finset.mem_filter.1 hC
+    have hCch : IsChain (· ≤ ·) (C : Set α) := (Finset.mem_filter.1 hC'.1).2
+    have hyC : y ∉ C := fun hy => (hC'.2.2 y hy).not_gt hxy
+    have hmem : insert y C ∈ top y := by
+      refine Finset.mem_filter.2 ⟨Finset.mem_filter.2 ⟨Finset.mem_univ _, ?_⟩,
+        Finset.mem_insert_self y C, ?_⟩
+      · rw [Finset.coe_insert]
+        exact hCch.insert fun b hb _ => Or.inr ((hC'.2.2 b hb).trans hxy.le)
+      · intro z hz
+        rw [Finset.mem_insert] at hz
+        rcases hz with rfl | hz
+        · exact le_rfl
+        · exact (hC'.2.2 z hz).trans hxy.le
+    have := Finset.le_sup (f := Finset.card) hmem
+    rw [Finset.card_insert_of_notMem hyC] at this
+    change (top x).sup Finset.card < (top y).sup Finset.card
+    omega
+  refine ⟨C₀, (Finset.mem_filter.1 hC₀).2,
+    fun x => ⟨h x - 1, by have := h_ge x; have := h_le x; omega⟩, fun i => ?_⟩
+  intro x hx y hy hne hle
+  simp only [Set.mem_ofPred_eq, Fin.ext_iff] at hx hy
+  have := h_mono x y (lt_of_le_of_ne hle hne)
+  have := h_ge x
+  have := h_ge y
+  omega
+
+end Konig.Poset
diff --git a/LeanPool/ClassicalMatchingFactors/Regular/BalancedOrientation.lean b/LeanPool/ClassicalMatchingFactors/Regular/BalancedOrientation.lean
new file mode 100644
index 000000000..2b30f1c7a
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Regular/BalancedOrientation.lean
@@ -0,0 +1,188 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import LeanPool.ClassicalMatchingFactors.Regular.EulerTrail
+
+/-!
+
+Imported from [jtraverso/euler-petersen](https://github.com/jtraverso/euler-petersen/blob/02c3f1a5327c5f066938860bb07e9fce226b36ca/Euler/Orientation.lean), registered as PALOMAR-2026-10-16-000016. The original proof is retained; module paths and imports are adapted for this collection.
+
+# Orientaciones eulerianas
+
+Todo grafo finito cuyos vértices tienen grado par admite una orientación *balanceada*: cada
+vértice tiene tantos arcos salientes como entrantes.
+
+La prueba reutiliza la maquinaria del teorema de Euler (`exists_closed_trail_avoiding`): se
+descomponen las aristas en trails cerrados disjuntos, agregando uno a la vez, y cada trail
+cerrado, recorrido en su sentido, aporta lo mismo a los grados de entrada y de salida.
+
+Representamos una orientación por un conjunto de dardos `Ds : Finset G.Dart` que contiene
+exactamente un dardo por arista.
+-/
+
+@[expose] public section
+
+namespace SimpleGraph
+
+open Walk Finset
+
+variable {V : Type*} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj]
+
+omit [Fintype V] [DecidableRel G.Adj] in
+/-- En un paseo de `u` a `w`, los dardos que salen de `v` y los que entran a `v` difieren sólo
+en los extremos. -/
+lemma Walk.countP_darts_fst_add {u w : V} (p : G.Walk u w) (v : V) :
+    p.darts.countP (fun d => d.fst = v) + (if w = v then 1 else 0) =
+      p.darts.countP (fun d => d.snd = v) + (if u = v then 1 else 0) := by
+  induction p with
+  | nil => simp
+  | cons h q ih =>
+    rename_i a b c
+    simp only [darts_cons, List.countP_cons]
+    have := ih
+    by_cases hav : a = v <;> by_cases hbv : b = v <;> simp_all <;> omega
+
+omit [Fintype V] [DecidableRel G.Adj] in
+/-- En un paseo cerrado salen de cada vértice tantos dardos como entran. -/
+lemma Walk.countP_darts_fst_eq {u : V} (p : G.Walk u u) (v : V) :
+    p.darts.countP (fun d => d.fst = v) = p.darts.countP (fun d => d.snd = v) := by
+  have := p.countP_darts_fst_add v
+  omega
+
+/-- `Ds` contiene a lo más un dardo por arista. -/
+def EdgeInj (Ds : Finset G.Dart) : Prop :=
+  ∀ d ∈ Ds, ∀ d' ∈ Ds, d.edge = d'.edge → d = d'
+
+/-- `Ds` es balanceado: en cada vértice salen tantos dardos como entran. -/
+def Balanced (Ds : Finset G.Dart) : Prop :=
+  ∀ v, (Ds.filter fun d => d.fst = v).card = (Ds.filter fun d => d.snd = v).card
+
+lemma card_filter_toFinset_of_nodup {α : Type*} [DecidableEq α] {l : List α} (hl : l.Nodup)
+    (p : α → Prop) [DecidablePred p] : (l.toFinset.filter p).card = l.countP p := by
+  rw [List.countP_eq_length_filter, ← List.toFinset_card_of_nodup (hl.filter _)]
+  congr 1
+  ext a
+  simp
+
+omit [Fintype V] [DecidableRel G.Adj] in
+/-- Las aristas de un conjunto de dardos con a lo más un dardo por arista, contadas en `v`. -/
+lemma card_image_edge_filter {Ds : Finset G.Dart} (hinj : EdgeInj Ds) (v : V) :
+    ((Ds.image Dart.edge).filter (v ∈ ·)).card =
+      (Ds.filter fun d => d.fst = v).card + (Ds.filter fun d => d.snd = v).card := by
+  have h1 : (Ds.image Dart.edge).filter (v ∈ ·) =
+      (Ds.filter fun d => v ∈ d.edge).image Dart.edge := by
+    ext e
+    simp only [mem_filter, mem_image]
+    constructor
+    · rintro ⟨⟨a, ha, rfl⟩, hv⟩; exact ⟨a, ⟨ha, hv⟩, rfl⟩
+    · rintro ⟨a, ⟨ha, hv⟩, rfl⟩; exact ⟨⟨a, ha, rfl⟩, hv⟩
+  rw [h1, card_image_of_injOn fun d hd d' hd' h =>
+    hinj d (mem_filter.mp hd).1 d' (mem_filter.mp hd').1 h]
+  have h2 : (Ds.filter fun d => v ∈ d.edge) =
+      (Ds.filter fun d => d.fst = v) ∪ (Ds.filter fun d => d.snd = v) := by
+    ext d
+    simp only [mem_filter, mem_union, Dart.edge, Sym2.mem_iff]
+    constructor
+    · rintro ⟨hd, h | h⟩
+      · exact Or.inl ⟨hd, h.symm⟩
+      · exact Or.inr ⟨hd, h.symm⟩
+    · rintro (⟨hd, h⟩ | ⟨hd, h⟩)
+      · exact ⟨hd, Or.inl h.symm⟩
+      · exact ⟨hd, Or.inr h.symm⟩
+  rw [h2, card_union_of_disjoint]
+  rw [Finset.disjoint_left]
+  intro d h1 h2
+  rw [mem_filter] at h1 h2
+  exact d.adj.ne (h1.2.trans h2.2.symm)
+
+/-- Paso: si `Ds` no cubre todas las aristas, se agrega un trail cerrado. -/
+lemma exists_larger_balanced (heven : ∀ v, Even (G.degree v)) {Ds : Finset G.Dart}
+    (hinj : EdgeInj Ds) (hbal : Balanced Ds) {x y₀ : V} (hxy : G.Adj x y₀)
+    (hnot : ∀ d ∈ Ds, d.edge ≠ s(x, y₀)) :
+    ∃ Ds' : Finset G.Dart, EdgeInj Ds' ∧ Balanced Ds' ∧ Ds ⊆ Ds' ∧ Ds.card < Ds'.card := by
+  set S := (Ds.image Dart.edge).toList
+  have hSnd : S.Nodup := nodup_toList _
+  have hSsub : ∀ e ∈ S, e ∈ G.edgeSet := by
+    intro e he
+    rw [mem_toList, mem_image] at he
+    obtain ⟨d, -, rfl⟩ := he
+    exact d.edge_mem
+  have hpar : ∀ y, Even (S.countP fun e => y ∈ e) ↔ Even (G.degree y) := by
+    intro y
+    refine iff_of_true ?_ (heven y)
+    rw [← card_filter_toFinset_of_nodup hSnd, toList_toFinset, card_image_edge_filter hinj,
+      hbal y]
+    exact ⟨_, rfl⟩
+  have hnotS : s(x, y₀) ∉ S := by
+    rw [mem_toList, mem_image]
+    rintro ⟨d, hd, he⟩
+    exact hnot d hd he
+  obtain ⟨c, hc, hcpos, hcdisj⟩ := exists_closed_trail_avoiding hSnd hSsub hpar hxy hnotS
+  have hdnd : c.darts.Nodup := List.Nodup.of_map Dart.edge hc.edges_nodup
+  have hdisj : Disjoint Ds c.darts.toFinset := by
+    rw [Finset.disjoint_left]
+    intro d hd hdc
+    have : d.edge ∈ c.edges := by
+      rw [edges_eq_map_darts]; exact List.mem_map_of_mem (List.mem_toFinset.mp hdc)
+    exact hcdisj _ this (by rw [mem_toList]; exact mem_image_of_mem _ hd)
+  refine ⟨Ds ∪ c.darts.toFinset, ?_, ?_, subset_union_left, ?_⟩
+  · intro d hd d' hd' he
+    rcases mem_union.mp hd with hd | hd <;> rcases mem_union.mp hd' with hd' | hd'
+    · exact hinj d hd d' hd' he
+    · exfalso
+      have : d'.edge ∈ c.edges := by
+        rw [edges_eq_map_darts]; exact List.mem_map_of_mem (List.mem_toFinset.mp hd')
+      exact hcdisj _ this (by rw [mem_toList, ← he]; exact mem_image_of_mem _ hd)
+    · exfalso
+      have : d.edge ∈ c.edges := by
+        rw [edges_eq_map_darts]; exact List.mem_map_of_mem (List.mem_toFinset.mp hd)
+      exact hcdisj _ this (by rw [mem_toList, he]; exact mem_image_of_mem _ hd')
+    · exact List.inj_on_of_nodup_map (by rw [← edges_eq_map_darts]; exact hc.edges_nodup)
+        (List.mem_toFinset.mp hd) (List.mem_toFinset.mp hd') he
+  · intro v
+    rw [filter_union, filter_union, card_union_of_disjoint (disjoint_filter_filter hdisj),
+      card_union_of_disjoint (disjoint_filter_filter hdisj), hbal v,
+      card_filter_toFinset_of_nodup hdnd, card_filter_toFinset_of_nodup hdnd,
+      c.countP_darts_fst_eq v]
+  · rw [card_union_of_disjoint hdisj, List.toFinset_card_of_nodup hdnd, length_darts]
+    omega
+
+omit [DecidableEq V] in
+/-- Un conjunto de dardos con a lo más un dardo por arista tiene a lo más `|E|` elementos. -/
+lemma card_le_of_edgeInj {Ds : Finset G.Dart} (hinj : EdgeInj Ds) :
+    Ds.card ≤ G.edgeFinset.card := by
+  classical
+  rw [← card_image_of_injOn fun d hd d' hd' h => hinj d hd d' hd' h]
+  refine card_le_card fun e he => ?_
+  obtain ⟨d, -, rfl⟩ := mem_image.mp he
+  rw [mem_edgeFinset]
+  exact d.edge_mem
+
+/-- **Orientación euleriana.** Si todos los grados son pares, existe un conjunto de dardos con
+exactamente un dardo por arista, balanceado en cada vértice. -/
+theorem exists_balanced_orientation (heven : ∀ v, Even (G.degree v)) :
+    ∃ Ds : Finset G.Dart, EdgeInj Ds ∧ Balanced Ds ∧
+      ∀ e ∈ G.edgeSet, ∃ d ∈ Ds, d.edge = e := by
+  suffices key : ∀ n, ∀ Ds : Finset G.Dart, EdgeInj Ds → Balanced Ds →
+      G.edgeFinset.card - Ds.card = n → ∃ Ds' : Finset G.Dart, EdgeInj Ds' ∧ Balanced Ds' ∧
+        ∀ e ∈ G.edgeSet, ∃ d ∈ Ds', d.edge = e by
+    exact key _ ∅ (by simp [EdgeInj]) (by simp [Balanced]) rfl
+  intro n
+  induction n using Nat.strong_induction_on with
+  | _ n ih =>
+  intro Ds hinj hbal hn
+  by_cases hcov : ∀ e ∈ G.edgeSet, ∃ d ∈ Ds, d.edge = e
+  · exact ⟨Ds, hinj, hbal, hcov⟩
+  push Not at hcov
+  obtain ⟨e, he, hnot⟩ := hcov
+  induction e using Sym2.ind with
+  | _ x y₀ =>
+  obtain ⟨Ds', hinj', hbal', -, hlt⟩ := exists_larger_balanced heven hinj hbal he hnot
+  have h1 := card_le_of_edgeInj hinj'
+  exact ih _ (by omega) Ds' hinj' hbal' rfl
+
+end SimpleGraph
diff --git a/LeanPool/ClassicalMatchingFactors/Regular/EulerCircuit.lean b/LeanPool/ClassicalMatchingFactors/Regular/EulerCircuit.lean
new file mode 100644
index 000000000..f2ec5e708
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Regular/EulerCircuit.lean
@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import LeanPool.ClassicalMatchingFactors.Regular.EulerTrail
+
+/-!
+# Eulerian circuit compatibility import
+
+The circuit theorems originally imported from
+[jtraverso/euler-petersen](https://github.com/jtraverso/euler-petersen/blob/02c3f1a5327c5f066938860bb07e9fce226b36ca/Euler/Basic.lean),
+registered as PALOMAR-2026-10-16-000016, are publicly re-exported here.
+Their shared helpers and proofs are in `EulerTrail`, where circuit existence is
+now a corollary of the prescribed-start parity theorem. Both original import paths
+and the circuit and trail declaration names remain available.
+-/
diff --git a/LeanPool/ClassicalMatchingFactors/Regular/EulerTrail.lean b/LeanPool/ClassicalMatchingFactors/Regular/EulerTrail.lean
new file mode 100644
index 000000000..583f869ba
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Regular/EulerTrail.lean
@@ -0,0 +1,267 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Trails
+public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
+public import Mathlib.Combinatorics.SimpleGraph.Finite
+
+/-!
+
+Imported from [jtraverso/euler-petersen](https://github.com/jtraverso/euler-petersen/blob/02c3f1a5327c5f066938860bb07e9fce226b36ca/Euler/Trail.lean), registered as PALOMAR-2026-10-16-000016. The parity proof is retained, with shared circuit helpers and compatibility results consolidated here to avoid parallel circuit-existence proofs.
+
+# Circuitos y caminos eulerianos
+
+Un grafo finito conexo admite un trail euleriano (camino que recorre cada arista exactamente una
+vez, no necesariamente cerrado) si y sólo si tiene 0 ó 2 vértices de grado impar. Más
+precisamente, si los vértices de grado impar son exactamente `a` y `b` (`a ≠ b`), hay un trail
+euleriano de `a` a `b`; si no hay vértices de grado impar, hay un circuito euleriano por
+cualquier vértice.
+
+Mathlib contiene la dirección necesaria (`SimpleGraph.Walk.IsEulerian.card_odd_degree`); aquí
+probamos la suficiencia (el TODO de `Mathlib/Combinatorics/SimpleGraph/Trails.lean`).
+
+## Estrategia
+
+Fijamos `a, b` con la condición de paridad
+`Even (deg x) ↔ (a ≠ b → x ≠ a ∧ x ≠ b)` (la misma que satisface un trail de `a` a `b`).
+Tomamos un trail `p : a → b` de longitud máxima. Si no es euleriano, por conexidad hay un vértice
+`x` de `p` con una arista libre. Las aristas de `p` tienen, en cada vértice, la misma paridad que
+el grado, así que en el grafo de aristas no usadas todos los grados son pares; de ahí sale un
+trail cerrado `c` en `x`, de longitud positiva, disjunto de `p`. Insertando `c` en `p` en `x`
+se obtiene un trail `a → b` más largo: contradicción.
+-/
+
+@[expose] public section
+
+namespace SimpleGraph
+
+open Walk
+
+variable {V : Type*} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj]
+
+/-- Si una lista sin repeticiones de aristas contiene todas las aristas en `x`, el número de
+sus aristas incidentes en `x` es `deg x`. -/
+lemma countP_eq_degree_of_forall_adj_mem {L : List (Sym2 V)} (hL : L.Nodup)
+    (hsub : ∀ e ∈ L, e ∈ G.edgeSet) {x : V} (h : ∀ y, G.Adj x y → s(x, y) ∈ L) :
+    L.countP (fun e => x ∈ e) = G.degree x := by
+  have hinc : G.incidenceFinset x = (⟨(L : Multiset (Sym2 V)), hL⟩ : Finset _).filter (x ∈ ·) := by
+    ext e
+    simp only [mem_incidenceFinset, incidenceSet, Set.mem_ofPred_eq, Finset.mem_filter]
+    constructor
+    · rintro ⟨he, hxe⟩
+      obtain ⟨y, rfl⟩ := Sym2.mem_iff_exists.mp hxe
+      exact ⟨h y he, hxe⟩
+    · rintro ⟨hm, hxe⟩
+      exact ⟨hsub _ hm, hxe⟩
+  rw [← card_incidenceFinset_eq_degree, hinc, ← Multiset.coe_countP,
+    Multiset.countP_eq_card_filter]
+  rfl
+
+/-- Si una lista sin repeticiones de aristas no tiene `deg x` aristas en `x`, falta alguna
+arista en `x`. -/
+lemma exists_adj_not_mem_of_countP_ne {L : List (Sym2 V)} (hL : L.Nodup)
+    (hsub : ∀ e ∈ L, e ∈ G.edgeSet) {x : V} (h : L.countP (fun e => x ∈ e) ≠ G.degree x) :
+    ∃ y, G.Adj x y ∧ s(x, y) ∉ L := by
+  by_contra! h'
+  exact h (countP_eq_degree_of_forall_adj_mem hL hsub h')
+
+/-- Si el número de aristas de un trail incidentes en `x` no tiene la paridad de `deg x`,
+hay una arista en `x` que el trail no usa. -/
+lemma exists_adj_not_mem_edges_of_not_even {u v x : V} {p : G.Walk u v} (hp : p.IsTrail)
+    (hx : Even (G.degree x)) (hodd : ¬ Even (p.edges.countP fun e => x ∈ e)) :
+    ∃ y, G.Adj x y ∧ s(x, y) ∉ p.edges := by
+  apply exists_adj_not_mem_of_countP_ne hp.edges_nodup (fun e he => p.edges_subset_edgeSet he)
+  intro hcount
+  apply hodd
+  rwa [hcount]
+
+omit [Fintype V] [DecidableRel G.Adj] in
+/-- En un grafo conexo, si un trail no es euleriano, algún vértice del trail tiene
+una arista que el trail no usa. -/
+lemma exists_mem_support_adj_not_mem_edges (hconn : G.Connected) {u v : V} {p : G.Walk u v}
+    (hp : p.IsTrail) (hne : ¬ p.IsEulerian) :
+    ∃ x ∈ p.support, ∃ y, G.Adj x y ∧ s(x, y) ∉ p.edges := by
+  by_contra! h
+  apply hne
+  -- Todo vértice alcanzable desde el soporte está en el soporte.
+  have hclosed : ∀ a b (q : G.Walk a b), a ∈ p.support → b ∈ p.support := by
+    intro a b q
+    induction q with
+    | nil => exact id
+    | cons hab q ih =>
+      intro ha
+      exact ih (p.snd_mem_support_of_mem_edges (h _ ha _ hab))
+  have hall : ∀ w, w ∈ p.support := fun w =>
+    hclosed u w (hconn.preconnected u w).some p.start_mem_support
+  refine hp.isEulerian_of_forall_mem fun e he => ?_
+  induction e using Sym2.ind with
+  | _ a b => exact h a (hall a) b he
+
+/-- Sea `S` una lista de aristas que en cada vértice tiene la paridad del grado. Si `x` tiene
+una arista fuera de `S`, existe un trail cerrado en `x`, de longitud positiva, que no usa
+aristas de `S`. -/
+lemma exists_closed_trail_avoiding {S : List (Sym2 V)} (hS : S.Nodup)
+    (hSsub : ∀ e ∈ S, e ∈ G.edgeSet)
+    (hpar : ∀ y, Even (S.countP fun e => y ∈ e) ↔ Even (G.degree y))
+    {x y₀ : V} (hxy : G.Adj x y₀) (hnot : s(x, y₀) ∉ S) :
+    ∃ c : G.Walk x x, c.IsTrail ∧ 0 < c.length ∧ ∀ e ∈ c.edges, e ∉ S := by
+  by_contra hno
+  have key : ∀ k : ℕ, ∃ v, ∃ q : G.Walk x v,
+      q.IsTrail ∧ 0 < q.length ∧ (∀ e ∈ q.edges, e ∉ S) ∧ k ≤ q.length := by
+    intro k
+    induction k with
+    | zero => exact ⟨y₀, cons hxy nil, by simp, by simp, by simpa using hnot, by simp⟩
+    | succ k ih =>
+      obtain ⟨v, q, hq, hpos, hdisj, hk⟩ := ih
+      by_cases hv : v = x
+      · subst hv
+        exact absurd ⟨q, hq, hpos, hdisj⟩ hno
+      have hqodd : ¬ Even (q.edges.countP fun e => v ∈ e) := by
+        rw [hq.even_countP_edges_iff]
+        simp [Ne.symm hv]
+      have hnd : (S ++ q.edges).Nodup :=
+        List.nodup_append.mpr ⟨hS, hq.edges_nodup, fun a ha b hb hab => hdisj b hb (hab ▸ ha)⟩
+      have hsub : ∀ e ∈ S ++ q.edges, e ∈ G.edgeSet := by
+        intro e he
+        rcases List.mem_append.mp he with he | he
+        · exact hSsub e he
+        · exact q.edges_subset_edgeSet he
+      have hne : (S ++ q.edges).countP (fun e => v ∈ e) ≠ G.degree v := by
+        intro heq
+        have := hpar v
+        rw [← heq, List.countP_append, Nat.even_add] at this
+        tauto
+      obtain ⟨w, hvw, hw⟩ := exists_adj_not_mem_of_countP_ne hnd hsub hne
+      rw [List.mem_append, not_or] at hw
+      refine ⟨w, (cons hvw.symm q.reverse).reverse, ?_, ?_, ?_, ?_⟩
+      · refine ((isTrail_cons _ _).mpr ⟨hq.reverse, ?_⟩).reverse
+        rw [edges_reverse, List.mem_reverse, Sym2.eq_swap]
+        exact hw.2
+      · simp
+      · intro e he
+        simp only [edges_reverse, edges_cons, List.reverse_cons, List.reverse_reverse,
+          List.mem_append, List.mem_singleton] at he
+        rcases he with he | rfl
+        · exact hdisj e he
+        · rw [Sym2.eq_swap]
+          exact hw.1
+      · simp
+        omega
+  obtain ⟨v, q, hq, -, -, hk⟩ := key (G.edgeFinset.card + 1)
+  have := hq.length_le_card_edgeFinset
+  omega
+
+/-- **Euler (suficiencia, versión con extremos).** Si `G` es conexo y los vértices de grado
+impar son exactamente `a` y `b` (o no hay ninguno, cuando `a = b`), existe un trail euleriano
+de `a` a `b`. -/
+theorem exists_isEulerian_of_parity (hconn : G.Connected) {a b : V}
+    (h : ∀ x, Even (G.degree x) ↔ (a ≠ b → x ≠ a ∧ x ≠ b)) :
+    ∃ p : G.Walk a b, p.IsEulerian := by
+  by_contra hno
+  -- Todo trail `a → b` se extiende a uno más largo.
+  have ext : ∀ p : G.Walk a b, p.IsTrail → ∃ q : G.Walk a b, q.IsTrail ∧ p.length < q.length := by
+    intro p hp
+    obtain ⟨x, hx, y, hxy, hnot⟩ :=
+      exists_mem_support_adj_not_mem_edges hconn hp fun he => hno ⟨p, he⟩
+    have hpar : ∀ z, Even (p.edges.countP fun e => z ∈ e) ↔ Even (G.degree z) := fun z => by
+      rw [hp.even_countP_edges_iff, h]
+    obtain ⟨c, hc, hcpos, hcdisj⟩ := exists_closed_trail_avoiding hp.edges_nodup
+      (fun e he => p.edges_subset_edgeSet he) hpar hxy hnot
+    have hedges : p.edges = (p.takeUntil x hx).edges ++ (p.dropUntil x hx).edges := by
+      rw [← edges_append, p.take_spec hx]
+    have hlen : p.length = (p.takeUntil x hx).length + (p.dropUntil x hx).length := by
+      rw [← length_append, p.take_spec hx]
+    refine ⟨(p.takeUntil x hx).append (c.append (p.dropUntil x hx)), ?_, ?_⟩
+    · have hperm : List.Perm ((p.takeUntil x hx).edges ++ (c.edges ++ (p.dropUntil x hx).edges))
+          (c.edges ++ p.edges) := by
+        rw [hedges, ← List.append_assoc, ← List.append_assoc]
+        exact List.perm_append_comm.append_right _
+      rw [isTrail_def, edges_append, edges_append, hperm.nodup_iff]
+      exact List.nodup_append.mpr
+        ⟨hc.edges_nodup, hp.edges_nodup, fun e he e' he' hee => hcdisj e he (hee ▸ he')⟩
+    · rw [length_append, length_append]
+      omega
+  -- Existe algún trail `a → b`.
+  have h0 : ∃ p : G.Walk a b, p.IsTrail := by
+    obtain ⟨q⟩ := hconn.preconnected a b
+    exact ⟨q.bypass, q.bypass_isPath.isTrail⟩
+  have key : ∀ k : ℕ, ∃ q : G.Walk a b, q.IsTrail ∧ k ≤ q.length := by
+    intro k
+    induction k with
+    | zero =>
+      obtain ⟨p, hp⟩ := h0
+      exact ⟨p, hp, Nat.zero_le _⟩
+    | succ k ih =>
+      obtain ⟨q, hq, hk⟩ := ih
+      obtain ⟨q', hq', hlt⟩ := ext q hq
+      exact ⟨q', hq', by omega⟩
+  obtain ⟨q, hq, hk⟩ := key (G.edgeFinset.card + 1)
+  have := hq.length_le_card_edgeFinset
+  omega
+
+/-- En un grafo conexo con todos los grados pares hay un circuito euleriano que pasa por
+cualquier vértice prefijado. -/
+theorem exists_isEulerian_circuit_at (hconn : G.Connected) (heven : ∀ v, Even (G.degree v))
+    (a : V) : ∃ p : G.Walk a a, p.IsEulerian :=
+  exists_isEulerian_of_parity hconn fun x => iff_of_true (heven x) fun h => absurd rfl h
+
+/-- **Euler (suficiencia).** Un grafo finito conexo con todos sus grados pares admite un
+circuito euleriano. -/
+theorem exists_isEulerian_of_forall_even_degree (hconn : G.Connected)
+    (heven : ∀ v, Even (G.degree v)) : ∃ u, ∃ p : G.Walk u u, p.IsEulerian := by
+  obtain ⟨u⟩ := hconn.nonempty
+  obtain ⟨p, hp⟩ := exists_isEulerian_circuit_at hconn heven u
+  exact ⟨u, p, hp⟩
+
+/-- **Teorema de Euler.** Un grafo finito conexo admite un circuito euleriano si y sólo si
+todos sus vértices tienen grado par. -/
+theorem exists_isEulerian_iff_forall_even_degree (hconn : G.Connected) :
+    (∃ u, ∃ p : G.Walk u u, p.IsEulerian) ↔ ∀ v, Even (G.degree v) := by
+  constructor
+  · rintro ⟨u, p, hp⟩ v
+    exact hp.even_degree_iff.mpr fun h => absurd rfl h
+  · exact exists_isEulerian_of_forall_even_degree hconn
+
+/-- Compatibility form of circuit existence, with the original trail-extension conclusion. -/
+lemma exists_isEulerian_or_longer_trail (hconn : G.Connected)
+    (heven : ∀ v, Even (G.degree v)) {u v : V} (p : G.Walk u v) (_hp : p.IsTrail) :
+    (∃ w, ∃ q : G.Walk w w, q.IsEulerian) ∨
+      ∃ a b, ∃ q : G.Walk a b, q.IsTrail ∧ p.length < q.length := by
+  exact Or.inl (exists_isEulerian_of_forall_even_degree hconn heven)
+
+/-- **Teorema de Euler (trails).** Un grafo finito conexo admite un trail euleriano si y sólo
+si tiene 0 ó 2 vértices de grado impar. -/
+theorem exists_isEulerian_walk_iff (hconn : G.Connected) :
+    (∃ u v, ∃ p : G.Walk u v, p.IsEulerian) ↔
+      Fintype.card {v | Odd (G.degree v)} = 0 ∨ Fintype.card {v | Odd (G.degree v)} = 2 := by
+  constructor
+  · rintro ⟨u, v, p, hp⟩
+    exact hp.card_odd_degree
+  · intro hcard
+    rw [← Set.toFinset_card, Set.toFinset_ofPred] at hcard
+    rcases hcard with h0 | h2
+    · obtain ⟨a⟩ := hconn.nonempty
+      rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff] at h0
+      exact ⟨a, a, exists_isEulerian_circuit_at hconn
+        (fun x => Nat.not_odd_iff_even.mp (h0 (Finset.mem_univ x))) a⟩
+    · obtain ⟨a, b, hab, hs⟩ := Finset.card_eq_two.mp h2
+      refine ⟨a, b, exists_isEulerian_of_parity hconn fun x => ?_⟩
+      have hx := Finset.ext_iff.mp hs x
+      simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_insert,
+        Finset.mem_singleton] at hx
+      rw [← Nat.not_odd_iff_even, hx]
+      simp [hab, not_or]
+
+/-- Versión con extremos explícitos: si los únicos vértices de grado impar son `a ≠ b`, hay un
+trail euleriano de `a` a `b`. -/
+theorem exists_isEulerian_of_odd_iff (hconn : G.Connected) {a b : V} (hab : a ≠ b)
+    (hodd : ∀ x, Odd (G.degree x) ↔ x = a ∨ x = b) : ∃ p : G.Walk a b, p.IsEulerian :=
+  exists_isEulerian_of_parity hconn fun x => by
+    rw [← Nat.not_odd_iff_even, hodd]
+    simp [hab, not_or]
+
+end SimpleGraph
diff --git a/LeanPool/ClassicalMatchingFactors/Regular/TwoFactors.lean b/LeanPool/ClassicalMatchingFactors/Regular/TwoFactors.lean
new file mode 100644
index 000000000..751bd9dcb
--- /dev/null
+++ b/LeanPool/ClassicalMatchingFactors/Regular/TwoFactors.lean
@@ -0,0 +1,296 @@
+/-
+Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Pablo Traverso Gianini
+-/
+module
+
+public import LeanPool.ClassicalMatchingFactors.Regular.BalancedOrientation
+public import Mathlib.Combinatorics.Hall.Basic
+public import Mathlib.Data.Set.Card
+
+/-!
+
+Imported from [jtraverso/euler-petersen](https://github.com/jtraverso/euler-petersen/blob/02c3f1a5327c5f066938860bb07e9fce226b36ca/Euler/Petersen.lean), registered as PALOMAR-2026-10-16-000016. The original proof is retained; module paths and imports are adapted for this collection.
+
+# Teorema del 2-factor de Petersen (1891)
+
+Todo grafo finito `2k`-regular es unión disjunta (en aristas) de `k` 2-factores, es decir, de `k`
+subgrafos generadores en los que cada vértice tiene grado exactamente `2`.
+
+Prueba clásica:
+1. **Euler**: por la orientación euleriana (`exists_balanced_orientation`, que descompone el grafo
+   en trails cerrados), cada vértice tiene `k` arcos salientes y `k` entrantes.
+2. **Hall**: un digrafo con `k ≥ 1` arcos salientes y entrantes en cada vértice contiene una
+   permutación `σ` (es decir, `v → σ v` es un arco para todo `v`); quitándola queda un digrafo
+   `(k-1)`-regular, y así los arcos se parten en `k` permutaciones.
+3. Cada permutación `σ` da un 2-factor: los vecinos de `v` son `σ v` y `σ⁻¹ v`, distintos porque
+   la orientación nunca contiene a la vez `v → w` y `w → v`.
+
+Referencia: J. Petersen, *Die Theorie der regulären graphs*, Acta Math. 15 (1891) 193–220.
+-/
+
+@[expose] public section
+
+namespace SimpleGraph
+
+open Finset
+
+variable {V : Type*} [Fintype V] [DecidableEq V]
+
+/-! ### Permutaciones en digrafos regulares (Hall) -/
+
+omit [Fintype V] in
+/-- **Hall para digrafos regulares.** Si cada vértice tiene `k ≥ 1` arcos salientes y `k`
+entrantes en `D`, existe una permutación `σ` con `(v, σ v) ∈ D` para todo `v`. -/
+theorem exists_perm_subset [Finite V] {D : Finset (V × V)} {k : ℕ} (hk : 0 < k)
+    (hout : ∀ v, (D.filter fun p => p.1 = v).card = k)
+    (hin : ∀ v, (D.filter fun p => p.2 = v).card = k) :
+    ∃ σ : Equiv.Perm V, ∀ v, (v, σ v) ∈ D := by
+  let := Fintype.ofFinite V
+  set t : V → Finset V := fun u => (D.filter fun p => p.1 = u).image Prod.snd
+  have hall : ∀ s : Finset V, s.card ≤ (s.biUnion t).card := by
+    intro s
+    -- arcos que salen de `s`
+    have h1 : (D.filter fun p => p.1 ∈ s).card = k * s.card := by
+      have : (D.filter fun p => p.1 ∈ s) = s.biUnion fun u => D.filter fun p => p.1 = u := by
+        ext p; simp only [mem_filter, mem_biUnion]
+        constructor
+        · rintro ⟨hp, hs⟩; exact ⟨p.1, hs, hp, rfl⟩
+        · rintro ⟨u, hu, hp, rfl⟩; exact ⟨hp, hu⟩
+      rw [this, card_biUnion fun x _ y _ hxy => disjoint_filter.mpr fun p _ h1 h2 =>
+        hxy (h1.symm.trans h2)]
+      rw [Finset.sum_congr rfl fun u _ => hout u, sum_const, smul_eq_mul, Nat.mul_comm]
+    -- llegan a `N(s)`
+    have h2 : (D.filter fun p => p.2 ∈ s.biUnion t).card = k * (s.biUnion t).card := by
+      have : (D.filter fun p => p.2 ∈ s.biUnion t) =
+          (s.biUnion t).biUnion fun w => D.filter fun p => p.2 = w := by
+        ext p; simp only [mem_filter, mem_biUnion]
+        constructor
+        · rintro ⟨hp, hs⟩; exact ⟨p.2, hs, hp, rfl⟩
+        · rintro ⟨w, hw, hp, rfl⟩; exact ⟨hp, hw⟩
+      rw [this, card_biUnion fun x _ y _ hxy => disjoint_filter.mpr fun p _ h1 h2 =>
+        hxy (h1.symm.trans h2)]
+      rw [Finset.sum_congr rfl fun w _ => hin w, sum_const, smul_eq_mul, Nat.mul_comm]
+    have h3 : (D.filter fun p => p.1 ∈ s) ⊆ D.filter fun p => p.2 ∈ s.biUnion t := by
+      intro p hp
+      obtain ⟨hpD, hps⟩ := mem_filter.mp hp
+      refine mem_filter.mpr ⟨hpD, mem_biUnion.mpr ⟨p.1, hps, ?_⟩⟩
+      exact mem_image.mpr ⟨p, mem_filter.mpr ⟨hpD, rfl⟩, rfl⟩
+    have := card_le_card h3
+    rw [h1, h2] at this
+    exact Nat.le_of_mul_le_mul_left this hk
+  obtain ⟨f, hf, hft⟩ := (Finset.all_card_le_biUnion_card_iff_exists_injective t).mp hall
+  have hbij : Function.Bijective f := Finite.injective_iff_bijective.mp hf
+  refine ⟨Equiv.ofBijective f hbij, fun v => ?_⟩
+  obtain ⟨p, hp, hpv⟩ := mem_image.mp (hft v)
+  obtain ⟨hpD, hp1⟩ := mem_filter.mp hp
+  have : p = (v, f v) := Prod.ext hp1 hpv
+  simpa [this] using hpD
+
+omit [Fintype V] in
+/-- **Descomposición en permutaciones.** Un digrafo `k`-regular (de entrada y salida) se parte
+en `k` permutaciones con arcos disjuntos. -/
+theorem exists_perm_decomp [Finite V] : ∀ (k : ℕ) (D : Finset (V × V)),
+    (∀ v, (D.filter fun p => p.1 = v).card = k) → (∀ v, (D.filter fun p => p.2 = v).card = k) →
+    ∃ σ : Fin k → Equiv.Perm V, (∀ i v, (v, σ i v) ∈ D) ∧
+      (∀ i j v, σ i v = σ j v → i = j) ∧ (∀ p ∈ D, ∃ i, σ i p.1 = p.2) := by
+  intro k
+  let := Fintype.ofFinite V
+  induction k with
+  | zero =>
+    intro D hout _
+    refine ⟨Fin.elim0, fun i => i.elim0, fun i => i.elim0, fun p hp => ?_⟩
+    have := hout p.1
+    rw [card_eq_zero] at this
+    have hmem : p ∈ D.filter (fun q => q.1 = p.1) := mem_filter.mpr ⟨hp, rfl⟩
+    rw [this] at hmem
+    exact absurd hmem (notMem_empty _)
+  | succ k ih =>
+    intro D hout hin
+    obtain ⟨σ₀, hσ₀⟩ := exists_perm_subset (Nat.succ_pos k) hout hin
+    set M := univ.image fun v => (v, σ₀ v)
+    set D' := D \ M
+    have hM : ∀ p, p ∈ M ↔ σ₀ p.1 = p.2 := by
+      intro p
+      simp only [M, mem_image, mem_univ, true_and]
+      constructor
+      · rintro ⟨v, rfl⟩; rfl
+      · intro h; exact ⟨p.1, Prod.ext rfl h⟩
+    have hout' : ∀ v, (D'.filter fun p => p.1 = v).card = k := by
+      intro v
+      have : D'.filter (fun p => p.1 = v) = (D.filter fun p => p.1 = v).erase (v, σ₀ v) := by
+        ext p
+        simp only [D', mem_filter, mem_sdiff, mem_erase, hM]
+        constructor
+        · rintro ⟨⟨hpD, hpM⟩, rfl⟩
+          exact ⟨fun h => hpM (by rw [h]), hpD, rfl⟩
+        · rintro ⟨hne, hpD, rfl⟩
+          exact ⟨⟨hpD, fun h => hne (Prod.ext rfl h.symm)⟩, rfl⟩
+      have hm : (v, σ₀ v) ∈ D.filter (fun p => p.1 = v) := mem_filter.mpr ⟨hσ₀ v, rfl⟩
+      rw [this, card_erase_of_mem hm, hout v]
+      rfl
+    have hin' : ∀ w, (D'.filter fun p => p.2 = w).card = k := by
+      intro w
+      have : D'.filter (fun p => p.2 = w) =
+          (D.filter fun p => p.2 = w).erase (σ₀.symm w, w) := by
+        ext p
+        simp only [D', mem_filter, mem_sdiff, mem_erase, hM]
+        constructor
+        · rintro ⟨⟨hpD, hpM⟩, rfl⟩
+          refine ⟨fun h => hpM ?_, hpD, rfl⟩
+          rw [h]; simp
+        · rintro ⟨hne, hpD, rfl⟩
+          refine ⟨⟨hpD, fun h => hne (Prod.ext ?_ rfl)⟩, rfl⟩
+          rw [← h]; simp
+      have hm : (σ₀.symm w, w) ∈ D.filter (fun p => p.2 = w) :=
+        mem_filter.mpr ⟨by simpa using hσ₀ (σ₀.symm w), rfl⟩
+      rw [this, card_erase_of_mem hm, hin w]
+      rfl
+    obtain ⟨τ, hτD, hτdisj, hτcov⟩ := ih D' hout' hin'
+    refine ⟨Fin.cons σ₀ τ, fun i v => ?_, fun i j v hij => ?_, fun p hp => ?_⟩
+    · refine Fin.cases ?_ (fun j => ?_) i
+      · exact hσ₀ v
+      · exact (mem_sdiff.mp (hτD j v)).1
+    · have hnot : ∀ j v, τ j v ≠ σ₀ v := by
+        intro j v h
+        exact (mem_sdiff.mp (hτD j v)).2 ((hM _).mpr h.symm)
+      induction i using Fin.cases with
+      | zero =>
+        induction j using Fin.cases with
+        | zero => rfl
+        | succ j => exact absurd hij.symm (by simpa using hnot j v)
+      | succ i =>
+        induction j using Fin.cases with
+        | zero => exact absurd hij (by simpa using hnot i v)
+        | succ j => simp only [Fin.cons_succ] at hij; rw [hτdisj i j v hij]
+    · by_cases hpM : p ∈ M
+      · exact ⟨0, by simpa using (hM p).mp hpM⟩
+      · obtain ⟨j, hj⟩ := hτcov p (mem_sdiff.mpr ⟨hp, hpM⟩)
+        exact ⟨j.succ, by simpa using hj⟩
+
+/-! ### Los 2-factores -/
+
+/-- El 2-factor asociado a una permutación: `u ∼ w` si `σ u = w` o `σ w = u`. -/
+def permGraph (σ : Equiv.Perm V) : SimpleGraph V where
+  Adj u w := u ≠ w ∧ (σ u = w ∨ σ w = u)
+  symm := ⟨fun _ _ h => ⟨h.1.symm, h.2.symm⟩⟩
+  loopless := ⟨fun _ h => h.1 rfl⟩
+
+variable {G : SimpleGraph V} [DecidableRel G.Adj]
+
+omit [DecidableEq V] in
+/-- **Teorema del 2-factor de Petersen.** Todo grafo finito `2k`-regular se descompone en `k`
+2-factores disjuntos en aristas. -/
+theorem petersen_two_factor (k : ℕ) (h : ∀ v, G.degree v = 2 * k) :
+    ∃ F : Fin k → SimpleGraph V, (∀ i, F i ≤ G) ∧
+      (∀ i v, ((F i).neighborSet v).ncard = 2) ∧
+      (∀ i j, i ≠ j → Disjoint (F i) (F j)) ∧ ⨆ i, F i = G := by
+  classical
+  obtain ⟨Ds, hinj, hbal, hcov⟩ :=
+    exists_balanced_orientation (G := G) fun v => ⟨k, by rw [h v]; omega⟩
+  set D := Ds.image Dart.toProd
+  have hDmem : ∀ p, p ∈ D ↔ ∃ d ∈ Ds, d.toProd = p := fun p => by simp [D]
+  have htoProd_inj : ∀ d ∈ Ds, ∀ d' ∈ Ds, d.toProd = d'.toProd → d = d' :=
+    fun d _ d' _ h => (Dart.ext_iff d d').mpr h
+  -- grados de salida y de entrada
+  have hsum : ∀ v, (Ds.filter fun d => d.fst = v).card + (Ds.filter fun d => d.snd = v).card =
+      2 * k := by
+    intro v
+    rw [← card_image_edge_filter hinj, ← h v, ← card_incidenceFinset_eq_degree]
+    congr 1
+    ext e
+    simp only [mem_filter, mem_image, mem_incidenceFinset, incidenceSet, Set.mem_ofPred_eq]
+    constructor
+    · rintro ⟨⟨d, -, rfl⟩, hv⟩; exact ⟨d.edge_mem, hv⟩
+    · rintro ⟨he, hv⟩; obtain ⟨d, hd, rfl⟩ := hcov e he; exact ⟨⟨d, hd, rfl⟩, hv⟩
+  have hfilter1 : ∀ v, (D.filter fun p => p.1 = v).card = (Ds.filter fun d => d.fst = v).card := by
+    intro v
+    rw [show D.filter (fun p => p.1 = v) = (Ds.filter fun d => d.fst = v).image Dart.toProd by
+      ext p; simp only [D, mem_filter, mem_image, and_comm]; constructor
+      · rintro ⟨h1, a, rfl, ha⟩; exact ⟨a, rfl, h1, ha⟩
+      · rintro ⟨a, rfl, h1, ha⟩; exact ⟨h1, a, rfl, ha⟩, card_image_of_injOn fun d hd d' hd' =>
+        htoProd_inj d (mem_filter.mp hd).1 d' (mem_filter.mp hd').1]
+  have hfilter2 : ∀ v, (D.filter fun p => p.2 = v).card = (Ds.filter fun d => d.snd = v).card := by
+    intro v
+    rw [show D.filter (fun p => p.2 = v) = (Ds.filter fun d => d.snd = v).image Dart.toProd by
+      ext p; simp only [D, mem_filter, mem_image, and_comm]; constructor
+      · rintro ⟨h1, a, rfl, ha⟩; exact ⟨a, rfl, h1, ha⟩
+      · rintro ⟨a, rfl, h1, ha⟩; exact ⟨h1, a, rfl, ha⟩, card_image_of_injOn fun d hd d' hd' =>
+        htoProd_inj d (mem_filter.mp hd).1 d' (mem_filter.mp hd').1]
+  have hout : ∀ v, (D.filter fun p => p.1 = v).card = k := by
+    intro v; have := hsum v; have := hbal v; rw [hfilter1]; omega
+  have hin : ∀ v, (D.filter fun p => p.2 = v).card = k := by
+    intro v; have := hsum v; have := hbal v; rw [hfilter2]; omega
+  obtain ⟨σ, hσD, hσdisj, hσcov⟩ := exists_perm_decomp k D hout hin
+  -- propiedades de `D`
+  have hDadj : ∀ u w, (u, w) ∈ D → G.Adj u w := by
+    intro u w huw
+    obtain ⟨d, -, hd⟩ := (hDmem _).mp huw
+    have := d.adj
+    rw [show d.fst = u from congrArg Prod.fst hd, show d.snd = w from congrArg Prod.snd hd] at this
+    exact this
+  have hDanti : ∀ u w, (u, w) ∈ D → (w, u) ∉ D := by
+    intro u w huw hwu
+    obtain ⟨d, hd, hdp⟩ := (hDmem _).mp huw
+    obtain ⟨d', hd', hdp'⟩ := (hDmem _).mp hwu
+    have he : d.edge = d'.edge := by
+      rw [Dart.edge, Dart.edge, hdp, hdp']; exact Sym2.eq_swap
+    have := hinj d hd d' hd' he
+    subst this
+    have h1 := congrArg Prod.fst (hdp.symm.trans hdp')
+    exact (hDadj u w huw).ne h1
+  refine ⟨fun i => permGraph (σ i), fun i u w huw => ?_, fun i v => ?_, fun i j hij => ?_, ?_⟩
+  · rcases huw.2 with h | h
+    · exact h ▸ hDadj _ _ (hσD i u)
+    · exact (h ▸ hDadj _ _ (hσD i w)).symm
+  · have hne1 : σ i v ≠ v := fun h' => (hDadj _ _ (hσD i v)).ne h'.symm
+    have hne2 : (σ i).symm v ≠ v := by
+      intro h'
+      have := hDadj _ _ (hσD i ((σ i).symm v))
+      rw [Equiv.apply_symm_apply, h'] at this
+      exact G.loopless.irrefl _ this
+    have hset : (permGraph (σ i)).neighborSet v = {σ i v, (σ i).symm v} := by
+      ext w
+      simp only [mem_neighborSet, permGraph, Set.mem_insert_iff, Set.mem_singleton_iff]
+      constructor
+      · rintro ⟨-, h' | h'⟩
+        · exact Or.inl h'.symm
+        · right; rw [← h']; simp
+      · rintro (rfl | rfl)
+        · exact ⟨hne1.symm, Or.inl rfl⟩
+        · exact ⟨hne2.symm, Or.inr (by simp)⟩
+    rw [hset, Set.ncard_pair]
+    intro heq
+    have h1 := hσD i v
+    have h2 := hσD i (σ i v)
+    have : σ i (σ i v) = v := by
+      conv_rhs => rw [← Equiv.apply_symm_apply (σ i) v]
+      rw [← heq]
+    rw [this] at h2
+    exact hDanti _ _ h1 h2
+  · rw [disjoint_iff_inf_le]
+    intro u w ⟨hi, hj⟩
+    exfalso
+    rcases hi.2 with h1 | h1 <;> rcases hj.2 with h2 | h2
+    · exact hij (hσdisj i j u (h1.trans h2.symm))
+    · exact hDanti _ _ (h1 ▸ hσD i u) (h2 ▸ hσD j w)
+    · exact hDanti _ _ (h1 ▸ hσD i w) (h2 ▸ hσD j u)
+    · exact hij (hσdisj i j w (h1.trans h2.symm))
+  · ext u w
+    rw [iSup_adj]
+    constructor
+    · rintro ⟨i, hi⟩
+      rcases hi.2 with h' | h'
+      · exact h' ▸ hDadj _ _ (hσD i u)
+      · exact (h' ▸ hDadj _ _ (hσD i w)).symm
+    · intro huw
+      obtain ⟨d, hd, hde⟩ := hcov s(u, w) huw
+      have hdD : d.toProd ∈ D := mem_image_of_mem _ hd
+      obtain ⟨i, hi⟩ := hσcov _ hdD
+      refine ⟨i, huw.ne, ?_⟩
+      rcases Sym2.eq_iff.mp hde with ⟨h1, h2⟩ | ⟨h1, h2⟩
+      · left; rw [← h1, ← h2]; exact hi
+      · right; rw [← h1, ← h2]; exact hi
+
+end SimpleGraph
diff --git a/LeanPool/projects/classical-matching-factors.yaml b/LeanPool/projects/classical-matching-factors.yaml
new file mode 100644
index 000000000..70a06c829
--- /dev/null
+++ b/LeanPool/projects/classical-matching-factors.yaml
@@ -0,0 +1,91 @@
+slug: classical-matching-factors
+title: Classical matching and factor theorems in finite graphs
+summary: >-
+  Develops augmenting-path and odd-component certificates for maximum matchings,
+  bipartite matching-cover duality, perfect matchings in bridgeless cubic graphs,
+  Tutte's f-factor criterion, and decompositions of even-regular graphs into
+  two-factors. Includes the finite Dilworth and Mirsky partition theorems as an
+  order-theoretic companion. All graph results use Mathlib's SimpleGraph and
+  matching predicates. Hall's and Tutte's one-factor theorems are imported from
+  Mathlib; the general matching and factor conclusions are proved here.
+  The collection integrates five Palomar-registered developments and does not
+  claim new mathematical results or a formalization of polynomial-time algorithms.
+branch: graph theory and finite order theory
+entry_module: LeanPool.ClassicalMatchingFactors
+authors:
+- Juan Pablo Traverso Gianini
+source:
+  title: A Short Proof of the Factor Theorem for Finite Graphs
+  authors:
+  - W. T. Tutte
+  doi: 10.4153/CJM-1954-033-3
+  url: https://github.com/jtraverso/tutte-f-factor/tree/dc3bbce463c80c499d3e9fa072d13f9145d907d0
+  github_repo: jtraverso/tutte-f-factor
+  commit: dc3bbce463c80c499d3e9fa072d13f9145d907d0
+  note: >-
+    This source anchors the f-factor development. The other four frozen source
+    repositories, their commits and Palomar IDs are linked in the imported
+    module docstrings; each main result below identifies its mathematical source.
+license: Apache-2.0
+status: verified
+provenance: AI
+main_declarations:
+- BergeMatching.exists_tutte_berge
+- FFactor.tutte_f_factor
+main_results:
+- declaration: BergeMatching.isMaximum_iff_not_exists_augmenting
+  informal: >-
+    A matching in a finite simple graph has maximum cardinality if and only if
+    it has no augmenting path, with distinct unmatched endpoints and alternating edges.
+  source_ref: Berge (1957), Two theorems in graph theory, doi:10.1073/pnas.43.9.842.
+- declaration: BergeMatching.exists_tutte_berge
+  informal: >-
+    Every finite simple graph admits a matching M and a vertex set U with
+    twice the number of matching edges plus the number of odd components of
+    G minus U equal to the number of vertices plus the size of U.
+  source_ref: Berge (1958), Sur le couplage maximum d'un graphe; PALOMAR-2026-10-16-000011.
+- declaration: Konig.Egervary.exists_matching_card_eq_vertexCover
+  informal: Every finite bipartite simple graph has a matching and a vertex cover of equal size.
+  source_ref: Kőnig and Egerváry (1931); PALOMAR-2026-10-15-000019.
+- declaration: PetersenTheorem.exists_isPerfectMatching_mem
+  informal: >-
+    For every edge in a finite bridgeless cubic simple graph there is a perfect
+    matching containing that edge.
+  source_ref: Petersen (1891), doi:10.1007/BF02392606; PALOMAR-2026-10-16-000004.
+- declaration: FFactor.tutte_f_factor
+  informal: >-
+    A finite simple graph has a spanning subgraph with prescribed nonnegative
+    integer vertex degrees f exactly when Tutte's odd-component inequality holds
+    for every pair of disjoint vertex sets S and T.
+  source_ref: Tutte (1952, 1954), doi:10.4153/CJM-1954-033-3; PALOMAR-2026-10-18-000005.
+- declaration: SimpleGraph.petersen_two_factor
+  informal: >-
+    Every finite simple graph of degree 2k at every vertex is the edge-disjoint
+    union of k spanning subgraphs of degree two at every vertex, including k equal to zero.
+  source_ref: Petersen (1891), doi:10.1007/BF02392606; PALOMAR-2026-10-16-000016.
+- declaration: Konig.Poset.dilworth
+  informal: A finite partially ordered set has an antichain A and a partition into the size of A chains.
+  source_ref: Dilworth (1950), doi:10.2307/1969503; proof follows Galvin (1994).
+- declaration: Konig.Poset.mirsky
+  informal: A finite partially ordered set has a chain C and a partition into the size of C antichains.
+  source_ref: Mirsky (1971), doi:10.1080/00029890.1971.11992886.
+- declaration: ClassicalMatchingFactors.exists_matching_with_barrier_and_no_augmenting
+  informal: >-
+    A finite graph admits a matching with both a tight odd-component barrier
+    and no augmenting path, combining the two maximum-matching certificates.
+  source_ref: Interface corollary of the two proved Berge theorems in this collection.
+- declaration: ClassicalMatchingFactors.exists_optimal_matching_cover_pair
+  informal: >-
+    A finite bipartite graph admits an equal-size matching and vertex cover
+    which respectively maximize matching size and minimize cover size.
+  source_ref: Interface corollary of the proved Kőnig-Egerváry theorem and weak duality.
+tags:
+- graph-theory
+- matchings
+- graph-factors
+- minimax-theorems
+- finite-orders
+msc:
+- 05C70
+- 05C15
+- 06A07