OneAcyclicSubstrate
plain-language theorem explainer
Predicate-level witness that the recognition substrate in spatial dimension D is integrally 1-acyclic (first homology vanishes). Cited by the T7.5 substrate package and the RS-compatible-dimension checklist on the T7/T8 forcing route. The structure is presently a trivial Prop shell: its only field is True, matching the module's deliberate placeholder style until a full duality proof is wired in.
Claim. For a spatial dimension $D \in \mathbb{N}$, the substrate satisfies integral $1$-acyclicity: the load-bearing clause is that $H_1$ vanishes. At present this is recorded as a predicate-level Prop whose sole field is the trivial proposition $\top$.
background
The module T7.5 Substrate Axioms collects structural inputs for the T7/T8 dimension route. Statements are deliberately predicate-level, in the same style as Foundation.AlexanderDuality: Lean names the commitments without claiming that Mathlib already supplies the full smooth-topology chain (cellular completions, Thom isomorphism, Alexander/Lefschetz duality).
Here Dimension is simply $\mathbb{N}$, the spatial dimension parameter. Sibling T7.5a (CellularCompletion) packages a closed orientable smooth $D$-manifold, a tame cube-graph embedding, and a retraction; the present declaration is the matching T7.5c clause for integral $1$-acyclicity of that substrate.
Upstream constants fix the physical target $D = 3$ (T8 / linking), but this predicate is stated uniformly in $D$.
proof idea
Not a proved theorem: a Prop-valued structure definition. The single field is H1_vanishes : True, so any instance is obtained by supplying trivial. The in-module constructor one_acyclic_trivial does exactly that for every $D$. No homology computation or duality lemma is invoked yet; the name records the intended mathematical content for downstream packaging.
why it matters
Fills paper step T7.5c on the substrate side of the dimension route. Downstream, RSCompatibleDimension requires this field alongside linking, eight-tick synchronization ($2^D = 8$), gap-45 sync, and cellular completion; that is the checklist that forces $D = 3$ together with the T7 eight-tick octave. It is also bundled into T75SubstratePackage (with loop entanglement and cycle compatibility) and exposed on the unified forcing chain as T75c_OneAcyclic_Bridge, which asserts the predicate for every dimension once T7 is in hand.
The open gap is topological substance: the framework still needs a real vanishing theorem for $H_1$ of the completed cube-graph substrate, not just the named placeholder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.