grayCycle3_no_higher_sphere
plain-language theorem explainer
The canonical 3-bit Gray cycle on the cube graph never realizes as a sphere of dimension p for any p ≥ 2. Dimension-route and T7/T8 forcing arguments cite this to pin the realized defect to a circle. The proof is a one-line specialization of the general closed-walk non-realization lemma to the explicit Gray walk.
Claim. For every natural number $p$ with $p \ge 2$, the image of the canonical 3-bit Gray closed walk on the 3-cube does not realize as the sphere $S^p$.
background
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 stays predicate-level; the module proves elementary finite-dimensional arithmetic and exposes the names the forcing chain needs.
ImageIsSpherePofDim is the present predicate for "closed-walk image realizes as a $p$-sphere." At this layer it is simply the assertion $p = 1$: the only sphere dimension a graph-shaped closed walk is allowed. The walk in play is grayCycle3ClosedWalk, the explicit 3-bit Gray cycle packaged as a closed walk on $Q_3$.
The general fact upstream is no_higher_sphere_from_closed_walk: for any closed walk $W$ on a cube and any $p \ge 2$, the image of $W$ does not realize as $S^p$. That lemma unfolds the predicate and obtains an immediate contradiction from $p = 1$ versus $p \ge 2$.
proof idea
One-line wrapper. Apply no_higher_sphere_from_closed_walk to the explicit Gray closed walk on $Q_3$, the dimension parameter $p$, and the hypothesis $2 \le p$. No extra arithmetic or case split is needed; the general closed-walk argument already discharges $\neg\mathrm{ImageIsSpherePofDim}$.
why it matters
Feeds the T7 realization bridge in the unified forcing chain: t7_to_realization_bridge_holds packages grayCycle3_realizes_circle together with this non-realization statement as the no_higher_sphere field of T7_To_Realization_Bridge. That bridge is the hand-off from T7 (eight-tick octave, period $2^3$) toward the T8 spatial-dimension forcing ($D = 3$).
In the Recognition Science landmarks, T7 forces the eight-tick cycle; the realization surface then asserts that the cycle's defect is topologically a circle and nothing higher. Without ruling out $S^p$ for $p \ge 2$, the dimension route could not lock the realized shape before the T8 step. The module itself notes that full CW/covering-dimension formalization is reserved for a later Mathlib-backed pass; this theorem is the exact name the chain currently consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.