Hamiltonian
plain-language theorem explainer
A closed walk on the D-cube is Hamiltonian when its phase-indexed path hits every vertex exactly once. The predicate is bijectivity of the map Fin(2^D) → Pattern D. T7 cycle-realization theorems cite it to pin the eight-tick octave as a genuine Hamiltonian cycle whose realized defect is a circle. One-line Prop definition; no proof obligations.
Claim. Let $W$ be a closed walk on the $D$-dimensional hypercube, given as a path $W:\mathrm{Fin}(2^D)\to\{\text{$D$-bit patterns}\}$. Then $W$ is Hamiltonian if and only if this path map is bijective (every vertex is visited exactly once).
background
Module T7CycleRealization supplies the graph-shaped half of the strengthened T7/T8 dimension route: the T7 closed cycle lives on the cube graph, its realized defect is a circle $S^1$, and no closed cube walk realizes a higher sphere $S^p$ for $p\ge 2$. Smooth topology stays predicate-level; the module proves the finite arithmetic and exposes the names the forcing chain needs.
A ClosedWalkOnCube D is a phase-indexed path Fin(2^D) → Pattern D through the $D$-bit pattern space (the vertices of the hypercube). The eight-tick octave of T7 is the $D=3$ case: period $2^3=8$. Upstream dimension constants fix spatial $D=3$ via T8/T9.
"Hamiltonian" here is the graph-theory sense (Hamiltonian cycle), not the classical energy functional. The predicate is kept at Prop level until a generic edge API is factored out of Patterns.GrayCycle.
proof idea
Pure definition: the predicate is definitionally Function.Bijective W.path. No tactics, no lemmas. Bijectivity of a map out of a finite type of cardinality $2^D$ into the $D$-cube vertex set is exactly the statement that every vertex appears once in the closed walk.
why it matters
This is the naming hinge for the T7 cycle story. Sibling theorems (t7_cycle_realizes_circle, closed_walk_image_is_circle, no_higher_sphere_from_closed_walk, edge_distinct_of_dim_ge_two) quantify over Hamiltonian closed walks to conclude that the realized defect is a circle and cannot be a higher sphere. That feeds the forcing-chain landmark T7 (eight-tick octave, period $2^3$) and the T7/T8 dimension route toward $D=3$.
Downstream cosmology uses (e.g. structural sphaleron-rate arguments about Hamiltonian cycles on $K_4$) reuse the same cycle language. Classical Action.Hamiltonian energy machinery is a separate namespace collision; this definition does not supply conjugate momenta or Noether conservation.
Keeps the module aligned with the AlexanderDuality discipline: elementary finite facts now, full CW/covering-dimension pass later.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.