Archer-Bourne Decomposition

Abstract

The permutations avoiding 312 and 321 are exactly the direct sums of cyclic rotations indexed by compositions, and the cube criterion gives the corresponding counting identity.

Definition 1.1 (The pattern 312).

$p_{312} : P er m (F in (3)) := [2, 0, 1] .$

Formalization. D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.pattern312 (✓ std3).

Source. Repository-derived.

Acknowledgement. Kassie Archer, Noel Bourne (2026). Pattern avoidance in compositions and powers of permutations. DOI: 10.46298/dmtcs.17199. URL: https://arxiv.org/abs/2505.05218v3.

Commentary.

The zero-based values two, zero, one define the permutation pattern 312.

Definition 1.2 (The pattern 321).

$p_{321} : P er m (F in (3)) := [2, 1, 0] .$

Formalization. D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.pattern321 (✓ std3).

Source. Repository-derived.

Acknowledgement. Kassie Archer, Noel Bourne (2026). Pattern avoidance in compositions and powers of permutations. DOI: 10.46298/dmtcs.17199. URL: https://arxiv.org/abs/2505.05218v3.

Commentary.

The zero-based values two, one, zero define the permutation pattern 321.

Definition 1.3 (Avoidance of 312).

$\forall n \in N, \forall π \in P er m (F in (n)), (A v o i d s_{312}) (π) := \neg C o n t ain s (p_{312}, π) .$

Formalization. D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.Avoids312 (✓ std3).

Source. Repository-derived.

Acknowledgement. Kassie Archer, Noel Bourne (2026). Pattern avoidance in compositions and powers of permutations. DOI: 10.46298/dmtcs.17199. URL: https://arxiv.org/abs/2505.05218v3.

Commentary.

This is the negation of the generic pattern-containment predicate at the permutation 312.

Definition 1.4 (Avoidance of 321).

$\forall n \in N, \forall π \in P er m (F in (n)), (A v o i d s_{321}) (π) := \neg C o n t ain s (p_{321}, π) .$

Formalization. D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.Avoids321 (✓ std3).

Source. Repository-derived.

Acknowledgement. Kassie Archer, Noel Bourne (2026). Pattern avoidance in compositions and powers of permutations. DOI: 10.46298/dmtcs.17199. URL: https://arxiv.org/abs/2505.05218v3.

Commentary.

This is the negation of the generic pattern-containment predicate at the permutation 321.

Theorem 1.5 (Positive rotation sums avoid both patterns).

$\forall d \in L i s t (N), (\forall i \in F in (l e n g t h (d)), 0 < d_{i}) \Rightarrow ((A v o i d s_{312}) (ro t a t i o n S u m P er m (d)) \land (A v o i d s_{321}) (ro t a t i o n S u m P er m (d))) .$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.rotationSumPerm_avoids_312_321 (✓ std3). ∎

Citation. Kassie Archer, Noel Bourne (2026). Pattern avoidance in compositions and powers of permutations. DOI: 10.46298/dmtcs.17199. URL: https://arxiv.org/abs/2505.05218v3.

Commentary.

A list of positive block sizes determines a direct sum of cyclic rotations. Archer and Bourne’s Lemma 3.1 gives the avoidance direction of this characterization.

Definition 1.6 (Rotation sum indexed by a composition).

$\forall n \in N, \forall c \in C o m p os i t i o n (n), ro t a t i o n S u m C o m p os i t i o n (c) : P er m (F in (n)) := t r an s p or t (ro t a t i o n S u m P er m (b l oc k s (c)))_{\sum_{i \in F in (l e n g t h (b l oc k s (c)))} b l oc k s (c)_{i} = n} .$

Formalization. D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.rotationSumComposition (✓ std3).

Source. Repository-derived.

Acknowledgement. Kassie Archer, Noel Bourne (2026). Pattern avoidance in compositions and powers of permutations. DOI: 10.46298/dmtcs.17199. URL: https://arxiv.org/abs/2505.05218v3.

Commentary.

The sum equation carried by a Mathlib composition transports the list-level rotation sum to a permutation of the required finite interval.

Theorem 1.7 (Every composition gives an avoider).

