One-Line Avoidance Under Insertion

Abstract

The first four low-arc insertions preserve one-line avoidance of 4123.

Theorem 1.1 (Pattern occurrence under insertion).

Lean statement: D5/S3/Combinatorics/ArcherCyclicTetranacciOneLine.contains_4123_insert_iff

Proof. Machine-checked in Lean as D5/S3/Combinatorics/ArcherCyclicTetranacciOneLine.contains_4123_insert_iff (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kassie Archer, Ethan Borsh, Jensen Bridges, Christina Graves, Millie Jeske (2024). Pattern-restricted cyclic permutations with a pattern-restricted cycle form. DOI: 10.48550/arXiv.2408.15000. URL: https://arxiv.org/abs/2408.15000v1.

Commentary.

For a rooted permutation word, inserting a low arc of length one through four produces a successor permutation containing 4123 exactly when the original successor permutation contains 4123.

References

• Truth anchor: D5/S3/Combinatorics/ArcherCyclicTetranacciOneLine.contains_4123_insert_iff
• Dependency: D5/S3/Combinatorics/ArcherCyclicPadovanPatterns
• Dependency: D5/S3/Combinatorics/ArcherCyclicTetranacciSuccessor