Norin and Steiner proved the Linear Hadwiger Conjecture, χ(G) ≤ C·had(G), but with a non-optimised constant C of order 10^100. The goal is to make the constant explicit and much smaller.

Each part of the Norin–Steiner argument is reworked with explicit constants, with extensive AI-based optimisation. The changes include a refined version of Lin's theorem that yields dense, highly connected small subgraphs, an explicit chromatic-separable reduction, and an additive bootstrap in place of the multiplicative one. The final theorem is formally verified in Lean 4 with Mathlib, building on the existing Lean formalisation of the Norin–Steiner proof and its external inputs.

Every graph G satisfies χ(G) ≤ 19,885,160·had(G). The term (472/3)·126,115.1, the constant for colouring graphs of order t(log t)^{O(1)}, accounts for 99.8% of the constant. The Lean statement matches Theorem 1.3 exactly, and the Lean files are provided as arXiv ancillary files.