cubePeriodEight_holds
plain-language theorem explainer
Any periodic walk on the Boolean 3-cube that hits every corner must have period at least 8. Recognition papers citing the eight-tick octave (T7) use this as the pure counting half of the D=3 / 8-tick bridge. The proof is a classical pigeonhole: periodicity collapses the image to the first p residues, and an injection from the 8 corners into Fin p forces 8 ≤ p.
Claim. For every walk $w : \mathbb{N} \to (\mathrm{Fin}\, 3 \to \mathrm{Bool})$ and every period $p > 0$, if $w(n+p)=w(n)$ for all $n$ and $w$ is surjective onto the $2^3=8$ corners of the Boolean 3-cube, then $8 \le p$.
background
PublicSpine is the dual forcing surface of UnifiedForcingChain: a δ-stratified map of what Recognition Science claims is forced, without encoding cheats. Among its closed targets is the D=3 / eight-tick bridge (campaign P-d3link). The eight-tick side is not the trivial identity eight_tick = 8; it is restated as a real counting statement about walks on the 3-cube.
A walk here is a map from discrete time $\mathbb{N}$ into the Boolean 3-cube (functions $\mathrm{Fin},3\to\mathrm{Bool}$, i.e. the $2^3=8$ corners). Periodicity means the walk repeats every $p$ steps. Surjectivity means every corner appears. The RS tick $\tau_0=1$ and the octave of eight ticks are the physical reading of this discrete period once the bridge is assembled; this lemma itself is pure combinatorics.
The companion half of the bridge is dimensional (Alexander linking / unknot-complement retract forcing $D=3$). This declaration deliberately does not touch that half.
proof idea
Classical tactic proof by counting. Fix a periodic surjective walk of period $p>0$. First prove by induction on $k$ that $w(n+k\cdot p)=w(n)$ for all $k,n$, then deduce $w(n)=w(n\bmod p)$ via the division algorithm.
From surjectivity, choose for each corner $x$ a preimage and reduce it mod $p$ to define $f : (\mathrm{Fin},3\to\mathrm{Bool})\to\mathrm{Fin},p$. The mod-reduction identity shows $w\circ f = \mathrm{id}$, so $f$ is injective. Fintype cardinality then gives $8 = |\mathrm{cube}| \le p$. No external RS lemmas are required; the argument is honest pigeonhole.
why it matters
This is R0 of campaign P-d3link and the period half of the public eight-tick target. Downstream, target_eight_tick_of_bridge packages it with the D=3 linking bridge: once non-encoding linking forces $D=3$, the eight-tick bound is already proved, so the assembled target reduces to the bridge alone.
In the Recognition forcing chain this is the combinatorial content of T7 (eight-tick octave, period $2^3$). Module docs record the full D=3 / 8-tick bridge as CLOSED on the public spine: cube-period pigeonhole plus unknot-complement retract, low-dimensional vanishing, and excision forcing $D=3$. Papers that mean "what is forced" should cite this surface rather than certificate-only UFC names.
Nothing here calibrates costs, φ, or α; it only locks the discrete period lower bound that the octave reading needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.