DimensionEightTickOpen
plain-language theorem explainer
The public D=3 and eight-tick targets are definitionally the content-typed Alexander linking bridge and the 3-cube period bound. Cite this disclosure in place of the old Nonempty T7/T8 certificate names on the dual public spine. Both targets are already proved elsewhere; the structure only records the honest binder equalities. Inhabitation is by reflexivity on those definitions.
Claim. The public $D=3$ target equals the proposition that an Alexander linking bridge exists (circle $H_1$ available, nontrivial linking detected in $S^3$, and only dimension $3$ admits the obstruction). The public eight-tick target equals the conjunction of that same $D=3$ target with the statement that every positive-period surjective walk on the $2^3$ corners of the $3$-cube has period at least $8$.
background
PublicSpine is the dual forcing surface to UnifiedForcingChain: a $\delta$-stratified map meant for papers and loops that ask what is forced, without replacing the Boolean certificate spine. Contract rules ban encoding predicates; T8/T7 must go through a content-typed linking bridge, never arithmetic sphere-linking.
The Alexander linking bridge packages three proved pieces: $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, detection of nontrivial complement homology for some embedded circle in $S^3$ (unknot complement retract), and the uniqueness claim that DetectsNontrivialLinking $D$ forces $D=3$ (excision spine plus arc-complement acyclicity). The eight-tick half is CubePeriodEight: any periodic surjective walk on Fin-3 Boolean corners has period at least 8 (honest pigeonhole; the literal $2^3=8$ is rfl-vacuous).
The two named targets are defs kept as gates: target_D3 is Nonempty of the bridge; target_eight_tick is that target conjoined with CubePeriodEight. Both are closed as theorems in PublicSpineLinkingClosure (campaign P-d3link).
proof idea
No proof body: this is a Prop structure whose fields are definitional equalities. The first field asserts that the public D=3 target is literally Nonempty AlexanderLinkingBridge. The second asserts that the public eight-tick target is literally the conjunction of that D=3 target with CubePeriodEight. Downstream inhabitation (dimensionEightTickOpen_holds) discharges both fields by rfl.
why it matters
This is the honest citation surface for the closed D=3 / eight-tick bridge on the public dual spine. The module doc marks that bridge CLOSED (campaign P-d3link, 2026-07-18): AlexanderLinkingBridge is fully inhabited with zero sorry and only standard axioms, with no appeal to encoding or to DimensionForcing.linking_requires_D3. Downstream, dimensionEightTickOpen_holds packages the disclosure as a theorem.
In the Recognition forcing chain this stands in for T8 (D=3 spatial dimensions) and T7 (eight-tick octave, period $2^3$). The doc-comment states the point directly: citing this structure replaces Nonempty T7_EightTick_Forced / Nonempty T8_Dimension_Forced. Panel K1 keeps the binder content-typed so an encoding cheat cannot discharge it; only real topology closed the targets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.