ImageIsSpherePofDim
plain-language theorem explainer
Predicate that a closed walk on the D-cube has image realizing as a p-sphere. At this graph-shaped layer the only allowed value is p = 1 (a circle). T7 realization and no-higher-sphere lemmas cite it to block S^p for p ≥ 2. Definitionally just the equality p = 1.
Claim. For any dimension $D$, any closed walk $W$ on the $D$-cube, and any $p \in \mathbb{N}$, the image of $W$ realizes as a sphere of dimension $p$ if and only if $p = 1$.
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 in the cube graph realizes a higher sphere $S^p$ for $p \ge 2$. Smooth topology stays predicate-level; the file proves elementary finite-dimensional arithmetic and exposes names the forcing chain needs.
A closed walk on the $D$-cube is a phase-indexed path through the $D$-bit pattern space (one vertex label per phase in $\mathrm{Fin}(2^D)$). Spatial dimension $D$ is the constant forced to 3 by T8 elsewhere in the chain. The present predicate is the local stand-in for "image is $S^p$" before a full CW or covering-dimension formalization.
proof idea
Definitional, not a proved theorem. The body is the single proposition $p = 1$; the walk argument is unused (underscore) because, at this layer, graph-shaped closed walks admit only the circle. Downstream proofs dsimp the name and substitute.
why it matters
Supplies the exact Prop that no_higher_sphere_from_closed_walk negates for every $p \ge 2$, and that grayCycle3_no_higher_sphere specializes to the canonical 3-bit Gray cycle. The forcing-chain bridge T7_To_Realization_Bridge then records that the $D = 3$ Gray cycle realizes as a circle in any T7.5a cellular completion. This is the predicate hinge between T7 (eight-tick octave, period $2^3$) and the claim that the realized defect is $S^1$, not a higher sphere, on the way to T8 ($D = 3$). Full smooth or CW sphere structure is deferred.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.