An Exponential Formula Lower Bound for Hamiltonian Cycle via Recursive Magnification

We prove that every Boolean formula computing the Hamiltonian Cycle function HAMn on n-vertex graphs has size 2^Ω (n). The proof introduces a separator interface state for Hamiltonian cycles, establishes a same-state stitchability theorem (mixed left–right graphs with matching interface states remain Hamiltonian), and a different-state collision fatality theorem (degree- profile mismatches in mixed graphs force formula errors). These are combined with a carrier-edge funnel recurrence: we fix a chromatic edge-partition frontier derived from a balanced red/blue vertex coloring and maintain a single bichromatic carrier edge throughout the recursion. At each level, the carrier edge is extended to a degree-visible two-terminal switch block whose two local states are both globally realizable, producing two pattern blocks that no monochromatic 1-rectangle can straddle. Suppressing the block’s internal vertices consumes the old carrier and replaces it with a new one of the same restriction cost, so the background restriction mass stays constant across the entire recursion depth. The Aho–Ullman–Yannakakis protocol- partition characterization converts this into the binary recurrence Γ (n) ≥ 2 Γ (n − 2), yielding L (n) ≥ 2^Ω (n).