PeriodDimensionBidirectional
plain-language theorem explainer
Master certificate packaging the equivalence of the eight-tick period and spatial dimension three: period $2^D$ equals 8 exactly when $D=3$, Alexander duality forces $D=3$ with no period input, and a unique RS-compatible dimension exists. Cite it to discharge the Beltracchi §4 circularity worry about ordering T7 before T8. It is a structure of five Prop fields; the inhabited instance is assembled elsewhere from the one-way lemmas.
Claim. A record asserting five claims: (1) if $D=3$ then the dimension-generic period $2^D$ equals $8$; (2) if $2^D=8$ then $D=3$; (3) every natural $D$ that supports nontrivial circle linking (Alexander duality) equals $3$; (4) $2^3=8$; (5) there exists a unique $D\in\mathbb{N}$ that is RS-compatible (nontrivial linking, eight-tick sync, gap sync, cellular completion, and one-acyclic substrate).
background
Beltracchi §4 in outstandingissues.tex objects that labeling T7 as the "8-tick" step already assumes $D=3$, so placing T7 before T8 looks circular. This module answers that charge by making the period a function of dimension rather than a hardcoded eight.
PeriodFromDimension D is defined as $2^D$. No numeric 8 appears in the definition; eight is recovered only after $D$ is fixed. Independently, SupportsNontrivialLinking D is the topological predicate that $S^D$ admits disjoint circle embeddings with nonzero linking number, equivalent via Alexander duality to $\tilde H^{D-2}(S^1;\mathbb{Z})\cong\mathbb{Z}$, which holds precisely at $D=3$. That predicate never mentions the period.
RSCompatibleDimension D packages the full forcing suite: nontrivial linking, eight-tick equality, gap-sync divisibility, cellular completion, and a one-acyclic substrate. The module's honest chain is therefore T5 (J unique) → T6 (φ forced) → T8 ($D=3$ from linking) → T7 (period $=2^D=8$).
proof idea
No proof body: this is a structure whose five fields are the Prop obligations of the master certificate. Inhabitation is deferred to the sibling theorem periodDimensionBidirectional, which fills the fields by
period_from_dim := T7_from_T8(dimension three yields period eight),dim_from_period := T8_from_T7(period eight forces dimension three),alexander_no_period := linking_requires_D3(Alexander duality alone pins $D=3$),period_of_D3 := rfl(definitional $2^3=8$),dimension_uniquely_pinned := dimension_forced(unique RS-compatible dimension).
The structure itself only names the interface; the one-way lemmas do the work.
why it matters
This is the Lean-level answer to the §4 ordering concern: once the period is named $2^D$ rather than the numeral 8, T7 and T8 are logically equivalent at the point $D=3$, and the honest forcing direction is T8 → T7 (Alexander duality → dimension → period). Downstream, periodDimensionBidirectional inhabits the structure and thereby certifies non-circularity for the rest of the foundation stack.
Framework landmarks: T7 (eight-tick octave, period $2^3$) and T8 ($D=3$ spatial dimensions) from the UnifiedForcingChain. The certificate also records uniqueness of an RS-compatible dimension, tying the topological linking force to the full compatibility package (gap sync, cellular completion, one-acyclic substrate). Anyone auditing whether the historical T7 label smuggles $D=3$ should start here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.