No Largest Derangement Limit Below One

Abstract

Bounded decreasing tails yield derangement limits cofinal below one.

The paragraph following Question 4.3 in Section 4 of D5/L/Words/vatter2026assortment asks: Is there a largest possible limit strictly less than 1? The question concerns arbitrary permutation classes, with no growth restriction. The construction below answers this question negatively. It gives limits arbitrarily close to one from below, without classifying all possible limits.

Perm(n) denotes Equiv.Perm(Fin(n)). Positions and values are numbered from zero; val is the underlying natural number of a Fin element or the underlying permutation of a subtype element, as appropriate. P(n,a) denotes tailPerm with the displayed assumption a<=n. C(k) denotes boundedTailClass(k). The containment relation Contains, the hereditary-class structure PermClass, the fixed-point-free predicate IsDerangement, and the real-valued ratio are those of D5/S1/Words/Patterns/DerangementRatioNonconvergence. Nonempty(S) means that the set S contains a permutation. Every cardinality is Fintype.card; all quotients of cardinalities or natural parameters in a real formula use their real casts.

Definition 1.1 (The two-block permutation).

$$\forall n:\mathbb{N},\forall a:\mathbb{N},a\le n⟹P\left(n,a\right):\mathrm{Perm}\left(n\right)\wedge (\forall i:\mathrm{Fin}\left(n\right),\mathrm{val}\left(P\left(n,a\right)\left(i\right)\right)=\mathrm{if}\mathrm{val}\left(i\right)<n-a\mathrm{then}a+\mathrm{val}\left(i\right)\mathrm{else}n-1-\mathrm{val}\left(i\right))$$

Formalization. D5/S1/Words/Patterns/DerangementLimitsCofinal.tailPerm (✓ std3).

Source. Repository-derived.

Commentary.

In one-based notation this is (a+1,…,n,a,…,1). The head increases through the high values and the tail decreases through the low values. The inverse sends a value j to j-a when a<=j and to n-1-j otherwise. The two branches are inverse bijections on the corresponding disjoint intervals. Either block can be empty, and length zero is included.

Theorem 1.2 (Patterns retain a bounded tail).

