The extremal matching number for odd degrees

Abstract

The least matching number of an almost regular, triangle-free, factor-critical graph has an exact formula for every odd degree at least twenty-one.

Definition 1.1 (The least admissible matching number).

$$\forall d:\mathbb{N},Z\left(d\right)=\mathrm{sInf}\left(\{m:\mathbb{N}\mid \exists n:\mathbb{N},\exists G:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right),(\mathrm{ite}\left(\mathrm{Even}\left(d\right),\mathrm{IsRegularOfDegree}\left(G,d\right),\mathrm{IsAlmostRegular}\left(G,d\right)\right))\wedge ((\mathrm{CliqueFree}\left(G,3\right))\wedge ((\mathrm{IsFactorCritical}\left(G\right))\wedge (\mathrm{matchingNumber}\left(G\right)=m)))\}\right)$$

Formalization. D5/S3/Combinatorics/Graph/ComponentPacking/AhanjidehEkimYildizZ.Z (✓ 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.

Definition 4.2, page 8: “For any d ≥ 2, let Z(d) be the smallest natural number n such that there exists a d-regular (if d is even) or almost d-regular (if d is odd) triangle-free and factor-critical graph G with ν(G) = n.” Finite graphs have carrier Fin n. The matching number is DimerVirialFourthDifferenceRefutation.matchingNumber; the minimum is the infimum in the natural numbers. The formula defines Z for every natural d, and the theorem uses only odd d at least 21.

Definition 1.2 (Conjecture 6.5).

$$(claim)\iff (\forall d:\mathbb{N},(21\le d)\Rightarrow ((\mathrm{Odd}\left(d\right))\Rightarrow (Z\left(d\right)=\mathrm{Nat}.\mathrm{div}\left(5\cdot (d+1),4\right))))$$

Formalization. D5/S3/Combinatorics/Graph/ComponentPacking/AhanjidehEkimYildizZ.claim (✓ 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.

Conjecture 6.5, page 20: “For d ≥ 21 and odd, we have Z(d) = ⌊5(d + 1)/4⌋.” The natural-number quotient is floor division. The degree d ranges over all natural numbers satisfying both hypotheses.

Theorem 1.3 (The conjectured equality).

$$\forall d:\mathbb{N},(21\le d)\Rightarrow ((\mathrm{Odd}\left(d\right))\Rightarrow (Z\left(d\right)=\mathrm{Nat}.\mathrm{div}\left(5\cdot (d+1),4\right)))$$

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

Resolves. Problems/ahanjideh-ekim-yildiz-2022-z-of-d-conjecture-6-5 (proved) by D5/S3/Combinatorics/Graph/ComponentPacking/AhanjidehEkimYildizZ.result.

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 triangle-free graph below the proposed extremal order admits a pentagon partition through the three-eighths minimum-degree theorem. The exceptional degree 23 and order 59 is handled by deleting the deficient vertex and extending the partition. The cyclic missing-edge incidence inequalities rule out total slack one and three. The almost regular pentagon constructions attain the remaining matching number.

References

• Truth anchor: D5/S3/Combinatorics/Graph/ComponentPacking/AhanjidehEkimYildizZ.Z
• Truth anchor: D5/S3/Combinatorics/Graph/ComponentPacking/AhanjidehEkimYildizZ.claim
• Truth anchor: D5/S3/Combinatorics/Graph/ComponentPacking/AhanjidehEkimYildizZ.result
• Dependency: D5/S3/Combinatorics/Graph/ComponentPacking/AhanjidehEkimYildizZUpper
• Dependency: D5/S3/Combinatorics/Graph/ComponentPacking/FactorCriticalMatching
• Dependency: D5/S3/Combinatorics/Graph/ComponentPacking/PentagonMissingEdgeObstruction
• Dependency: D5/S3/Combinatorics/Graph/Walks/DenseTriangleFreeConfigurations
• Dependency: D5/S3/Combinatorics/Graph/Walks/HaggkvistPentagonHomomorphism
• Dependency: D5/S3/StatisticalMechanics/DimerVirialFourthDifferenceRefutation