Holography Eight Tick Subperiod Exclusion Walk End

The walk's endpoint

In the Recognition Science framework, a recognition event is a single bit flip on a boundary plaquette: a cube face with one bit per vertex. The declaration walkEnd is a simple recursive definition: given a starting configuration and a list of vertex indices to flip, it returns the configuration after all flips have been applied. For example, starting from 0000 and flipping vertices 0,1,2,3 in that order yields 1111. This is the discrete ledger of what a recognition walk does, step by step.

The function itself is trivial, but it supports a nontrivial theorem. The framework's library proves that among the divisors of 8, the smallest closed recognition walk that visits all four admissible sector types has length exactly 8. A closed walk returns to its starting configuration; a census-complete walk touches each of the four sectors: the empty loop, the adjacent-edge loops, the diagonal loops, and the full loop. The theorems no_subperiod_one, no_subperiod_two, and no_subperiod_four exclude walks of length 1, 2, and 4, respectively, by cardinality or parity arguments. The theorem eight_tick_census_witness provides an explicit length-8 walk, and minimal_census_period_eight packages all four results into a single statement.

What this establishes is a discrete exclusion principle: if you try to identify ticks modulo a proper divisor of 8, you cannot see all four sectors. This is the discrete analog of a conical deficit in the Euclidean period, and it supports the claim that the census-preserving period is the full 8-tick turn, not a sub-multiple. The proof is a machine-checked enumeration of all 4096 possible walks of length 4, so the result is exact and axiom-clean.

What walkEnd does not claim is equally important. It does not prove that the physical Euclidean continuation must preserve the census. That is an open question, owned by a different part of the program. walkEnd only shows that once census preservation is granted, the period cannot be a proper divisor of 8. It also does not prove anything about the continuum KMS window, which is a separate lemma. The function is a tool, not a conclusion.

/-- The endpoint of a flip walk from `s` through the tick sequence `fs`. -/
def walkEnd : FaceCfg → List (Fin 4) → FaceCfg
  | s, [] => s
  | s, i :: fs => walkEnd (flip s i) fs

/-- **The subperiod-exclusion capstone**: among the divisors of 8, the census-complete
closed walk lengths begin exactly at 8. Every proper divisor fails; 8 succeeds. This
is the discrete deficit-free-period statement: identifying the recognition cycle
modulo a proper divisor of 8 (the discrete conical deficit `2π/n`) destroys the
admissible sector census, so the census-preserving period is the full 8-tick turn. -/
theorem minimal_census_period_eight :
    (∀ (s : FaceCfg) (fs : Fin 1 → Fin 4),
        walkEnd s (List.ofFn fs) = s → censusComplete s (List.ofFn fs) = false) ∧
    (∀ (s : FaceCfg) (fs : Fin 2 → Fin 4),
        walkEnd s (List.ofFn fs) = s → censusComplete s (List.ofFn fs) = false) ∧
    (∀ (s : FaceCfg) (fs : Fin 4 → Fin 4),
        walkEnd s (List.ofFn fs) = s → censusComplete s (List.ofFn fs) = false) ∧
    (∃ (s : FaceCfg) (fs : Fin 8 → Fin 4),
        walkEnd s (List.ofFn fs) = s ∧ censusComplete s (List.ofFn fs) = true) :=
  ⟨no_subperiod_one, no_subperiod_two, no_subperiod_four, eight_tick_census_witness⟩

/-- **d = 1 excluded**: no closed 1-tick walk is census-complete (cardinality:
it visits at most 2 configurations; 4 orbits are required). -/
theorem no_subperiod_one :
    ∀ (s : FaceCfg) (fs : Fin 1 → Fin 4),
      walkEnd s (List.ofFn fs) = s → censusComplete s (List.ofFn fs) = false := by
  decide

/-- **d = 2 excluded**: no closed 2-tick walk is census-complete (cardinality). -/
theorem no_subperiod_two :
    ∀ (s : FaceCfg) (fs : Fin 2 → Fin 4),
      walkEnd s (List.ofFn fs) = s → censusComplete s (List.ofFn fs) = false := by
  decide

set_option maxRecDepth 4096 in
set_option maxHeartbeats 1600000 in

/-- **d = 4 excluded**: no closed 4-tick walk is census-complete. The mechanism is
parity: single-bit flips alternate popcount parity, so a closed 4-walk sees at most
2 distinct even-parity configurations, short of the 4 required orbits. The proof is
the full kernel enumeration of all 16 × 4⁴ = 4096 walks. -/
theorem no_subperiod_four :
    ∀ (s : FaceCfg) (fs : Fin 4 → Fin 4),
      walkEnd s (List.ofFn fs) = s → censusComplete s (List.ofFn fs) = false := by
  decide

/-- **d = 8 realizes the census**: a closed 8-tick flip walk exhibiting all four
admissible sectors exists. Witness: from `0000`, flip vertices `0,1,2,3,0,2,1,3`,
visiting `0 → 1 → 3 → 7 → 15 → 14 → 10 → 8 → 0` (orbits met at `0, 3, 15, 10`). -/
theorem eight_tick_census_witness :
    ∃ (s : FaceCfg) (fs : Fin 8 → Fin 4),
      walkEnd s (List.ofFn fs) = s ∧ censusComplete s (List.ofFn fs) = true := by
  exact ⟨0, ![0, 1, 2, 3, 0, 2, 1, 3], by decide, by decide⟩

What this page does not claim

This does not prove that the physical Euclidean continuation must preserve the census. This does not establish the continuum KMS window lemma. This does not derive the value of the Bekenstein-Hawking coefficient.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Holography/EightTickSubperiodExclusion.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: