FinalPeriod
plain-language theorem explainer
A final-period datum packages a spatial dimension D with Alexander-duality linking evidence that pins D, then defines the fundamental period as 2^D. Anyone resolving the T7/T8 ordering (Beltracchi §4 circularity) cites this record. It is pure structure packaging: the period field is the one-line definition PeriodFromDimension applied to the stored D.
Claim. A final-period datum is a pair $(D, h)$ where $D \in \mathbb{N}$ and $h$ is evidence that $D$ supports nontrivial linking (Alexander duality). Its period is defined by $\mathrm{period}(D,h) := 2^D$. In particular the period is not an independent input; it is computed from the dimension.
background
Beltracchi §4 objects that the historical label "8-tick" seems to presuppose $D = 3$, so placing T7 before T8 looks circular. This module answers that charge by making the dependence explicit.
PeriodFromDimension D is defined as $2^D$ with no hardcoded 8: "Writing 8 here would be wrong in general; writing $2^D$ is dimension-generic." The linking predicate SupportsNontrivialLinking D is the topological statement (from DimensionForcing) that reduced cohomology $\tilde H^{D-2}(S^1;\mathbb{Z})$ is nontrivial; linking_requires_D3 forces $D = 3$ from that predicate alone, with zero reference to eight-tick structure.
Honest forcing order is therefore T5 (J unique) → T6 (φ forced) → T8 ($D = 3$ from linking) → T7 (period $= 2^D = 8$ follows). The structure below is the packaging of that honest direction.
proof idea
No proof content. FinalPeriod is a structure with two fields: a natural number $D$ and a term of SupportsNontrivialLinking D. The associated period map is the one-line definition PeriodFromDimension F.D, i.e. $2^D$. Downstream, the canonical instance fills $D := 3$ and supplies D3_has_linking.
why it matters
This record is the module's third deliverable: packaging the claim that the period is 8 because $D = 3$ (honest direction), with the $D = 3$ step sourced from Alexander duality rather than from the 8-tick itself.
It feeds final_period_canonical, the canonical instance at $D = 3$ whose period evaluates to 8 as a consequence, not a premise. Together with period_eq_eight_iff_D_eq_three and no_period_circularity, it closes the Beltracchi §4 objection and reorders the forcing chain so T8 precedes T7. Framework landmark: T8 ($D = 3$ spatial dimensions) and the eight-tick octave as $2^D$, not as an independent axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.