Exact 6-cut rigidity and small-order superconnectivity for the 6-regular case of Dirac's k=4 problem

Dirac asked in 1970 whether for every \(k\ge 4\) there is a \(k\)-vertex-critical graph without critical edges; Jensen settled all \(k\ge 5\), and only \(k=4\) remains open. Following Skottová and Steiner, call a graph \(G\) a \((4,1)\)-graph if \(\chi(G)=4\), \(\chi(G-v)=3\) for every vertex \(v\), and \(\chi(G-e)=4\) for every edge \(e\); they proved \(\delta(G)\ge 6\) and \(\lambda(G)\ge 6\) for every \((4,1)\)-graph and asked whether a 6-regular \((4,1)\)-graph exists. We prove three results about this 6-regular case. Theorem A (computational): there is no 6-regular 4-vertex-critical graph on \(n\le 15\) vertices, except for a unique graph (up to isomorphism) on \(n=13\), whose 13 critical edges form a Hamilton cycle; hence any 6-regular \((4,1)\)-graph has at least 16 vertices. Theorem B: in a 6-regular \((4,1)\)-graph every 6-edge-cut is either the edge star of a vertex or has both shores of size at least 15; consequently every 6-regular \((4,1)\)-graph on at most 29 vertices is super-6-edge-connected. Theorem C (all sizes): no shore of a nontrivial 6-edge-cut in a 6-regular \((4,1)\)-graph induces a bipartite graph; more generally, a shore whose deficiency is concentrated on two vertices forces them to receive equal colours in every proper 3-colouring. The proof of Theorem B rests on an exact classification of the \(3\times 3\) cut matrices of 6-edge-cuts in \((4,1)\)-graphs (exactly 21 matrices, five types up to row/column permutations) together with a boundary-shortfall lemma; the unique near-miss is \(K_{3,3,3}\) minus a rainbow 3-matching. Several supporting lemmas are machine-checked in Lean 4/Mathlib.