no_period_circularity
plain-language theorem explainer
Every spatial dimension that admits nontrivial circle linking equals 3, and the period at dimension 3 is exactly 8. Cite this to discharge Beltracchi's circularity objection that the eight-tick label presupposes D = 3. The proof is a two-component pair: the topological linking theorem plus definitional reflexivity of 2^3.
Claim. Every natural number $D$ that supports nontrivial linking of closed curves satisfies $D = 3$, and the dimension-derived period at $D = 3$ equals $8$ (i.e. $2^3 = 8$). The linking half is independent of any eight-tick hypothesis.
background
Beltracchi §4 objects that labeling T7 as the "8-tick" forces $D = 3$ before T8 is proved, so the historical order T7 before T8 looks circular. This module answers that charge by making the period a pure function of dimension.
PeriodFromDimension D is defined as $2^D$, with no hardcoded 8. SupportsNontrivialLinking D is the topological predicate that $S^D$ admits disjoint $S^1$-embeddings with nonzero linking number, decided by Alexander duality: $\tilde H_1(S^D \setminus S^1) \cong \tilde H^{D-2}(S^1) \cong \mathbb{Z}$ if and only if $D = 3$. Upstream, linking_requires_D3 is the T8 primary theorem: any $D$ supporting nontrivial linking equals 3, proved from Alexander duality with zero reference to the eight-tick or gap-45.
The honest forcing order is therefore T5 (J unique) → T6 (φ forced) → T8 ($D = 3$ from linking) → T7 (period $= 2^D = 8$ follows).
proof idea
Term-mode pair constructor. The left conjunct is exactly the upstream theorem linking_requires_D3 (Alexander duality: SupportsNontrivialLinking implies $D = 3$). The right conjunct is rfl on the definition PeriodFromDimension 3 := 2^3, which reduces to $8$ by arithmetic. No further tactics; the non-circularity is exhibited by the statement itself, which never mentions an eight-tick hypothesis.
why it matters
Closes the Beltracchi §4 circularity objection inside the Foundation layer. It packages the two independent routes to $D = 3$ that the module doc and the following bidirectional-confirmation comment emphasize: the primary topological route (Alexander duality → linking → $D = 3$) and the secondary arithmetic observation that $2^D = 8$ forces $D = 3$. Neither route presupposes the other; agreement is a consistency check.
In the Recognition forcing chain this locks T8 before T7: dimension is pinned first, and the eight-tick octave is the consequence $2^3 = 8$, not a premise. Downstream usage is currently empty (diagnostic exhibit), but sibling theorems period_eq_eight_iff_D_eq_three, FinalPeriod, and two_independent_forcings sit on the same non-circular footing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.