A Machine-Verified Bijective Proof of the Rooted Child-Factorial Catalan Identity over Spanning Trees of the Complete Graph

Let K n+1 be the complete graph on the vertex set {0, 1, ..., n}, and for a spanning tree T of K n+1 , rooted at 0, let c T (v) denote the number of children of the vertex v. We prove the exact identity: the sum, over all spanning trees T of K n+1 , of the product over vertices v of c T (v)! equals n! C n , where C n is the n-th Catalan number. Equivalently, the normalized sum (n+1)((n+1)!) -1 times the weighted tree sum equals C n exactly. The proof is bijective: pairs consisting of a spanning tree together with a linear ordering of every child set are placed in explicit bijection with vertex-labeled plane trees on n+1 nodes whose root carries the label 0. The identity arises as the exact "second-Ursell" normalization constant in the author's audit-first programme on four-dimensional SU(N) Yang-Mills existence and mass gap, where it had been isolated as a named open proposition in a public challenge repository; the present paper is self-contained combinatorics and makes no claim about that programme. The entire proof has been formalized in Lean 4 against a pinned Mathlib snapshot: the headline declarations compile with no sorry, and the kernel's axiom oracle reports exactly [propext, Classical.choice, Quot.sound]. All artifacts, including a pinned continuous-integration replay of the full verification, are public.