CubePeriodEight
plain-language theorem explainer
Any periodic walk on the eight corners of the 3-cube that hits every vertex must have period at least 8. This is the non-vacuous eight-tick binder on the public dual spine: the literal constant 8 is rfl-true, so the claim is restated as a counting lower bound. Cite it when assembling T7 or the D=3/eight-tick public target. Content is pure pigeonhole; the inhabiting proof lives in a sibling theorem.
Claim. For every map $w:\mathbb{N}\to\{0,1\}^3$ and every positive integer $p$, if $w(n+p)=w(n)$ for all $n$ and $w$ is surjective onto the $2^3=8$ corners of the 3-cube, then $p\ge 8$.
background
PublicSpine is the public dual of UnifiedForcingChain: a δ-stratified map of what is forced, kept separate from the Boolean certificate spine. Among its closed targets is the D=3 / eight-tick bridge (campaign P-d3link). The eight-tick half is not the constant identity eight_tick = 8, which is definitionally true and vacuous as a theorem goal.
Instead the claim is packaged as a property of walks. A walk here is a map $\mathbb{N}\to(\mathrm{Fin},3\to\mathrm{Bool})$, i.e. a sequence of corners of the unit 3-cube. Periodicity means the sequence repeats every $p$ steps; surjectivity means every one of the $2^3=8$ corners appears. The RS landmark T7 (eight-tick octave, period $2^3$) and the native tick/octave constants sit behind this binder, but the Prop itself is pure discrete counting.
Module contract: papers that mean "what is forced" cite this surface; T7/T8 must go through the Alexander linking bridge and this period half, never an encoding predicate.
proof idea
Definitional binder only: the body is the quantified Prop, not a proof term. No tactics, no lemmas applied at this declaration.
The inhabiting argument is the sibling theorem that proves the Prop. Sketch of that argument (for orientation): periodicity implies the image equals the finite initial segment of length $p$, so surjectivity onto an 8-element set forces $8\le p$ by counting (honest pigeonhole). Nothing in that proof touches the D=3 linking bridge.
why it matters
Closes the period half of the public eight-tick target. Downstream, target_eight_tick_from_D3 is exactly the conjunction of the non-encoding D=3 bridge with this Prop; DimensionEightTickOpen records that the eight-tick public target is that same conjunction. The sibling theorem that inhabits the Prop is R0 of campaign P-d3link and is cited as the period half of the assembled guidepost.
Framework landmark: T7, the eight-tick octave (period $2^3$). The module doc states the D=3 / 8-tick bridge target is CLOSED, with pieces including the unknot-complement retract, this pigeonhole binder, low-dimensional vanishing, and the excision spine for other D. Without this non-vacuous restatement, the eight-tick goal collapsed to rfl and could not carry weight in the dual surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.