walkEnd
plain-language theorem explainer
Recursive fold that returns the face configuration reached by applying a sequence of single-vertex bit flips, starting from a given plaquette state. Every closed-walk and census theorem in the eight-tick subperiod exclusion module evaluates endpoints through this map. The body is the standard list recursion: empty path leaves the state unchanged; each head index flips that vertex and continues.
Claim. Given a boundary face configuration $s \in \{0,\ldots,15\}$ (four recognition bits on a cube face) and a finite sequence $f_1,\ldots,f_n$ of vertex indices in $\{0,1,2,3\}$, write $\mathrm{walkEnd}(s,(f_k))$ for the configuration obtained by flipping vertex $f_1$, then $f_2$, and so on. The empty sequence returns $s$ unchanged.
background
The module EightTickSubperiodExclusion is LEG-B of the Bekenstein–Hawking coefficient program: it shows that the discrete Euclidean recognition period on the forced $D=3$ substrate is the full 8-tick turn, not a proper divisor (the discrete analog of a conical deficit $2\pi/n$).
Configurations are FaceCfg $= \mathrm{Fin},16$: one recognition bit per vertex of a cube face. A single tick is flip: XOR the bit of a chosen vertex $i\in\mathrm{Fin},4$ (Gray-code posting discipline of the 8-tick cube traversal). A walk is a list of such vertex indices; the endpoint of that walk is what this definition computes.
Downstream predicates (closed walk, census-complete visit of the four admissible $D_4$-orbits ${0}$, ${3,6,12,9}$, ${5,10}$, ${15}$) all compare or inspect configurations reached by this fold.
proof idea
Pure structural recursion on the tick list. Base case: empty list returns the starting configuration. Inductive step: apply flip at the head index, then recurse on the tail. No lemmas; the definition is the computation used by later decide proofs.
why it matters
This is the shared dynamics primitive for the discrete half of the deficit-free-period argument (forcing-chain landmark T7: eight-tick octave). Every exclusion theorem (no_subperiod_one, no_subperiod_two, no_subperiod_four) and the positive witness (eight_tick_census_witness) phrase closedness as walkEnd s fs = s. The capstone minimal_census_period_eight packages those facts: among divisors of 8, census-complete closed walks begin exactly at length 8.
Outside the module, SeamTransferCore.witnessWalk3_census and TurnRatioCarrier.eight_tick_multiple_exclusion reuse the same endpoint map on concatenated witness walks, linking the 8-tick census to surplus pairing and $J(3)=2/3$. Without a uniform walk endpoint, the kernel enumerations would not share a single closedness predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.