Holography Eight Tick Subperiod Exclusion No Subperiod One

The eight-tick minimum

In the Recognition Science framework, a boundary plaquette is a square face of a cube with one recognition bit stored at each of its four vertices. A recognition walk advances by flipping exactly one bit per tick, the Gray-code discipline of the eight-tick cube traversal. A walk is closed when it returns to its starting configuration, and census-complete when it visits at least one representative of each of the four admissible ledger-closed sectors: the empty loop, the adjacent-edge loops, the diagonal loops, and the full loop.

The declaration no_subperiod_one establishes, by exhaustive kernel enumeration, that no closed one-tick walk is census-complete. The obstruction is cardinality: a closed one-tick walk visits at most two distinct configurations, but four sectors must be met. The same argument excludes closed two-tick walks, and a parity argument excludes closed four-tick walks: single-bit flips alternate the parity of the popcount, so a closed four-walk sees at most two distinct even-parity configurations, again short of the four required sectors.

The capstone theorem minimal_census_period_eight assembles these exclusions with a witness: a closed eight-tick walk that is census-complete exists, flipping vertices 0,1,2,3,0,2,1,3 from 0000 and visiting all four sectors. Among the divisors of 8, the census-complete closed walk lengths begin exactly at 8. Identifying the recognition cycle modulo a proper divisor of 8, the discrete analog of a conical deficit 2π/n, destroys the admissible sector census.

In Recognition Science, this is the discrete half of the deficit-free-period argument for the Bekenstein-Hawking coefficient program. Combined with the continuum result that one full eight-tick cycle equals one full 2π turn, it forces the census-preserving Euclidean period to be the full 2π/κ. The declaration does not prove that the physical Euclidean continuation must preserve the census; that regularity condition at the horizon fixed point remains open. The module removes the which-sub-period freedom once census preservation is granted; it does not grant it.

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

The declaration does not prove that the physical Euclidean continuation must preserve the census. The declaration does not establish the continuum KMS window lemma, which is owned separately. The declaration does not derive the full Bekenstein-Hawking coefficient; it only removes the sub-period freedom.

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: