PeriodFromDimension
plain-language theorem explainer
Defines the fundamental recognition period as a pure function of spatial dimension: period(D) = 2^D. Anyone citing the eight-tick octave or the T7/T8 ordering should use this rather than a hardcoded 8. The body is a one-line power definition with no presupposition that D equals 3.
Claim. For each natural number $D$, the fundamental period length associated to spatial dimension $D$ is $2^D$.
background
Beltracchi's §4 objection is that the historical label "8-tick" seems to bake in $D = 3$ before dimension is forced, making the T7–T8 order look circular. This module answers that charge by separating the period from any fixed numeral.
Upstream, DimensionForcing.linking_requires_D3 already forces $D = 3$ from Alexander duality and the linking predicate on reduced cohomology $\tilde H^{D-2}(S^1;\mathbb{Z})$, with no reference to the number 8. Constants modules elsewhere pin a global $D := 3$ only after that forcing step.
The honest chain is therefore T5 (unique $J$) → T6 ($\varphi$ fixed) → T8 ($D = 3$ from linking) → T7 (period $= 2^D = 8$ as a consequence). The present definition is the dimension-generic map that makes that last arrow explicit.
proof idea
Pure definitional abbreviation: the period is the natural-number power $2^D$. No tactics, no lemmas, no numeric literal 8. Downstream equalities such as period at $D=3$ equal to 8 are then just rfl on this definition.
why it matters
This is the named hinge that dissolves the apparent T7/T8 circularity. Downstream, period_at_D1–period_at_D4 evaluate the map at small dimensions; period_eq_eight_iff_D_eq_three proves the biconditional $2^D = 8 \leftrightarrow D = 3$; FinalPeriod packages the honest direction (linking forces $D=3$, then period is defined as $2^D$); and no_period_circularity exhibits both halves side by side without ever feeding an eight-tick hypothesis into the linking argument.
In the Recognition forcing chain this is exactly the content of T7 once T8 is in place: the eight-tick octave is $2^3$, not an independent axiom. Framework landmark: T7 eight-tick octave (period $2^3$) as a corollary of T8 ($D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.