recognition_loop_has_surjection
Every recognition loop on a list of 3-simplices includes a surjective assignment of 3-bit patterns to its positions. Researchers working on the simplicial formulation of the ledger cite this to guarantee complete coverage of local states in closed cycles. The result follows by direct extraction of the existential witness from the third conjunct of the loop predicate.
claimLet $C$ be a nonempty list of 3-simplices. If $C$ satisfies the recognition loop conditions, then there exists a surjective map $p : {Fin}(|C|) → {Pattern}_3$.
background
The module formalizes the ledger as a simplicial 3-complex rather than a fixed lattice, supplying a coordinate-free sheaf that unifies local and global J-cost. Simplex3 is the structure of a tetrahedron with four vertices in R^3 and strictly positive volume. The predicate is_recognition_loop on a list of such simplices requires a nonempty cycle, shared-face conditions, and an existential surjective pass from cycle positions to 3-bit patterns. Upstream, the Cycle structure from LedgerAlgebra supplies the closed-sequence notion, while the tick constant fixes the fundamental time quantum.
proof idea
This is a one-line wrapper that applies the definition of is_recognition_loop by selecting its third conjunct, which is already the required existential statement for the surjective pass.
why it matters in Recognition Science
The declaration is invoked by eight_tick_uniqueness to prove that any recognition loop has length at least 8, confirming the eight-tick octave as the minimal self-consistent period on a simplicial manifold. It directly supports the T7 forcing-chain step that fixes the fundamental evolution period at 2^3 ticks and feeds the uniqueness claim for the 8-tick closure cycle.
scope and limits
- Does not assert that any given list of simplices forms a recognition loop.
- Does not bound the length of the cycle.
- Does not constrain the internal geometry of the simplices beyond the loop predicate.
- Does not address global J-cost stationarity or consistency with external fields.
Lean usage
rcases recognition_loop_has_surjection hloop with ⟨pass, hsurj⟩formal statement (Lean)
89theorem recognition_loop_has_surjection {cycle : List Simplex3}
90 (hloop : is_recognition_loop cycle) :
91 ∃ pass : Fin cycle.length → Pattern 3, Function.Surjective pass := by
proof body
Term-mode proof.
92 exact hloop.2.2
93
94/-- **THEOREM: Eight-Tick Cycle Uniqueness**
95 The 8-tick closure cycle is the unique minimal sequence for a self-consistent
96 recognition loop on a simplicial manifold. -/