Holography Eight Tick Subperiod Exclusion Census Complete

The census condition

The declaration censusComplete is a precise test on a small discrete model. The model places one recognition bit on each of the four vertices of a square face. A walk advances by flipping one bit per step, the Gray-code discipline of an eight-tick traversal. The walk is closed when it returns to its starting configuration. The test asks whether the walk visits at least one representative of each of four admissible sectors: the empty loop, the adjacent-edge loops, the diagonal loops, and the full loop. These four sectors are the ledger-closed orbits of the square's symmetry group.

The framework's machine-checked library of formal theorems proves a sharp result. For every proper divisor of 8, namely 1, 2, and 4, no closed walk of that length is census-complete. For lengths 1 and 2 the obstruction is cardinality: such a walk visits at most two distinct configurations, but four sectors must be met. For length 4 the obstruction is parity: single-bit flips alternate the parity of the number of flipped bits, so a closed 4-walk sees at most two even-parity configurations, again short of the four required sectors. The proof is a full enumeration of all 4096 possible walks, checked by the kernel's decide procedure.

Length 8 succeeds. The witness walk flips vertices in the order 0, 1, 2, 3, 0, 2, 1, 3, starting from 0000 and visiting 0, 1, 3, 7, 15, 14, 10, 8, 0. This walk meets all four sectors at configurations 0, 3, 15, and 10. The capstone theorem minimal_census_period_eight assembles these facts: among the divisors of 8, the census-complete closed walk lengths begin exactly at 8.

In Recognition Science, this discrete result feeds a larger argument about the Euclidean period of the recognition cycle. The claim is that identifying ticks modulo a proper divisor of 8, the discrete analog of a conical deficit 2π/n, destroys the admissible sector census. So a census-preserving period must be the full eight-tick turn. The theorem removes the which-sub-period freedom once census preservation is granted.

The declaration does not grant that census preservation itself. Whether the physical Euclidean continuation must preserve the census is an open problem, owned by the derive captain. The result is conditional: if the census is preserved, then the period is exactly 8. The proof says nothing about the continuum half of the argument, the KMS window lemma, which remains loop-owned.

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

The declaration does not prove that census preservation is physically required. The declaration says nothing about the continuum half of the deficit-free-period argument. The result does not establish the Bekenstein-Hawking coefficient itself.

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: