simplicial_loop_tick_lower_bound
plain-language theorem explainer
Every simplicial recognition loop on a ledger of 3-simplices requires a cycle of length at least eight ticks. Researchers deriving spatial dimension from the Recognition Science forcing chain cite this bound to anchor the minimal period before identifying it with 2^D. The proof is a one-line wrapper that invokes the eight-tick uniqueness theorem and simplifies against the constant definition of eight_tick.
Claim. For any simplicial ledger $L$ and any list $c$ of 3-simplices such that $c$ forms a recognition loop, the length satisfies $8 ≤ |c|$.
background
The Dimension Forcing module derives D = 3 from topological linking and synchronization constraints. A simplicial ledger is built from 3-simplices; a recognition loop is a nonempty closed cycle of such simplices that induces a surjective map from cycle positions onto the 3-bit pattern states. The constant eight_tick is defined as 8, matching the fundamental octave period in RS-native units where one tick is the base time quantum τ₀ = 1.
proof idea
The proof is a one-line wrapper that applies the eight_tick_uniqueness theorem from SimplicialLedger to the supplied cycle and loop hypothesis, then uses simpa to rewrite against the definition of eight_tick.
why it matters
This bound supplies the minimal cycle length required by the eight-tick octave (T7) in the forcing chain, directly supporting the identification 8 = 2^3 that forces D = 3. It precedes sibling results such as eight_tick_forces_D3 and power_of_2_forces_D3. The module document ties the bound to the requirement that only three dimensions permit stable topological conservation through non-trivial linking of curves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.