slug: ahanjideh-ekim-yildiz-2022-z-of-d-conjecture-6-5
bibkey: ahanjidehekimyildiz2022matching
doi: 10.1007/s10878-024-01123-z
url: https://arxiv.org/abs/2207.02271v1
triage: theorem
motivation_gids:
  - D5/S3/Combinatorics/Graph/ComponentPacking/AhanjidehEkimYildizZ.result

The extremal matching number of almost regular triangle-free graphs

Problem

M. Ahanjideh, T. Ekim and M. A. Yıldız, Maximum size of a triangle-free graph with bounded maximum degree and matching number, arXiv:2207.02271v1, Conjecture 6.5:

For d ≥ 21 and odd, we have Z(d) = ⌊5(d + 1)/4⌋.

The journal locator is DOI 10.1007/s10878-024-01123-z. The quotations refer to version 1. The source defines $Z(d)$, for $d\ge 2$, as the least matching number of a triangle-free factor-critical graph that is regular of degree $d$ when $d$ is even, and almost regular of degree $d$ when $d$ is odd.

Statement echo

Finite simple graphs have carrier Fin n; the matching number is the existing DimerVirialFourthDifferenceRefutation.matchingNumber. The formal definition of $Z$ is total on natural numbers and admits an empty carrier. The proved range has a deficient vertex and is nonempty. No statement about the paper’s convention at even or small degrees is inferred from this total extension.

Motivation

The source’s Lemma 4.7 brackets $Z(d)$ between $\lfloor 5(d-1)/4\rfloor$ and $\lfloor 5(d+1)/4\rfloor$ for odd $d$. The result identifies the endpoint for every odd $d\ge 21$. The two odd residue classes have uniform extremal constructions, while the lower bound rules out smaller orders.

Gap

Preregistration #19633 gives the source quotation, quantified conventions and literature screen. The inspected Banak–Ekim–Taşkın arXiv:2304.01729v1 gives small cases and leaves the target range unsettled. The original source’s full journal text and all later literature have not been exhaustively verified. Literature status is not-found-in-searched-scope; completeness is ASSUMED-UNVERIFIED.

The structural input is the strict three-eighths theorem of Häggkvist: every finite triangle-free graph with $3|V|<8\delta$ admits a homomorphism to the pentagon. Its source is identified in Library/GraphInvariants/haggkvist1982oddcycles.md; the original chapter’s full text is unverified. The delivered graph modules prove the structural reduction from finite counting.

Route

Factor-criticality identifies the order as twice the matching number plus one. Below the proposed bound, the three-eighths inequality gives a pentagon homomorphism except at degree 23 and order 59. In that exception, deletion of the deficient vertex permits the density theorem; an independent support argument extends the map to the deleted vertex. Nonbipartiteness forces the pentagon map to be surjective.

Write $s_i$ for the five class sizes, $t_i=s_{i-1}+s_{i+1}$ and $u_i=t_i-d$. The total slack can only be one or three. Missing edges give cyclic incidence equations whose independent-set inequalities contradict every slack pattern. This proves the lower bound. Dense balanced Hall matchings supply the almost regular pentagon constructions for both odd residue classes, giving attainment and the matching upper bound. Natural-infimum composition yields the exact equality.

Falsifier

The exact target is false if an odd $d\ge 21$ has an admissible graph with matching number below $\lfloor 5(d+1)/4\rfloor$, or if no admissible graph attains that number. The kernel-checked lower obstruction and uniform attainment exclude these two possibilities in the formal finite-simple-graph model. No axiom asserting a graph-structure theorem is added.

Evidence

The settling declaration is D5.S3.Combinatorics.Graph.ComponentPacking.AhanjidehEkimYildizZ.result. Its Scribe displays the entire quantified equality. Each supporting module has its own canonical state record under Golden/Frozen/state/; the modified Dimer owner and its affected frozen importer are maintained by the canonical writer.

The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}.

Experiment

Exact finite checks contain the independent program and results. The script check.py has SHA-256 e66ffd72eab1d44edba7d8a5d51ae7904ad8e413ba460f7a5f412e15f32605d6. Running python3 docs/reports/ahanjideh-ekim-yildiz-2022-z-of-d-odd-conjecture-6-5/check.py in that experiment checkout with NetworkX 3.7 exits 0 (RESULT PASS). The implementation seat measured this with its isolated Python interpreter.

