FactorCriticalMatching

Abstract

Finite graph structure, degree counting, and perfect matchings.

Definition 1.1 (IsAlmostRegular).

$$\forall (n:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}(\mathrm{Fin}n)),\forall [\mathrm{DecidableRel}G.\mathrm{Adj}],\forall (d:\mathbb{N}),(\mathrm{IsAlmostRegular}Gd)⟺((\exists (w:\mathrm{Fin}n),(G.\mathrm{degree}w=d-1)\wedge ((\forall (v:\mathrm{Fin}n),(v\ne w)\to (G.\mathrm{degree}v=d)))))$$

Formalization. D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.IsAlmostRegular (✓ std3).

Citation. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

Section 2, page 3: “if d(w) = d − 1 for some w ∈ V(G) and d(v) = d for all v ∈ V(G) − w, then G is said to be almost d-regular.” The carrier is Fin n and the natural subtraction d − 1 follows this expression.

Definition 1.2 (IsFactorCritical).

$$\forall (n:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}(\mathrm{Fin}n)),(\mathrm{IsFactorCritical}G)⟺((\forall (v:\mathrm{Fin}n),\exists (M:(G.\mathrm{induce}(\{v{\}}^c:\mathrm{Set}(\mathrm{Fin}n))).\mathrm{Subgraph}),M.\mathrm{IsPerfectMatching}))$$

Formalization. D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.IsFactorCritical (✓ std3).

Citation. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

Section 2, page 4: “A graph G is said to be factor-critical if G \ v has a perfect matching for all v ∈ V(G).” Deletion is the induced graph on the complement of the singleton.

Theorem 1.3 (odd order).

$$\forall (N:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}(\mathrm{Fin}N)),((\mathrm{IsFactorCritical}G))\to ((((0<N))\to ((\mathrm{Odd}N))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.odd_order (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

A perfect matching after one vertex deletion forces the remaining order to be even.

Theorem 1.4 (almost regular order eq).

$$\forall (N:\mathbb{N}),\forall (d:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}(\mathrm{Fin}N)),\forall [\mathrm{DecidableRel}G.\mathrm{Adj}],((\mathrm{IsFactorCritical}G))\to ((((\mathrm{IsAlmostRegular}Gd))\to ((N=2\cdot \mathrm{matchingNumber}G+1))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.almost_regular_order_eq (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

A nonempty factor-critical graph has one more vertex than twice its matching number. Almost regularity supplies nonemptiness.

Theorem 1.5 (exists equiv of omission bound).

$$\forall (A:\mathrm{Type}),\forall (B:\mathrm{Type}),\forall [\mathrm{Fintype}A],\forall [\mathrm{Fintype}B],\forall (R:(A)\to ((B)\to (\mathrm{Prop}))),\forall [\mathrm{DecidableRel}R],\forall (r:\mathbb{N}),((\mathrm{Fintype}.\mathrm{card}A=\mathrm{Fintype}.\mathrm{card}B))\to ((((2\cdot r\le \mathrm{Fintype}.\mathrm{card}B))\to (((\forall (a:A),(\mathrm{Finset}.\mathrm{univ}.\mathrm{filter}(fun(b:B)\mapsto \neg Rab)).\mathrm{card}\le r)\to ((\forall (b:B),(\mathrm{Finset}.\mathrm{univ}.\mathrm{filter}(fun(a:A)\mapsto \neg Rab)).\mathrm{card}\le r)\to (\exists (f:\mathrm{Equiv}\left(A,B\right)),\forall (a:A),Ra(fa)))))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.exists_equiv_of_omission_bound (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

Two finite sets of equal size admit a compatible bijection when each element omits at most r partners in the other set and both sets have at least 2r elements. The proof verifies Hall’s condition.

Theorem 1.6 (color balance).

$$\forall (V:\mathrm{Type}),\forall [\mathrm{Fintype}V],\forall (G:\mathrm{SimpleGraph}V),\forall (M:G.\mathrm{Subgraph}),((M.\mathrm{IsPerfectMatching}))\to ((\forall (c:(V)\to (\mathrm{Fin}2)),(\forall (xy:V),(G.\mathrm{Adj}xy)\to (cx\ne cy))\to (\mathrm{Fintype}.\mathrm{card}\{x:V\mid cx=0\}=\mathrm{Fintype}.\mathrm{card}\{x:V\mid cx=1\})))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.color_balance (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

Every perfect matching exchanges the two classes of a proper two-coloring, so the classes have the same cardinality.

Theorem 1.7 (deleted color count).

$$\forall (V:\mathrm{Type}),\forall [\mathrm{Fintype}V],\forall [\mathrm{DecidableEq}V],\forall (C:\mathrm{Type}),\forall [\mathrm{DecidableEq}C],\forall (c:(V)\to (C)),\forall (i:C),\forall (v:V),\mathrm{Fintype}.\mathrm{card}\{x:(\{v{\}}^c:\mathrm{Set}V)\mid c(\mathrm{Subtype}.\mathrm{val}x)=i\}=(\mathrm{Finset}.\mathrm{univ}.\mathrm{filter}(fun(x:V)\mapsto cx=i)).\mathrm{card}-(ifcv=ithen1else0)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.deleted_color_count (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

Deleting a vertex removes one member of its color class and leaves every other color count unchanged.

Theorem 1.8 (no two color).

$$\forall (N:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}(\mathrm{Fin}N)),((\mathrm{IsFactorCritical}G))\to (((\exists (ab:\mathrm{Fin}N),G.\mathrm{Adj}ab)\to (\neg (\exists (c:(\mathrm{Fin}N)\to (\mathrm{Fin}2)),\forall (xy:\mathrm{Fin}N),(G.\mathrm{Adj}xy)\to (cx\ne cy)))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.no_two_color (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. M. Ahanjideh; T. Ekim; M. A. Yıldız (2022). Maximum size of a triangle-free graph with bounded maximum degree and matching number. DOI: 10.1007/s10878-024-01123-z. URL: https://arxiv.org/abs/2207.02271v1.

Commentary.

A factor-critical graph containing an edge has no proper two-coloring: deleting vertices of opposite colors would force incompatible color-class balances.

References

• Truth anchor: D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.IsAlmostRegular
• Truth anchor: D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.IsFactorCritical
• Truth anchor: D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.almost_regular_order_eq
• Truth anchor: D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.color_balance
• Truth anchor: D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.deleted_color_count
• Truth anchor: D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.exists_equiv_of_omission_bound
• Truth anchor: D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.no_two_color
• Truth anchor: D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching.odd_order
• Dependency: D5/S3/StatisticalMechanics/DimerVirialFourthDifferenceRefutation
• Dependency: D5/S3/Zeros/Convolution/MatchingFiber