Positions after Crossing Insertion

Abstract

Crossing insertion gives explicit positions for both occurrences.

Theorem 1.1 (Positions under crossing insertion).

Lean statement: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveInc.crossing_positions

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveInc.crossing_positions (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Sergi Elizalde, Amya Luo (2024). Pattern avoidance in nonnesting permutations. DOI: 10.48550/arXiv.2412.00336. URL: https://arxiv.org/abs/2412.00336v6.

Commentary.

After the 121 crossing insertion, the first occurrence of j plus one is at position one if j began the original word and otherwise shifts by two; its second occurrence shifts by two.

References

• Truth anchor: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveInc.crossing_positions
• Dependency: D5/S3/Combinatorics/Nonnesting/NonnestingFourIncCount