Pith. sign in
module module moderate

IndisputableMonolith.Holography.EightTickSubperiodExclusion

show as:
view Lean formalization →

The Gray-code walk on a D=3 boundary plaquette has no proper subperiod: lengths 1, 2, and 4 never visit every vertex, while an explicit length-8 cycle does. Holography and octave arguments cite this to lock the recognition tick count at 2^3. The module is exhaustive case analysis on the proper divisors of eight plus a concrete census witness.

claimOn the $D=3$ recognition boundary, successive single-bit flips generate a walk whose minimal census period is $8=2^3$: no period $1$, $2$, or $4$ visits every vertex of the plaquette, while an explicit length-$8$ Gray-code cycle completes the census.

background

Recognition Science forces $D=3$ spatial dimensions and the eight-tick octave (forcing chain T7–T8) from the discrete substrate of size $2^D$. The holography panel splits the pixel area $a_{\mathrm{pix}}=4\cdot H\cdot\ell_P^2$ into three separately derived factors; PixelLocal attacks the integer factor on that forced lattice rather than by continuum postulate.

This module works on one boundary plaquette. Each recognition tick flips the bit of a single vertex (one posting per tick), the Gray-code step of the eight-tick traversal. A walk is census-complete when its visit set equals the full vertex set. The local question is whether any proper divisor of eight already finishes that census.

Upstream PixelLocal supplies the recognition-sector geometry on the $D=3$, $8=2^3$ lattice; the present file only treats period minimality of the discrete walk.

proof idea

The module first defines the single-vertex flip, the endpoint of an $n$-step walk, the set of visited vertices, a hit predicate, and census-completeness. Three short lemmas show that periods one, two, and four leave the visit set a proper subset of the eight vertices. An explicit eight-step witness is then exhibited that does complete the census. The headline result packages the three exclusions with the witness into minimality of period eight. No analytic estimates appear; the argument is finite enumeration on the hypercube skeleton.

why it matters in Recognition Science

TurnRatioCarrier imports this module so that the continued eight-tick cycle can be priced as $C(T)=J(\kappa T/2\pi)$ with the T5 cost $J(x)=(x+x^{-1})/2-1$. Without subperiod exclusion the cycle length would be ambiguous and the per-cycle recognition cost ill-defined. The result therefore anchors both the holographic integer factor and the T7 octave on an actual discrete walk, rather than by declaration. It sits between PixelLocal (substrate geometry) and the Bekenstein LEG-B pricing loop that consumes the real turn ratio.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)