$$\forall m:\mathbb{N},\forall n:\mathbb{N},\forall a:\mathbb{N},a\le n⟹\forall \sigma :\mathrm{Perm}\left(m\right),\mathrm{Contains}\left(\sigma ,P\left(n,a\right)\right)⟹\exists t:\mathbb{N},t\le m\wedge t\le a\wedge \sigma =P\left(m,t\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Patterns/DerangementLimitsCofinal.pattern_tailPerm (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let f be the order embedding selecting the pattern. There is a cut b such that f(i) is in the original head exactly when i<b. To obtain it, take the least b after which every selected position is in the tail; monotonicity of f makes every earlier selected position a head position. The m-b selected tail positions inject into the original a tail positions. For i<j, the selected values increase exactly when j<b. The permutation P(m,m-b) has precisely the same comparisons. Composing one permutation with the inverse of the other gives a strictly increasing self-map of a finite chain, which is the identity. Hence the pattern equals P(m,m-b).

Definition 1.3 (The hereditary class).

$$\begin{array}{r}\forall k:\mathbb{N},C\left(k\right):\mathrm{PermClass}\\ \forall k:\mathbb{N},\forall n:\mathbb{N},\mathrm{mem}\left(C\left(k\right),n\right)=\{\pi :\mathrm{Perm}\left(n\right)\mid \exists a:\mathbb{N},a\le n\wedge a\le k\wedge \pi =P\left(n,a\right)\}\\ \forall k:\mathbb{N},\mathrm{downset}\left(C\left(k\right)\right):\forall m:\mathbb{N},\forall n:\mathbb{N},\forall \sigma :\mathrm{Perm}\left(m\right),\forall \pi :\mathrm{Perm}\left(n\right),\pi \in \mathrm{mem}\left(C\left(k\right),n\right)⟹\mathrm{Contains}\left(\sigma ,\pi \right)⟹\sigma \in \mathrm{mem}\left(C\left(k\right),m\right)\end{array}$$

Formalization. D5/S1/Words/Patterns/DerangementLimitsCofinal.boundedTailClass (✓ std3).

Source. Repository-derived.

Commentary.

Membership means being one of the permutations with tail length at most k. The preceding theorem supplies arbitrary-pattern closure: a contained pattern has tail length at most that of the containing permutation, and therefore still at most k. Membership concerns permutations themselves; different witnesses for a do not create distinct members.

Theorem 1.4 (Exact eventual counts).

$$\forall k:\mathbb{N},\forall n:\mathbb{N},2\times k+2<n⟹\mathrm{card}\left(\mathrm{mem}\left(C\left(k\right),n\right)\right)=k+1\wedge \mathrm{card}\left(\{\pi :\mathrm{mem}\left(C\left(k\right),n\right)\mid \mathrm{IsDerangement}\left(\mathrm{val}\left(\pi \right)\right)\}\right)=k$$

Proof. Machine-checked in Lean as D5/S1/Words/Patterns/DerangementLimitsCofinal.boundedTailClass_counts (✓ std3). ∎

Source. Repository-derived.

Commentary.

When n>2*k+2, every a from 0 through k has a nonempty head. Its first value is a, so these k+1 permutations are distinct and exhaust the slice. The parameter a=0 gives the identity, which has a fixed point because n>0. For a>0 a head position shifts upward by a. A tail position is at least n-a, whereas its value is less than a; the threshold separates these intervals. Thus precisely the k positive parameters give derangements. Bijections from Fin(k+1) and Fin(k) give the two displayed subtype counts. No distinctness claim is made at smaller lengths: P(n,n) and P(n,n-1) coincide when n>0.

Theorem 1.5 (Attained limits are cofinal below one).

$$\forall q:\mathbb{R},q<1⟹\exists C:\mathrm{PermClass},\exists l:\mathbb{R},q<l\wedge l<1\wedge (\forall n:\mathbb{N},\mathrm{Nonempty}\left(\mathrm{mem}\left(C,n\right)\right))\wedge \mathrm{Tendsto}\left(\mathrm{ratio}\left(C\right),\mathrm{atTop},\mathrm{nhds}\left(l\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Patterns/DerangementLimitsCofinal.exists_derangement_limit_between (✓ std3). ∎

Resolves. Problems/vatter-largest-derangement-limit-below-one (refuted) by D5/S1/Words/Patterns/DerangementLimitsCofinal.exists_derangement_limit_between.

Source. Repository-derived.

Acknowledgement. Vincent Vatter (2026). An Assortment of Problems in Permutation Patterns: Unimodality, Equivalence, Derangements, and Sorting. URL: https://arxiv.org/abs/2602.16355.

Commentary.

For a real q<1 choose a natural k greater than q/(1-q). Positive-denominator arithmetic gives q<k/(k+1)<1. Choose C(k) and this real limit. At every length P(n,0) is a member, so all slices are nonempty. The two exact counts make the ratio identically k/(k+1) for n>2*k+2, and eventual constancy gives convergence. Applying the theorem to any attained limit below one produces a larger attained limit still below one. These classes have eventually constant slice cardinality; the assertion is the arbitrary-class question. The cited source supplies the question; the construction and proof are derived here.

References

• Truth anchor: D5/S1/Words/Patterns/DerangementLimitsCofinal.boundedTailClass
• Truth anchor: D5/S1/Words/Patterns/DerangementLimitsCofinal.boundedTailClass_counts
• Truth anchor: D5/S1/Words/Patterns/DerangementLimitsCofinal.exists_derangement_limit_between
• Truth anchor: D5/S1/Words/Patterns/DerangementLimitsCofinal.pattern_tailPerm
• Truth anchor: D5/S1/Words/Patterns/DerangementLimitsCofinal.tailPerm
• Dependency: D5/S1/Words/Patterns/DerangementRatioNonconvergence
• Narrative reference: D5/S1/Words/Patterns/DerangementRatioNonconvergence