visitCount
plain-language theorem explainer
Counts how many cycle representatives of a face-configuration flip walk land in a given admissible orbit, dropping the closing return so only open-cycle posts are tallied. Holography and census-pricing arguments cite it to record once-per-closure versus multiple-sheet over-posting on the witness 8-walk. The body is a short list filter-and-length over walk visits.
Claim. Given a face configuration $s$, a flip sequence $fs$, and an admissible orbit listed by natural values, $\mathrm{visitCount}(s,fs,\mathrm{orbit})$ is the number of intermediate walk configurations (the full visit list with the closing return dropped) whose packed value lies in that orbit.
background
The module prices the continued 8-tick cycle by the real turn ratio $C(T)=J(\kappa T/2\pi)$ with $J(x)=(x+x^{-1})/2-1$ (T5), not by any U(1)-phase extension of $J$. Unique zero-cost period, cover positivity, and census records all live here.
A FaceCfg is a boundary plaquette: four recognition bits on a cube face, packed as Fin 16. walkVisits s fs lists every configuration the flip walk meets, including the start. The length primitive is ordinary finite-trace length; here it is applied after filtering.
Admissible orbits are the $D_4$ sectors that the witness walk is required to post into for a complete census. Dropping the last visit removes the forced return to the start so the count is a pure cycle-representative census, not a closed-loop double-count of the basepoint.
proof idea
Definitional one-liner: build walkVisits s fs, drop the final closing configuration, keep only those $c$ with $c.\mathrm{val}$ in the orbit list, and take the resulting list length. No lemmas are applied beyond the upstream visit enumerator and ordinary list filter/length.
why it matters
Feeds the once-per-closure census theorem eight_tick_multiple_exclusion: the witness 8-walk posts each of the four admissible sectors exactly once, while its $n=2$ retrace posts each exactly twice. That double-posting is the over-posting half of the CensusPricing premise and cannot be read off from subperiod exclusion alone (covers remain census-complete).
Also feeds witnessWalk3_census in SeamTransferCore: the triple retrace is census-complete and posts each sector exactly three times, giving absolute surplus 2 and relative surplus $2/3$ per post, which pair as $J(3)=2/3$. Together these records pin the discrete cover side of the B2/turn-ratio carrier against lattice multiples of the eight-tick octave (T7).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.