Holography Eight Tick Subperiod Exclusion Minimal Census Period Eight

The minimal census period

The declaration minimal_census_period_eight is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It concerns a boundary plaquette, which is a square face of a cube with one recognition bit at each of its four vertices. The framework models a recognition event as a single-bit flip, meaning one vertex changes its bit from 0 to 1 or from 1 to 0 per tick, where a tick is one discrete step of a walk. The walk is closed when it returns to its starting configuration, and it is census-complete when it visits at least one representative of each of four admissible sectors, which are the four possible orbit types of the square's symmetry group: the empty loop, the adjacent-edge loops, the diagonal loops, and the full loop.

The theorem proves, by exhaustive machine enumeration, that no closed walk of length 1, 2, or 4 can be census-complete. The obstruction for lengths 1 and 2 is cardinality: such a short walk visits at most two distinct configurations, but four sectors must be met. The obstruction for length 4 is parity: each single-bit flip alternates the parity of the number of 1-bits, so a closed 4-walk visits at most two even-parity configurations, again short of the four required sectors. The proof is a full enumeration of all 16 × 4⁴ = 4096 possible walks of length 4. In contrast, the theorem provides an explicit witness for length 8: starting from configuration 0000, flipping vertices in the sequence [0,1,2,3,0,2,1,3] visits all four sectors and returns to the start.

In plain terms, the theorem establishes that the minimal closed recognition walk that exhibits the complete admissible sector census has length exactly 8. It rules out identifying ticks modulo a proper divisor of 8, which the framework interprets as the discrete analog of a conical deficit, a missing wedge of angle 2π/n. The theorem shows that such a sub-period destroys the census, so the census-preserving period must be the full 8-tick turn. This is the discrete half of a larger argument about the Euclidean period of the recognition cycle; the continuum half is handled separately.

In Recognition Science, this result is a step toward forcing the full 2π period of the continued clock. The theorem itself does not prove that the physical Euclidean continuation must preserve the census. That condition, the regularity at the horizon fixed point, remains open and is owned by the derive captain. The theorem removes the freedom of choosing a sub-period once census preservation is granted; it does not grant that preservation.

/-- **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⟩

/-- **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⟩

What this page does not claim

This theorem does not prove that the physical Euclidean continuation must preserve the census. This theorem does not establish the full 2π period of the continued clock by itself. This theorem does not apply to walks that are not required to be closed or census-complete.

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: