ImageIsCircle
plain-language theorem explainer
Predicate asserting that a closed walk on the D-cube has image a circle S¹. At the present layer it is definitionally True, so any Hamiltonian closed walk satisfies it by triviality. Downstream theorems cite it as the circle-image half of the strengthened T7 route. The body is a one-line Prop abbreviation, not a topological construction.
Claim. For any dimension $D\in\mathbb{N}$ and any closed walk $W$ on the $D$-cube (a phase-indexed path through the $D$-bit pattern space), the image of $W$ is a circle. At the current predicate layer this statement is taken as definitionally true.
background
The module T7CycleRealization supplies the theorem surface for the strengthened T7/T8 dimension route: the T7 closed cycle is graph-shaped, so its realized defect is a circle $S^1$, and no closed walk in the cube graph realizes a higher sphere $S^p$ for $p\ge 2$. Smooth-topology content is kept predicate-level; only elementary finite-dimensional arithmetic is proved, matching the AlexanderDuality discipline.
A closed walk on the $D$-cube is a structure with a path $\mathrm{Fin}(2^D)\to\mathrm{Pattern},D$. Hamiltonian means the walk visits every vertex exactly once. Spatial dimension $D=3$ is the value forced upstream by T8 (and by the linking argument labeled T9 in the constants module). The eight-tick octave of T7 is the combinatorial period $2^3$ on that cube.
This definition is the circle half of that predicate surface: it names "image is a circle" without yet constructing a CW or covering-dimension model of $S^1$.
proof idea
No proof. The declaration is a definition whose body is the proposition True, parameterized by dimension $D$ and an unused closed-walk witness. Downstream goals of the form ImageIsCircle W therefore close by trivial (or exact True.intro). There is no appeal to Gray-cycle lemmas, edge-distinctness, or continuum bridges at this layer.
why it matters
It is the named target of closed_walk_image_is_circle (Part (ii): a Hamiltonian closed walk has circle image), which itself feeds t7_cycle_realizes_circle in the same module. That package is the combinatorial half of the forcing-chain step T7 (eight-tick octave) as strengthened toward T8 ($D=3$ spatial dimensions): graph-shaped closed walks realize $S^1$ and cannot realize $S^p$ for $p\ge 2$.
The definition exists so the forcing chain can cite a stable theorem name while full CW/covering-dimension formalization is deferred to a later Mathlib-backed pass. Without it, the circle-image claim would be an anonymous True goal rather than a reusable interface in the T7/T8 route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.