Symmetric chains in noncrossing partition lattices

Every noncrossing partition lattice of a finite well-generated complex reflection group admits a symmetric chain decomposition. This answers the saturated-chain part of Question 1.1 of Mühle, first posted in September 2015. We give a computer-assisted proof for the exceptional types H₄, G₃₃, G₃₄, E₆, E₇, and E₈. The other irreducible types follow from the work of Simion–Ullman, Reiner, Bessis–Corran, and Mühle. Explicit chain certificates are checked against exact reflection-group models; exhaustive rank descent certifies that their graphs are the full absolute-order intervals. Reflection-preserving automorphisms and a constructive product decomposition give every Coxeter element and every reducible group. Lean verifies the general interval-closure, product, and transfer lemmas. The finite group calculations and the published classification and decomposition results remain external inputs. No symmetric Boolean decomposition is asserted for the new exceptional cases. Computer-assisted; not yet reviewed by experts. Produced by AI models under the author's direction.