$\forall n \in N, \forall c \in C o m p os i t i o n (n), (A v o i d s_{312}) (ro t a t i o n S u m C o m p os i t i o n (c)) \land (A v o i d s_{321}) (ro t a t i o n S u m C o m p os i t i o n (c)) .$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.rotationSumComposition_avoids_312_321 (✓ std3). ∎

Citation. Kassie Archer, Noel Bourne (2026). Pattern avoidance in compositions and powers of permutations. DOI: 10.46298/dmtcs.17199. URL: https://arxiv.org/abs/2505.05218v3.

Commentary.

Every block of a composition is positive, so the associated rotation sum avoids both 312 and 321.

Theorem 1.8 (Archer-Bourne decomposition).

$\forall n \in N, \forall π \in P er m (F in (n)), ((A v o i d s_{312}) (π) \land (A v o i d s_{321}) (π)) \Leftrightarrow (\exists c \in C o m p os i t i o n (n), π = ro t a t i o n S u m C o m p os i t i o n (c)) .$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.avoids_312_321_iff_exists_rotationSumComposition (✓ std3). ∎

Citation. Kassie Archer, Noel Bourne (2026). Pattern avoidance in compositions and powers of permutations. DOI: 10.46298/dmtcs.17199. URL: https://arxiv.org/abs/2505.05218v3.

Commentary.

A permutation avoids 312 and 321 exactly when it is the direct sum of the cyclic rotations determined by a composition of its size. This is Archer and Bourne’s Lemma 3.1.

Theorem 1.9 (Uniqueness of the composition).

$\forall n \in N, \forall c, e \in C o m p os i t i o n (n), ro t a t i o n S u m C o m p os i t i o n (c) = ro t a t i o n S u m C o m p os i t i o n (e) \Rightarrow c = e .$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.rotationSumComposition_injective (✓ std3). ∎

Citation. Kassie Archer, Noel Bourne (2026). Pattern avoidance in compositions and powers of permutations. DOI: 10.46298/dmtcs.17199. URL: https://arxiv.org/abs/2505.05218v3.

Commentary.

The boundary set consists of zero and exactly the positions x + 1 for which pi(x) <= x. Equal rotation sums therefore have equal compositions; together with the decomposition theorem, this is the bijection identified after Lemma 3.1.

Theorem 1.10 (The Archer-Bourne counting equality).

$\forall n \in N, c a r d ({π \in P er m (F in (n)) : (A v o i d s_{312}) (π) \land (A v o i d s_{321}) (π) \land \neg (C o n t ain s_{2143}) (π^{3})}) = c a r d ({c \in C o m p os i t i o n (n) : c a r d ({i \in F in (l e n g t h (b l oc k s (c))) : b l oc k s (c)_{i} \neq = 1 \land b l oc k s (c)_{i} \neq = 3}) \leq 1}) .$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.card_avoids_312_321_cube_2143_eq_compositions (✓ std3). ∎

Resolves. Problems/archer-bourne-cube-2143-count (proved) by D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.card_avoids_312_321_cube_2143_eq_compositions.

Source. Repository-derived.

Acknowledgement. Kassie Archer, Noel Bourne (2026). Pattern avoidance in compositions and powers of permutations. DOI: 10.46298/dmtcs.17199. URL: https://arxiv.org/abs/2505.05218v3.

Commentary.

The decomposition and its uniqueness identify the 312/321 avoiders with compositions. The frozen cube criterion restricts this bijection on both sides to exactly the displayed exceptional-part condition.

References

Truth anchor: D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.Avoids312
Truth anchor: D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.Avoids321
Truth anchor: D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.avoids_312_321_iff_exists_rotationSumComposition
Truth anchor: D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.card_avoids_312_321_cube_2143_eq_compositions
Truth anchor: D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.pattern312
Truth anchor: D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.pattern321
Truth anchor: D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.rotationSumComposition
Truth anchor: D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.rotationSumComposition_avoids_312_321
Truth anchor: D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.rotationSumComposition_injective
Truth anchor: D5/S3/ConceptDynamics/PatternAvoidance/ArcherBourneDecomposition.rotationSumPerm_avoids_312_321
Dependency: D5/S1/Words/Patterns/DerangementRatioNonconvergence
Dependency: D5/S3/ConceptDynamics/PatternAvoidance/RotationSumPowerPatternAvoidance

Keyboard shortcuts

trureturing — Discovering truth

Archer-Bourne Decomposition

Abstract

References