The Borodin–Kostochka conjecture for maximum degree at least 4583

We prove that every finite simple graph of maximum degree Δ ≥ 4583 satisfies χ ≤ max{ω, Δ − 1}. The proof combines a decomposition into large cliques and sparse neighbourhoods with a random partial colouring. Families of disjoint triples, each consisting of a clique vertex and two outside neighbours, supply repeated colours at clique vertices. We first select these families from distributions of prescribed size to control the intersections between bad-event supports. Finite exponential-moment bounds account jointly for repeated colours surviving in a neighbourhood and its root being uncoloured, and yield the numerical threshold. The finite inequalities are verified with rational arithmetic; the programs and their parameter file accompany the paper.