T7_from_T8
plain-language theorem explainer
If spatial dimension equals 3, the fundamental period length is 8. Anyone citing the honest T8→T7 direction of the forcing chain (eight-tick as consequence of D=3, not a premise) uses this. The proof is pure substitution into the definition PeriodFromDimension D := 2^D, then definitional equality.
Claim. For any natural number $D$, if $D = 3$, then the dimension-derived period $2^D$ equals $8$.
background
This module answers Beltracchi's circularity concern: the historical label "8-tick" (T7) appears to presuppose $D = 3$ (T8). The honest order is the reverse. Dimension forcing via Alexander duality (linking_requires_D3) pins $D = 3$ with no reference to the number 8; the period is then a derived quantity.
PeriodFromDimension D is defined as $2^D$. It is deliberately dimension-generic: writing the constant 8 into the definition would bake in T8. The eight-tick octave of the forcing chain is therefore $2^3$, not an independent numeric premise.
Upstream, DimensionForcing supplies the topological link that forces three spatial dimensions. Constants modules elsewhere hardcode D := 3 once that step is accepted; this theorem makes the period consequence explicit rather than assumed.
proof idea
Term-mode one-liner. Substitute the hypothesis $D = 3$ into the goal, reducing it to PeriodFromDimension 3 = 8. Unfold the definition $2^D$ and close by rfl (definitional equality $2^3 = 8$). No external lemmas are required.
why it matters
Closes the T8→T7 leg of the forcing chain: T5 (J-uniqueness) → T6 (φ) → T8 ($D = 3$ from linking) → T7 (period $= 2^D = 8$). The historical T7 clause is thereby a theorem depending on T8, not a separate premise.
Downstream it is packaged into periodDimensionBidirectional as the period_from_dim field, alongside the converse T8_from_T7 and the Alexander-duality witness that never mentions the eight-tick. That bidirectional record is the module's answer to the circularity charge: either direction may be taken as hypothesis; they are equivalent, and the topological forcing of $D$ is independent of period.
Framework landmark: T7 eight-tick octave (period $2^3$) as consequence of T8 ($D = 3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.