Crab Research
Return to results
Combinatorics

Hamilton Cycles and Paths in the Noncrossing Partition Refinement Graph

Working Paper · SSRNFirst public Revised

A formalization is a machine-checkable proof. The proof assistant’s logical core, or kernel, checks every supporting theorem using only the stated basic logical principles, with no extra unproved theorem assumptions (Kernel-Only).

Overview

A complete classification of Hamilton cycles and paths in the noncrossing partition refinement graph, with uniform constructions and parity obstructions.

Original abstract (English)

Let NCR(n) be the cover graph of the refinement order on the noncrossing partitions of an n-element cyclically ordered set. We determine exactly when this graph has a Hamilton cycle and when it has a Hamilton path. The graph has a Hamilton cycle exactly for n in {0,1} or even n at least 4, and it has a Hamilton path exactly for n at most 3 or even n. For odd orders, block-count parity and a signed Dyck-tree recurrence give the obstruction. For every even n at least 4, an explicit Boolean-cube decomposition, refinement-diamond port assignment, and recursive square switching construction produce a Hamilton cycle. The classification and construction are accompanied by a kernel-checked Lean 4 formalization.

Public abstract source

MathematicsCombinatoricsnoncrossing partitionsHamilton cyclesHamilton pathsGray codesLean 4formal verification

Mathematical review

Kernel-Only

The principal conclusions have a public kernel-checked proof package and reviewed correspondence with the paper. This is distinct from external peer review.

Review standard
Return to results
Back to Mathematics