Hamilton Cycles in the Noncrossing Partition Refinement Graph

Let NC_R(n) be the cover graph of the refinement order on the noncrossing partitions of an n-element cyclically ordered set. Thus an edge merges two blocks, or reverses such a merge by splitting one block. We determine exactly when this graph has a Hamilton cycle. For odd n >= 3, block-count parity is a bipartition and a signed Dyck-tree recurrence gives color-class difference (-1)^(m+1) Cat_m at n = 2m+1, so a Hamilton cycle is impossible. For every even n >= 4, we give one uniform construction. A noncrossing partition is encoded bijectively by a noncrossing partial matching Q and a Boolean mask on the unmatched nonroot points. Each fixed Q is therefore an odd-dimensional hypercube and carries a cyclic reflected Gray code. Deleting the lexicographically first chord makes the matchings into a rooted tree. For every tree edge we exhibit an explicit refinement diamond; an injective port assignment makes all selected cube edges disjoint. Recursive square switching then joins all Boolean cycles into one Hamilton cycle. With the formal convention for singleton graphs, the complete classification for all natural n is that NC_R(n) is Hamiltonian if and only if n is 0 or 1, or n is even and n >= 4. The construction, the odd obstruction, the small cases, and the final classification are formalized in Lean 4. The publication theorem has no project axiom; its axiom audit is exactly [propext, Classical.choice, Quot.sound].