eight_tick_forces_nontrivial
plain-language theorem explainer
Any non-degenerate 8-tick cycle on real values must contain at least one entry different from the initial position. Recognition Science researchers cite this to close the T7 octave step, showing that period-8 dynamics cannot collapse to a uniform state. The proof is a direct case split on the non-degeneracy witness pair.
Claim. Let $f : Fin 8 → ℝ$. If there exist $i,j$ with $f(i) ≠ f(j)$, then there exists $k$ such that $f(k) ≠ f(0)$.
background
The module derives that the ground state x=1 is unstable under the T0–T8 chain. cycle_nondegenerate is the predicate that a length-8 assignment visits at least two distinct values; a uniform assignment would have effective period 1. The upstream tick definition supplies the fundamental time quantum τ₀=1, while the 8-tick octave is the period forced by T7. PrimitiveDistinction supplies the structural conditions that recognition requires distinguishable states.
proof idea
Obtain the witness pair i,j from cycle_nondegenerate. Case on whether values i equals values 0. If equal, the inequality with j forces j to differ from 0. Otherwise i itself differs from 0. This is a one-line wrapper around the non-degeneracy hypothesis.
why it matters
It supplies the non-degeneracy step required by the StillnessGenerative derivation chain after T7 (period exactly 8) and before T6 closure onto the phi ladder. The module doc states that a degenerate cycle would contradict the period-8 requirement from Patterns.period_exactly_8, forcing departure from the zero-defect state. This lemma therefore converts the abstract octave into concrete non-trivial content on the configuration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.