LoopEntanglement
plain-language theorem explainer
Loop-entanglement is the dimension-uniform substrate axiom that some sphere dimension p ≥ 1 has a complement carrying a nontrivial homological separator. Anyone assembling the T7.5 package or the realization bridge to T8 (D = 3) cites it. As a Prop structure it is a thin predicate placeholder; the circle case p = 1 is the intended witness.
Claim. For a spatial dimension $D\in\mathbb{N}$, loop-entanglement holds when there exists a recognized sphere dimension $p\geq 1$ whose complement carries the required nontrivial homological separator.
background
The module records T7.5 substrate-side structural inputs for the T7/T8 dimension route. Statements are deliberately predicate-level in the style of Foundation.AlexanderDuality: Lean names the load-bearing commitments without claiming a full Mathlib smooth-topology chain (cellular completions, Thom isomorphism, Alexander/Lefschetz duality).
Here Dimension is simply a natural-number spatial dimension parameter. Sibling axioms in the same package include cellular completion of the cube graph in dimension $D$ (closed orientable smooth $D$-manifold, tame cube-graph embedding, retraction) and one-acyclicity of the substrate.
Upstream constants fix the target spatial value $D = 3$ (T8 / linking), but this predicate is stated uniformly in $D$ so the forcing chain can quantify over candidate dimensions.
proof idea
Definitional Prop structure, not a proved theorem. The single field is an existence claim $\exists p:\mathbb{N},, 1\le p\land\mathrm{True}$: the second conjunct is a deliberate placeholder for the homological-separator content not yet formalized in Mathlib. The companion one-line witness loop_entanglement_circle_witness instantiates $p = 1$ (the circle) via decide and trivial, discharging the predicate at the intended minimal case.
why it matters
This is the loop-entanglement leg of the bundled T7.5 substrate package (T75SubstratePackage), which also requires cellular completion, one-acyclicity, and compatibility with the realized recognition cycle. Downstream, RSCompatibleDimension folds the package into the full RS-compatibility checklist (nontrivial linking, eight-tick $2^D = 8$, gap-45 sync, substrate axioms). The unified forcing chain uses it in T8_Via_Realization_Bridge: T7.5a/T7.5c plus loop-entanglement and cycle compatibility route to the same $D = 3$ conclusion as the surface T8 step (primer T8: three spatial dimensions; T7: eight-tick octave $2^3$). It closes the predicate interface for the realization bridge while leaving the actual duality/homology proofs as future Mathlib work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.