PeriodFromDimension_def
plain-language theorem explainer
By definition, the fundamental recognition period attached to spatial dimension D is exactly 2^D, with no numeric 8 baked in. Anyone auditing the T7/T8 ordering (Beltracchi §4 circularity) cites this to keep the period dimension-generic. The proof is pure reflexivity: the equality is the definition itself.
Claim. For every natural number $D$, the fundamental period length determined by spatial dimension $D$ equals $2^D$.
background
Recognition Science historically labels the discrete ledger cycle an "8-tick" octave. Beltracchi §4 objects that writing "8" before forcing $D=3$ looks circular: the period seems to presuppose the dimension it is meant to follow from.
This module separates the two. PeriodFromDimension is defined as the pure power $2^D$, with no special case at three. Upstream, DimensionForcing.linking_requires_D3 already forces $D=3$ from Alexander duality (nontrivial reduced cohomology $\tilde H^{D-2}(S^1;\mathbb{Z})$), without ever mentioning the number 8. The honest chain is therefore T5 (J unique) → T6 (φ) → T8 ($D=3$ from linking) → T7 (period $=2^D=8$).
Sibling facts then specialize: at $D=1,2,3,4$ the periods are 2, 4, 8, 16, and period equals 8 if and only if $D=3$.
proof idea
One-line term proof by rfl. The left-hand side is the definition PeriodFromDimension D := 2^D, so the equality is definitional and needs no lemmas.
why it matters
Closes the definitional half of the anti-circularity package in Foundation.PeriodDependsOnDimension. Without a named, dimension-generic period, the historical T7 label "eight-tick" looks like a premise rather than a consequence of T8. This theorem makes the dependence explicit: the period is a function of $D$, and the value 8 appears only after $D=3$ is forced by linking.
It underwrites the bidirectional equivalence period_eq_eight_iff_D_eq_three, the FinalPeriod record (period is 8 because $D=3$), and the diagnostic no_period_circularity. Framework landmark: T7 (eight-tick octave, period $2^3$) is demoted from independent axiom to corollary of T8 ($D=3$). No downstream consumers are wired yet; the declaration is infrastructure for the reordered forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.