recognition_loop_has_surjection
plain-language theorem explainer
A list of 3-simplices that forms a recognition loop admits a surjective map from its positions to the 3-bit pattern space. Workers formalizing the ledger as a simplicial complex cite this to guarantee that every closed cycle covers all local states. The argument is a direct extraction of the third conjunct from the loop predicate.
Claim. If a finite list $c$ of 3-simplices satisfies the recognition-loop predicate, then there exists a surjective function from the index set of $c$ to the set of 3-bit patterns.
background
The module equips the ledger with a coordinate-free simplicial 3-complex whose atoms are tetrahedra (Simplex3) carrying four vertices in R^3 and positive volume. A recognition loop on such a list is defined to be nonempty, to satisfy a shared-face condition between consecutive simplices, and to induce a complete pass through Pattern 3 via a surjective assignment. The predicate therefore already encodes the surjectivity claim that the theorem isolates.
proof idea
The proof is a one-line wrapper that applies exact to the third conjunct of the hypothesis hloop, which is precisely the existential statement of the surjective pass inside the definition of is_recognition_loop.
why it matters
The result supplies the surjective pass that eight_tick_uniqueness consumes to obtain the length lower bound of 8, thereby placing the eight-tick octave inside the simplicial ledger. It therefore anchors the T7 step of the forcing chain for any recognition loop on a 3-complex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.