is_recognition_loop
plain-language theorem explainer
A recognition loop is a non-empty list of 3-simplices that admits a surjective mapping from its positions onto all 3-bit patterns. Researchers deriving the eight-tick lower bound in the simplicial ledger cite this definition when applying the forcing chain. The declaration is a direct definition that conjoins non-emptiness, a trivial shared-face predicate, and the surjectivity condition.
Claim. A list $c$ of 3-simplices is a recognition loop if $c$ is nonempty, every index admits a shared face (formalized trivially), and there exists a surjective map from the indices of $c$ to the set of functions from a 3-element set to the booleans.
background
The module represents the ledger as a simplicial 3-complex, supplying a coordinate-free sheaf that unifies local and global J-cost. Simplex3 is the structure of a tetrahedron with positive volume that serves as the volume atom. Pattern 3 is the type Fin 3 → Bool, i.e., all 3-bit assignments, matching the finite-window definitions appearing in the Streams, Patterns, and Measurement modules.
proof idea
This is a definition, not a derived theorem. It directly assembles the three conjuncts: non-emptiness of the list, a universal quantifier whose body is an existential over a dummy Prop (always true), and an existential witness for a surjective function to Pattern 3. No upstream lemmas are invoked.
why it matters
The definition supplies the hypothesis for eight_tick_uniqueness, which concludes that every such cycle has length at least 8, and for simplicial_loop_tick_lower_bound. It encodes the eight-tick octave (T7) by requiring a complete pass through the 3-bit pattern states on the simplicial manifold. The parent theorem eight_tick_uniqueness states that the 8-tick closure is the unique minimal sequence for self-consistent recognition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.