T75SubstratePackage
plain-language theorem explainer
Four substrate-side structural commitments for the T7.5/loop route are bundled into one Prop-valued package on spatial dimension D: cellular completion of the cube graph, integral 1-acyclicity, dimension-uniform loop entanglement, and compatibility with the realized recognition cycle. Anyone citing the T7/T8 dimension argument uses this as the single interface name for those inputs. It is a pure structure definition, not a proved theorem.
Claim. For a spatial dimension $D\in\mathbb{N}$, the T7.5 substrate package is the conjunction of: (i) a cellular completion of the cube graph in dimension $D$ (closed orientable smooth $D$-manifold, tame cube-graph embedding, retraction to the cube graph); (ii) integral $1$-acyclicity of the substrate ($H_1$ vanishes); (iii) loop entanglement (some recognized sphere dimension $p\ge 1$ whose complement carries a nontrivial homological separator); (iv) compatibility of that topological witness with the closed walk of the T7 recognition cycle.
background
The module records 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 for the required substrates).
Spatial dimension here is simply $D:\mathbb{N}$. Cellular completion (T7.5a) packages three structural clauses from the dimension paper: closed orientable smooth $D$-manifold substrate, tame cube-graph embedding, and a retraction back to the cube graph. One-acyclic substrate (T7.5c) asserts integral $H_1$ vanishing. Loop entanglement asks for some $p\ge 1$ with a nontrivial homological separator in the complement. Compatibility ties the topological witness to the closed walk produced by the T7 recognition cycle.
Upstream constants elsewhere fix $D=3$ (T8/T9 linking), but this package is parameterized uniformly in $D$.
proof idea
No proof body: this is a Prop-valued structure definition. It declares four fields, each a named substrate predicate on $D$, and nothing more. Inhabitation is supplied downstream by the trivial package witness, which fills each field from the corresponding predicate-level trivial or circle witness (cellular completion, one-acyclic, loop-entanglement circle case, compatibility).
why it matters
This is the single named interface for the T7.5 substrate package used by the T7/T8 dimension route in the forcing chain (eight-tick octave at T7, spatial $D=3$ at T8). Downstream, substrate_package_trivial builds a package witness in every dimension by assembling the four predicate-level witnesses, so later dimension-forcing arguments can depend on one object rather than four loose hypotheses.
The module is explicit that Mathlib does not yet carry the full smooth-topology proofs; the package therefore marks the structural commitments (cellular completion, 1-acyclicity, loop entanglement, cycle compatibility) that a completed Alexander/Lefschetz duality chain would discharge. It does not itself force $D=3$; it packages the substrate side of that argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.