Holography Eight Tick Subperiod Exclusion No Subperiod Two

The two-tick exclusion

In the Recognition Science framework, a recognition tick is a single discrete event: one vertex of a cube face posts a bit, flipping its value from 0 to 1 or back. A walk is a sequence of such flips. The declaration no_subperiod_two is a theorem about walks of length two: it proves that no closed two-tick walk can visit all four admissible loop types on a cube face. A 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 the four ledger-closed sectors: the empty loop, the adjacent-edge loops, the diagonal loops, and the full loop. The theorem states that for every starting configuration and every pair of flips, if the walk returns to its start, then it fails to meet all four sectors.

The proof is a finite enumeration, checked by the machine. There are 16 possible starting configurations and 4 choices for each of the two flips, so 256 two-tick walks in total. The kernel verifies each one. The reason is cardinality: a closed two-tick walk visits at most two distinct configurations, but four sectors must be met. The same argument excludes closed one-tick walks. A separate parity argument excludes closed four-tick walks, because single-bit flips alternate the parity of the number of 1s, so a closed four-walk sees at most two even-parity configurations. The capstone theorem, minimal_census_period_eight, assembles all three exclusions and adds a witness: an eight-tick walk that does visit all four sectors, flipping vertices 0,1,2,3,0,2,1,3 from 0000 and passing through 0, 1, 3, 7, 15, 14, 10, 8, 0.

What this establishes is a discrete deficit-free period statement. The recognition cycle has a natural period of eight ticks, and identifying ticks modulo a proper divisor of 8 destroys the census of loop types. In the framework's holography program, this is the discrete half of an argument that the Euclidean period of the analytically continued recognition cycle is the full 2π turn, not a proper sub-multiple such as 2π/2 or 2π/4. The continuum half is a separate lemma about KMS windows, not proved here. The theorem removes the freedom of choosing a sub-period, but only once census preservation is granted; it does not grant that preservation.

What the theorem does not claim is important. It does not prove that the physical Euclidean continuation must preserve the census. That is an open problem, owned by the derive captain. It does not say anything about walks of length other than 1, 2, 4, or 8, nor about walks that are not closed. It does not assert that the eight-tick witness is unique, only that one exists. And it does not, by itself, establish the full 2π period; that requires combining this discrete result with the continuum KMS lemma. The exclusion is a precise, machine-checked fact about finite walks on a cube face, with a clear scope and a clear boundary.

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

/-- **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 theorem does not prove that the physical Euclidean continuation must preserve the census. The theorem does not establish the full 2π period by itself, only together with the continuum KMS lemma. The theorem does not assert that the eight-tick witness is unique.

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: