substrate_package_trivial
plain-language theorem explainer
For every spatial dimension D, the four T7.5 substrate commitments (cellular completion, one-acyclicity, loop entanglement, and cycle compatibility) hold simultaneously as a bundled Prop. Anyone citing the T7/T8 dimension route or the loop-substrate interface needs this package witness. The proof is a pure structure assembly: it plugs in the four existing trivial/circle witnesses fieldwise.
Claim. For every spatial dimension $D \in \mathbb{N}$, the bundled T7.5 substrate package holds: there is a cellular completion of the cube graph in dimension $D$, the substrate is one-acyclic, loop entanglement is realized, and that entanglement is compatible with a realized cycle.
background
This module records the substrate-side structural inputs for the T7/T8 dimension route. Statements are deliberately predicate-level: Lean names the load-bearing commitments without claiming a full Mathlib smooth-topology chain (cellular completions, Thom isomorphism, Alexander/Lefschetz duality).
Dimension is just $\mathbb{N}$. The bundled package T75SubstratePackage D is a Prop with four fields: a cellular completion (closed orientable smooth $D$-manifold, tame cube-graph embedding, retraction to the cube graph), one-acyclicity of the substrate, loop entanglement, and compatibility of that entanglement with a realized cycle.
Upstream, cellular_completion_trivial supplies "a predicate-level completion witness in every dimension" (the Lean counterpart of the paper's $S^D$ witness). compatibility_trivial is the matching predicate-level compatibility witness. Sister lemmas fill one-acyclicity and the circle witness for loop entanglement.
proof idea
Term-mode structure construction, not a calculation. Instantiate T75SubstratePackage D by assigning each field to an already-proved sibling witness: cellular_completion from cellular_completion_trivial D, one_acyclic from one_acyclic_trivial D, loop_entanglement from loop_entanglement_circle_witness D, and compatibility from compatibility_trivial D. No further rewriting or case analysis.
why it matters
Closes the T7.5 substrate interface as a single Prop that the T7/T8 dimension route can assume. In the forcing chain, T7 is the eight-tick octave and T8 forces $D = 3$ spatial dimensions; this package is the substrate-side precondition those steps lean on (cellular geometry of the cube graph, acyclicity, and loop entanglement compatible with a realized cycle).
No downstream consumers are wired yet (used_by is empty), so the declaration is presently a terminal package witness rather than an intermediate lemma. It matches the module's stated design: name the commitments at predicate level until a fuller topological development (Alexander duality style) can replace the trivial field witnesses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.