CellularCompletion
plain-language theorem explainer
Predicate packaging the three structural clauses of a cellular completion of the D-cube graph: closed orientable smooth D-manifold substrate, tame cube-graph embedding, and retraction onto that graph. Dimension-forcing and T7 cycle-realization routes cite it as the T7.5a substrate interface. Fields are presently True placeholders, so the object is a named Prop interface rather than a Mathlib topology proof.
Claim. For a spatial dimension $D\in\mathbb{N}$, a cellular completion of the $D$-cube graph is the conjunction of three structural clauses: the substrate is a closed orientable smooth $D$-manifold; the $D$-cube graph embeds tamely into that substrate; and there is a retraction from the substrate back onto the cube graph.
background
Module T7.5 Substrate Axioms records the substrate-side structural inputs for the T7/T8 dimension route. Statements are deliberately predicate-level, matching the Foundation.AlexanderDuality style: Lean names the load-bearing commitments without claiming that Mathlib already supplies the full smooth-topology chain (cellular completions, Thom isomorphism, Alexander/Lefschetz duality).
Here $D$ is the spatial dimension parameter (an abbreviation for $\mathbb{N}$). In the broader forcing chain, T7 forces the eight-tick octave (period $2^3$) and T8 forces $D=3$ spatial dimensions; several upstream constants already pin $D:=3$. The paper's $S^D$ witness is the geometric picture this interface stands for: a sphere-like closed orientable completion of the hypercube skeleton.
The three fields name exactly the dimension-paper clauses: closed orientable smooth substrate, tame cube-graph embedding, and retraction back to the cube graph. Sibling predicates (one-acyclic substrate, loop entanglement, compatibility with a realized cycle) bundle with this into the full T7.5 package.
proof idea
Definitional structure, not a proved theorem. Each of the three fields has type True, so inhabiting the structure is immediate once the interface is accepted. The companion theorem cellular_completion_trivial builds a witness in every dimension by filling all three fields with trivial. No Mathlib manifold, embedding, or retraction lemmas are invoked; the object is an explicit structural-interface Prop.
why it matters
This is T7.5a in the substrate package that sits between the eight-tick forcing (T7) and spatial-dimension forcing (T8). Downstream, RSCompatibleDimension requires cellular completion (with linking, eight-tick synchronization $2^D=8$, gap-45 sync, and one-acyclic substrate) as one of the RS-compatibility clauses. T75SubstratePackage bundles it with one-acyclic substrate, loop entanglement, and cycle-compatibility.
T7 cycle realization takes a cellular completion as input: t7_cycle_realizes_circle states that in such a completion, a Hamiltonian cube closed walk realizes as a circle (RealizedDefect equals Circle); grayCycle3_realizes_circle specializes to the canonical 3-bit Gray cycle at $D=3$. UnifiedForcingChain bridges (T75a_CellularCompletion_Bridge, T7_To_Realization_Bridge) thread this interface into the global forcing spine.
The open gap is geometric substance: the fields are True placeholders until a real smooth-topology development discharges closed-orientable-smooth, tame embedding, and retraction for the intended substrate class (paper $S^D$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.