cellular_completion_trivial
plain-language theorem explainer
In every spatial dimension D, the cube graph admits a cellular completion at the structural-interface level: a closed orientable smooth D-manifold substrate, a tame embedding of the cube graph, and a retraction back onto it. Dimension-route and T7.5 package proofs cite this as the universal S^D-style witness. The proof is a pure term constructor: each clause is True, so each field is discharged by trivial.
Claim. For every spatial dimension $D \in \mathbb{N}$, there exists a cellular completion of the cube graph in dimension $D$: a closed orientable smooth $D$-manifold substrate, a tame embedding of the cube graph into that substrate, and a retraction from the substrate back onto the cube graph. At the present interface level each of these three structural clauses is recorded as the unit proposition $\mathrm{True}$.
background
Module Foundation.SubstrateAxioms 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).
Dimension is simply $\mathbb{N}$. CellularCompletion D is the T7.5a structure with three fields: a closed orientable smooth $D$-manifold substrate, a tame cube-graph embedding, and a retraction back to the cube graph. In the current framework each field has type True, so the structure is a named Prop bundle rather than a deep geometric construction. The doc-comment identifies this as the Lean counterpart of the paper's $S^D$ witness at the structural-interface level.
Upstream dimension constants elsewhere fix $D = 3$ (T8/T9), but this theorem is parametric in every $D$.
proof idea
Term-mode structure constructor. CellularCompletion D is a Prop structure whose three fields are each True. The proof supplies trivial for closed_orientable_smooth, cube_graph_embeds, and retraction_back_to_cube_graph. No lemmas are applied; the witness exists in every dimension precisely because the interface has not yet demanded nontrivial topology.
why it matters
This is the T7.5a cellular-completion leg of the substrate package that feeds the dimension-forcing chain. Downstream, substrate_package_trivial packages it with 1-acyclicity, loop entanglement, and cycle compatibility; D3_compatible uses cellular_completion_trivial 3 to show $D = 3$ is RS-compatible; and t75a_bridge_holds in UnifiedForcingChain takes it as the exists_completion field of the T7.5a bridge under the eight-tick hypothesis (T7).
In the forcing chain, T7 forces the eight-tick octave and T8 forces $D = 3$. The substrate axioms sit between those steps as the geometric interface the codimension and linking arguments need. The open gap is intentional: Mathlib does not yet carry the full smooth cellular-completion and duality proofs, so the framework keeps a predicate-level $S^D$ witness until that chain is formalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.