no_higher_sphere_from_closed_walk
plain-language theorem explainer
Any closed walk on the D-cube fails to realize as a sphere of dimension p whenever p ≥ 2. Cited by the T7 Gray-cycle specialization that rules out higher spheres for the canonical 3-bit cycle. The proof is a one-line arithmetic contradiction: the image-is-sphere predicate is defined to hold only at p = 1.
Claim. For every natural number $D$, every closed walk $W$ on the $D$-cube, and every integer $p \ge 2$, the image of $W$ does not realize as a sphere of dimension $p$.
background
The module strengthens the T7/T8 dimension route: the T7 closed cycle is graph-shaped, so its realized defect is a circle $S^1$, and no closed walk on the cube graph realizes a higher sphere $S^p$ for $p \ge 2$. Smooth-topology content stays predicate-level; the module proves elementary finite-dimensional arithmetic and exposes the theorem names the forcing chain needs.
A closed walk on the $D$-cube is a phase-indexed path through the $D$-bit pattern space. The predicate "image realizes as a sphere of dimension $p$" is, at this layer, simply the equality $p = 1$: the only sphere dimension a graph-shaped closed walk is allowed is the circle. Spatial dimension $D$ is forced to 3 by T8 elsewhere in the foundation stack; this lemma is parametric in $D$ and does not need that specialization.
proof idea
Term-mode proof by contradiction. Assume the image-is-sphere predicate holds for the given walk and $p$. Unfolding the definition yields $p = 1$. The hypothesis $2 \le p$ then contradicts $p = 1$ by elementary arithmetic (omega). No graph-theoretic lemmas are invoked; the result is pure definitional arithmetic at the predicate layer.
why it matters
Part (iv) of the T7 cycle-realization surface: closed walks on graph-shaped cubes cannot realize higher spheres. Downstream, grayCycle3_no_higher_sphere instantiates it on the canonical 3-bit Gray cycle, the concrete T7 eight-tick object (period $2^3$). Together with the companion claim that a Hamiltonian T7 closed walk realizes as a circle, this pins the realized defect to $S^1$ and blocks $S^p$ for $p \ge 2$, feeding the strengthened T7/T8 dimension route toward $D = 3$. Full CW/covering-dimension content is deferred to a later Mathlib-backed pass; this lemma supplies the exact name the forcing chain already expects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.