T8_from_T7
plain-language theorem explainer
If the fundamental period equals 8, spatial dimension must be three. Anyone citing the T7–T8 equivalence or the non-circularity of the eight-tick octave uses this converse. The proof unfolds the period-as-power-of-two definition and applies the elementary uniqueness lemma that $2^D=8$ forces $D=3$.
Claim. For any natural number $D$, if the period determined by dimension equals $8$ (i.e. $2^D = 8$), then $D = 3$.
background
This module answers Beltracchi's §4 concern: labeling T7 as an "8-tick" seems to presuppose $D=3$, so ordering T7 before T8 looks circular. The honest chain is the reverse. Alexander duality forces $D=3$ with no reference to the number 8; the period is then defined as $2^D$ and equals 8 only as a consequence.
PeriodFromDimension D is the dimension-generic definition $2^D$. It does not hardcode 8. Upstream, power_of_2_forces_D3 states exactly: if $2^D=8$ then $D=3$, proved by finite case analysis on $D$. The historical T7 claim (period equals 8) is therefore a minimal restatement of T8 ($D=3$), not an independent premise.
proof idea
One-line term proof. Unfold PeriodFromDimension in the hypothesis so $2^D=8$ is exposed, then apply power_of_2_forces_D3, which matches on $D\in{0,1,2,3}$ and discharges the impossible cases by norm_num, leaving $D=3$ by reflexivity.
why it matters
Closes the converse half of the T7/T8 equivalence inside the forcing chain. Downstream, periodDimensionBidirectional packages both directions: T7 from T8 and this theorem as dim-from-period, together with Alexander duality (linking_requires_D3) as the period-free source of $D=3$. That record is the Lean-level answer to the §4 circularity worry: once the period is named $2^D$ rather than the numeral 8, T7 and T8 are equivalent at $D=3$, and the honest forcing order is T8 then T7. Framework landmarks: T7 (eight-tick octave, period $2^3$) and T8 ($D=3$ spatial dimensions).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.