eight_tick_uniqueness
plain-language theorem explainer
Any recognition loop formed by a cycle of 3-simplices in a simplicial ledger has length at least 8. Researchers deriving dimension forcing or pattern coverage bounds in Recognition Science cite this to anchor the minimal period for self-consistent recognition. The argument reduces the loop property to a surjective mapping onto 3-bit patterns and invokes the known lower bound for such coverings.
Claim. Let $L$ be a simplicial ledger. For every list $c$ of 3-simplices, if $c$ forms a recognition loop then the length of $c$ is at least 8.
background
The SimplicialLedger module represents the ledger as a collection of 3-simplices that form a manifold covering, providing a coordinate-free sheaf representation. A Simplex3 is a tetrahedron with four vertices in three-dimensional space and positive volume. A recognition loop is a nonempty closed cycle of such simplices that induces a surjective pass through all 3-bit local pattern states, per the definition is_recognition_loop.
proof idea
This is a term-mode proof. It introduces the cycle and loop hypothesis, applies recognition_loop_has_surjection to extract a surjective pass onto Pattern 3, and concludes by applying eight_tick_min to that pass and surjectivity witness.
why it matters
This theorem supplies the lower bound that feeds simplicial_loop_tick_lower_bound in DimensionForcing. It realizes the eight-tick octave (T7) in the UnifiedForcingChain for D = 3 spatial dimensions, where the period 2^3 is the minimal self-consistent cycle length. The downstream doc-comment describes it as the derived ledger lower bound for every simplicial recognition loop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.