periodDimensionBidirectional
plain-language theorem explainer
The eight-tick period and the claim D = 3 are packaged as logically equivalent at the point D = 3, with the honest forcing direction running Alexander duality → dimension → period 2^D = 8. Anyone answering circularity objections to the Recognition forcing chain (Beltracchi §4) would cite this certificate. The proof is a term-mode structure inhabitant wiring five already-proved lemmas into the bidirectional master record.
Claim. There is a certificate establishing: (i) $D = 3$ implies the period $2^D$ equals $8$; (ii) $2^D = 8$ implies $D = 3$; (iii) nontrivial circle linking forces $D = 3$ with no reference to the period; (iv) the period at $D = 3$ is exactly $8$; (v) there exists a unique RS-compatible dimension.
background
This module answers Beltracchi's §4 concern that the historical label "8-tick" for T7 seems to presuppose $D = 3$, making a T7-before-T8 order circular. The fix is definitional: the period is named as a function of dimension, $2^D$, so the numeral 8 is not an a-priori input.
Upstream dimension forcing is topological. Ledger conservation requires nontrivial linking; by Alexander duality, integer linking of disjoint circles in $S^D$ exists if and only if $D = 3$ (Hatcher Thm 3.44). The theorem linking_requires_D3 proves $D = 3$ with zero reference to eight-tick structure. The honest chain order is therefore T5 (J unique) → T6 ($\varphi$ forced) → T8 ($D = 3$ from linking) → T7 (period $2^D = 8$ follows).
The two directions of the period-dimension equivalence are already theorems: from $D = 3$ one gets period 8 by substitution and reflexivity; from period 8 one recovers $D = 3$ by the elementary fact that $2^D = 8$ forces $D = 3$. Unique existence of an RS-compatible dimension is the dimension-forcing theorem.
proof idea
Term-mode construction of the master structure. Each field is filled by a named upstream result:
- period-from-dimension is
T7_from_T8(substitute $D = 3$, thenrflon $2^3 = 8$); - dimension-from-period is
T8_from_T7(unfold $2^D$, apply the power-of-two lemma); - Alexander-without-period is
linking_requires_D3from DimensionForcing (Alexander duality, no eight-tick mention); - period-at-$D=3$ is bare
rfl; - unique dimension pin is
dimension_forced.
No new mathematics is proved here; the certificate only assembles the bidirectional package.
why it matters
This is the Lean-level answer to Beltracchi §4 in outstandingissues.tex: once the period is named $2^D$ rather than the numeral 8, T7 and T8 are equivalent restatements and there is no ordering problem. The honest forcing direction is T8 → T7 (Alexander duality → dimension → period), matching the primer landmarks T7 (eight-tick octave, period $2^3$) and T8 ($D = 3$ spatial dimensions).
The structure also records that linking forces $D = 3$ independently of any period hypothesis, and that the RS-compatible dimension is uniquely pinned. Together these close the circularity diagnostic for the UnifiedForcingChain narrative. No downstream consumers are wired yet; the declaration stands as the master non-circularity certificate for the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.