Erdős 944: machine-checked cores for the k=4, r=1 six-regular subproblem

[AlperTheKing]

Adds a "Verified partial results" section to FormalConjectures/ErdosProblems/944.lean with machine-checked cores of verified progress on the k=4, r=1 case (the six-regular subproblem isolated by Skottova-Steiner, arXiv:2508.08703, Problem 5.2). Existing statement declarations are unchanged.

Proven, no sorry / no native_decide; axioms at most [propext, Classical.choice, Quot.sound] (singleton_edge_critical is axiom-free). The added results: singleton_edge_critical (recolouring core of the singleton lemma: a colour appearing exactly once in N(v) under a 3-colouring of G-v yields a critical edge in a 4-vertex-critical graph); comps and mem_comps (enumeration of weak compositions with a proved completeness lemma); cut_matrix_classification (exactly 21 of the 3x3 nonnegative matrices with entry sum 6 have all six permutation-diagonal sums at least 2 - the exact equality case of the Skottova-Steiner 6-edge-cut bound for (4,1)-graphs); matrix_mem_classification (bridge from the genuine matrix form to the enumerated list); turan_count_shore (floor(a^2/3) < 3a-3 for 2 <= a <= 7, excluding small 6-cut shores).

Context, verified computationally with two independent implementations and generator-completeness guards (code and certificates available on request): no 6-regular 4-vertex-critical graph exists on n <= 15 other than a unique one on n = 13 (which has critical edges), so any 6-regular (4,1)-graph has at least 16 vertices; and in any 6-regular (4,1)-graph every 6-edge-cut is either a vertex star or has both shores of size at least 15 (119,236,283,370 candidate shores excluded at size 14 alone) - hence such a graph on n <= 29 vertices is super-6-edge-connected.

Update (commit 3): adds an Erdos944.ZeroBudget sub-namespace with the zero-budget identities for the deficiency-6 shore analysis, fully proven (no sorry / no native_decide; axioms [propext, Classical.choice, Quot.sound]): zero_budget_edge_formula (L1: s_IJ = 6p - 6q + 2B_k - 8 for a deletion-unfrozen full vertex in a graph with max degree 6 and total deficiency 6), charge_identity (L2: 6p - s_IJ = 6q + 8 - 2B_k, the component charge identity), and double_sum_even (kappa-parity). These are the arithmetic core of the structural ("frozen kernel") programme on Problem 5.2.

Update (commit 5): adds cut_row_forcing, the row-sum equality cases of the 21-matrix classification (proven, no sorry / no native_decide; axioms [propext]): among the 21 valid 6-edge-cut matrices, row sums (3,3,0) force both nonzero rows to be (1,1,1) and row sums (6,0,0) force the nonzero row to be (2,2,2). This is the matrix engine behind a new all-sizes structural theorem on Problem 5.2 (verified computationally and by hand, write-up in preparation): no shore of a nontrivial 6-edge-cut in a 6-regular (4,1)-graph induces a bipartite graph, and a shore whose deficiency is concentrated on two vertices forces those vertices to receive equal colours in every proper 3-colouring. The proof plays the cut-matrix classification against vertex-criticality; it is sharp, since the incidence graph of PG(2,5) yields deficiency-6 candidates passing all one-sided counting filters.

---

These results now have a companion arXiv note with full proofs (these Lean cores are included as ancillary files): A. Ferudun, Exact 6-cut rigidity and small-order superconnectivity for the 6-regular case of Dirac's k=4 problem, arXiv:2606.18462 (2026).

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.

[mo271]

Thanks, thise seems a little bit to long or too far away from questions ask on erdosproblems.com?
Perhaps on could comapct it using the formal_proof using formal_conjectures at [link] mechanism?
Also: please prefer latex markdown over backticks in markdown.

[AlperTheKing]

Thanks! Addressed in 0946e98:

• Compacted the file: removed the ~470-line inlined "Verified partial results" / "Zero-budget identities" development. The file is now back to the problem statements plus a single compact statement of the verified consequence — any 6-regular (4,1)-graph has ≥ 16 vertices — which is exactly the small-order case of Skottová–Steiner Problem 5.2.
• LaTeX markdown used for the math in the docstrings instead of backticks.

On the formal_proof using formal_conjectures at [link] suggestion: I held off, because it would overclaim here. The result is established by a computational enumeration (all 6-regular graphs on n ≤ 15, ~21.6M, in C++/nauty) together with the partial Lean cores from the previous version — there is no single self-contained Lean proof to point formal_proof at. Instead the docstring cites the arXiv note (2606.18462), whose ancillary files contain the full proofs, code, certificates and those Lean cores. Happy to switch to a formal_proof using ... attribute (or other_system) if you'd prefer a specific framing.