The construction checks cover exactly $d=21,23,25,27,29,31$, with orders $55,61,65,71,75,81$ and matching numbers $27,30,32,35,37,40$. At $d=23$, order 59, all 2310 feasible pairs $(a,w)$ have independent support. The slack tests cover $U=1$ with $11\le C\le 60$, and $U=3$ with $13\le C\le 60$, every composition and deficient class; no pattern survives all independent-set inequalities. The arithmetic tests cover odd $d$ from 21 through 401. These finite computations do not establish the unbounded theorem; the Lean proofs do.

Escape audit

The four-slot escape audit is unfinished in #20094. Faithful dependent-family reconstruction, exact bridges, variation, sensitivity and actual observational dependence have not been established. No registration is reported as declared_validated.

Triage

Tier 1 published conjecture. Settlement Proved, admission basis open-problem-resolution (#19633; Proved). The existing Dimer refutation retains open-problem-resolution (issue #12197; Refuted) and its own dossier and resolution node.

What the settlement shows

• Kernel-checked: AhanjidehEkimYildizZ.result proves $Z(d)=\lfloor 5(d+1)/4\rfloor$ for every odd $d\ge 21$.
• Kernel-checked: PentagonMissingEdgeObstruction.PentagonSurjectiveLower.no_small_surjective_map excludes the smaller odd orders for a surjective pentagon map with the almost regular degree pattern. The decisive obstruction is the incompatibility of missing-edge incidence with total slack one or three.
• Kernel-checked: PentagonMissingEdgeObstruction.OrderArithmetic.threshold_or_exception isolates the degree-23, order-59 exception. The proof of AhanjidehEkimYildizZ.ExceptionalLower.no_order_59 excludes it by vertex deletion, independent support and extension.
• Kernel-checked: AhanjidehEkimYildizZUpper.AEYUpperAttainment.attainment constructs triangle-free factor-critical witnesses attaining the bound for both odd residue classes. Its proof uses the degree-row identities ConstructionRows.degree_small and .degree_large and the consumed factor-critical matching construction.
• Kernel-checked proof step: AhanjidehEkimYildizZ.AEYInfimum.Z_eq_of_attainment composes the lower bound and attainment, including the equality transport between decidability instances. No mathematical obligation remains for the stated conjecture.
• Literature reading: the source’s Lemma 4.7 gives the two-sided partial bound; Banak–Ekim–Taşkın, Section 2, lists $Z(d)=d$ for $d=2,3$ and $Z(d)=d+1$ for $d=4,5$. These are cited source statements, not additional Lean theorems of this delivery. The proposed formula already fails at $d=3,5$; the present theorem asserts no uniform extension to small odd degrees.
• Proved in prose, conditional on the source’s Theorem 4.8: that theorem states $f_M(d,m)=dm+\lfloor d/2\rfloor$ when $Z(d)\le m<2d$. Substituting the established equality gives its explicit interval $\lfloor 5(d+1)/4\rfloor \le m<2d$ for odd $d\ge 21$. Theorem 4.8 itself is not formalized here.
• Computed: the finite construction, exceptional-support, slack and arithmetic readings have exactly the scopes in the Experiment entry. Uniform validity beyond those experimental scopes is supplied only where a named Lean theorem above states it.
• Open: extensions outside odd $d\ge 21$, independent formal verification of the source’s other results, and the four-slot registration evidence in #20094.

Declaration classification

The module labels below expand to the following Lean namespace prefixes:

• dense: D5.S3.Combinatorics.Graph.Walks.DenseTriangleFreeConfigurations.
• hagg: D5.S3.Combinatorics.Graph.Walks.HaggkvistPentagonHomomorphism.
• matching: D5.S3.Combinatorics.Graph.ComponentPacking.FactorCriticalMatching.
• obstruction: D5.S3.Combinatorics.Graph.ComponentPacking.PentagonMissingEdgeObstruction.
• upper: D5.S3.Combinatorics.Graph.ComponentPacking.AhanjidehEkimYildizZUpper.
• settlement: D5.S3.Combinatorics.Graph.ComponentPacking.AhanjidehEkimYildizZ.
• dimer: D5.S3.StatisticalMechanics.DimerVirialFourthDifferenceRefutation.

Classifications expand same-delivery helpers and compiler-generated constants, with the frozen base and pinned Mathlib as the stopping boundary. Fixed closed certificate checks are bind-only consumed helpers.

ASSUMED-UNVERIFIED

Literature completeness, the source’s journal text, the original Häggkvist chapter, and every later paper outside the preregistration’s inspected scope remain unverified. Bounded unsuccessful owner/bypass searches do not prove that no alternative proof exists. The total definition’s even/small-degree and empty-carrier boundary is outside the proved statement. The registration gap is #20094.