Recognizable factorial words and finite holonomy
Abstract
Recognizable factorial words and finite holonomy.
Definition 1.1 (Construction).
Lean statement: D5/S1/Dynamics/Symbolic/PermutativeLifts/FactorialWords.word
Formalization. D5/S1/Dynamics/Symbolic/PermutativeLifts/FactorialWords.word (✓ std3).
Source. Repository-derived.
Commentary.
The words begin with the single letter a at level zero. At level n+1 they concatenate (n+1)! copies of the zero-type level-n word and (a+1)(n+1)! copies of the one-type word. The same unbounded sequence of words neutralizes every prescribed finite group-valued letter product once the level is large enough. The ordered holonomy multiplies the last letter on the left. Pair occurrence and length growth are used by the minimality and aperiodicity proofs.
Theorem 1.2 (Result).
Lean statement: D5/S1/Dynamics/Symbolic/PermutativeLifts/FactorialWords.word_holonomy_eq_one
Proof. Machine-checked in Lean as D5/S1/Dynamics/Symbolic/PermutativeLifts/FactorialWords.word_holonomy_eq_one (✓ std3). ∎
Source. Repository-derived.
Commentary.
The words begin with the single letter a at level zero. At level n+1 they concatenate (n+1)! copies of the zero-type level-n word and (a+1)(n+1)! copies of the one-type word. The same unbounded sequence of words neutralizes every prescribed finite group-valued letter product once the level is large enough. The ordered holonomy multiplies the last letter on the left. Pair occurrence and length growth are used by the minimality and aperiodicity proofs.