Foundation Simplicial Ledger Eight Tick Uniqueness

The eight-tick minimum

A recognition loop, a closed cycle of steps in a discrete record of events, must pass through every one of the eight possible three-bit patterns. That requirement, formalized in the framework's machine-checked library of formal theorems, forces a hard lower bound: no such loop can be shorter than eight steps. The theorem eight_tick_uniqueness states this bound for any loop built from tetrahedral volume elements, the atoms of the ledger's geometry.

The proof is short and direct. A recognition loop is defined to carry a surjective pass over the eight three-bit patterns, meaning each pattern appears at least once. Since there are eight distinct patterns and each step of the loop can realize only one pattern, the loop must contain at least eight steps. The theorem recognition_loop_has_surjection extracts that surjective pass from the loop's definition, and the bound follows by counting.

In Recognition Science, this eight-step floor is the seed of the framework's eight-tick cycle, the minimal closed sequence of recognition states. The framework models the ledger as a simplicial complex, a manifold-like covering by tetrahedra, rather than a fixed cubic grid. Within that model, the theorem shows the eight-tick cycle is not a chosen convention but a forced consequence of requiring every local pattern to appear in a self-consistent loop.

What the theorem does not claim is just as important. It does not prove that an eight-step loop exists, only that none can be shorter. It does not show that every recognition loop is exactly eight steps; longer loops are allowed. And it does not establish that the simplicial ledger's covering property holds, which the framework marks as an open scaffold, not a proved result. The uniqueness in the name refers to the minimal length, not to a unique loop shape.

/-- Every recognition loop carries a surjective pattern pass. -/
theorem recognition_loop_has_surjection {cycle : List Simplex3}
    (hloop : is_recognition_loop cycle) :
    ∃ pass : Fin cycle.length → Pattern 3, Function.Surjective pass := by
  exact hloop.2.2

/-- **THEOREM: Eight-Tick Cycle Uniqueness**
    The 8-tick closure cycle is the unique minimal sequence for a self-consistent
    recognition loop on a simplicial manifold. -/
theorem eight_tick_uniqueness (_L : SimplicialLedger) :
    ∀ cycle : List Simplex3,
    (is_recognition_loop cycle) → 8 ≤ cycle.length := by
  intro cycle hloop
  rcases recognition_loop_has_surjection hloop with ⟨pass, hsurj⟩
  exact eight_tick_min pass hsurj

What this page does not claim

The theorem does not prove that any eight-step loop exists, only that none is shorter. The theorem does not show every recognition loop has exactly eight steps; longer loops are permitted. The simplicial ledger's manifold covering property remains an open scaffold, not a proved result.

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/Foundation/SimplicialLedger.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: