CompatibilityWithRealizedCycle
plain-language theorem explainer
Predicate-level compatibility of a spatial dimension D with the realized T7 recognition cycle, whose topological witness is that cycle's closed walk. Cited by the bundled T7.5 substrate package and the realization-bridge route to T8 (D = 3). Defined as a named Prop with one trivial field, matching the module's placeholder style until full topology is in Mathlib.
Claim. For a spatial dimension $D \in \mathbb{N}$, compatibility with the realized recognition cycle is the predicate asserting that the topological witness is the closed walk produced by the T7 eight-tick recognition cycle.
background
The module records substrate-side structural inputs for the T7/T8 dimension route. Statements are deliberately predicate-level, in the same spirit as the Alexander-duality scaffolding: Lean names the load-bearing commitments without claiming that Mathlib already supplies cellular completions, Thom isomorphism, or Alexander/Lefschetz duality for the needed substrate class.
Here spatial dimension is an abbreviation for $\mathbb{N}$. The T7 landmark forces the eight-tick octave (period $2^3$); the "realized recognition cycle" is that closed walk on the cube graph. Several upstream constants already pin $D = 3$ as the value forced by T8 (and by linking in related T9 material), but this predicate itself is parametric in $D$.
proof idea
Structure definition, not a proved theorem. It exposes a single field whose type is True (the closed-walk witness is recorded only at the predicate level). The sibling theorem compatibility_trivial builds an instance for every $D$ by discharging that field with trivial. No topology, graph theory, or arithmetic is executed here.
why it matters
One of four clauses in the bundled T7.5/loop substrate package (with cellular completion, one-acyclic substrate, and loop entanglement). That package is required by RS-compatible dimension (the substrate/loop package clause) and by the realization-bridge form of T8, whose doc-comment states that T7.5a/T7.5c plus loop-entanglement and compatibility route to the same $D = 3$ conclusion as the main T8 surface. Framework landmarks: T7 eight-tick octave and T8 spatial dimensions. Closes a named commitment on the substrate side without yet importing a full smooth-topology proof chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.