cycle_nondegenerate
plain-language theorem explainer
A cycle assignment on eight positions is non-degenerate precisely when at least two of the assigned real values differ. Researchers deriving the T7 eight-tick forcing and the ground-state instability theorem cite this predicate to exclude uniform configurations. The declaration is a direct existential definition with no lemmas or reduction steps.
Claim. A map $v : [8] → ℝ$ is non-degenerate when there exist indices $i,j$ such that $v(i) ≠ v(j)$.
background
The StillnessGenerative module derives from the T0–T8 chain that the unique zero-defect state x=1 cannot remain uniform. T7 requires an eight-tick octave whose period is exactly 8. The predicate records that a cycle on Fin 8 fails to be uniform. MODULE_DOC states that a uniform ledger has zero information content and cannot support recognition events, so non-trivial content must appear. Upstream results supply the period definition (phi^k) and the active-edge count A=1 used in the surrounding forcing arguments.
proof idea
The declaration is the direct definition of non-degeneracy: the existential statement that at least one pair of the eight values differs. No lemmas are invoked and no tactics are applied; it serves as the primitive predicate for the non-degeneracy theorems that follow.
why it matters
The predicate is the central hypothesis in eight_tick_forces_nontrivial (the T7 Non-Degeneracy Theorem) and feeds directly into stillness_is_creative. It encodes the requirement that the eight-tick cycle cannot collapse to period 1, thereby forcing departure from the ground state x=1. The result closes the step from T7 to the claim that stillness is generative and touches the question of how the phi-ladder is populated once the first non-trivial rung appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.