is_nontrivial
plain-language theorem explainer
A configuration of length N is non-trivial precisely when at least one entry differs from the ground-state value 1. Researchers working on the T4 recognition forcing step cite this definition to separate uniform states from those that can support distinguishing operations. The definition is a direct encoding of non-uniformity with no lemmas or reduction steps required.
Claim. A configuration $c$ of length $N$ is non-trivial if there exists an index $i$ such that the $i$-th entry of $c$ is not equal to 1.
background
In the StillnessGenerative module the ground state is the uniform ledger in which every entry equals 1, the unique zero-defect state supplied by the Law of Existence (T5). InitialCondition.Configuration N is the structure whose entries map Fin N into positive scale factors; the module treats these factors as lying on the phi-ladder once non-uniformity appears. The local setting is the derivation that x = 1 is not passive equilibrium but the source of all subsequent structure, obtained strictly from T0-T8 without external assumptions.
proof idea
This is a one-line definition that directly encodes the existence of an index i in Fin N for which the corresponding entry differs from 1. No upstream lemmas are invoked; the definition serves as the primitive predicate consumed by the T4 Recognition structure and the nontrivial_closed_has_phi_structure theorem.
why it matters
The definition supplies the central hypothesis for the T4 Recognition Theorem, which states that any configuration supporting recognition events must be non-trivial, and for the T6 Closure Theorem (nontrivial_closed_has_phi_structure) that extracts phi-structure from non-trivial closed sequences. It implements the T4 step of the forcing chain: recognition requires distinguishing states and therefore forces departure from the uniform ground state. It touches the question of how the initial uniform configuration populates the phi-ladder while preserving the eight-tick periodicity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.