A Literal Negative Answer to Vatter’s Question 4.3

Abstract

Av(12) has one permutation per length and a nonconvergent derangement ratio.

Question 4.3 of Vincent Vatter’s arXiv:2602.16355v2 asks whether the derangement ratio converges for every permutation class. This is a literal counterexample to the question as stated; the author may have had nontrivial (e.g. infinite-growth) classes in mind. The module claims only the refutation of the universally quantified statement. The literature provenance on the two answer nodes identifies the question, not a published negative answer; the counterexample and its proof are derived here.

Perm(n) denotes Equiv.Perm(Fin(n)), with positions numbered from zero. OrderEmbedding denotes an order embedding of positions. The record field mem is the length-indexed family; downset is its displayed closure law. rev(n) denotes Mathlib’s Fin.revPerm, sending i to n-1-i. Every cardinality is Fintype.card. The quotient defining ratio is real division after casting both natural cardinalities to the reals. Length zero is included.

Definition 1.1 (Pattern containment).

$$\forall k,n:\mathbb{N},\forall \sigma :\mathrm{Perm}\left(k\right),\forall \pi :\mathrm{Perm}\left(n\right),\mathrm{Contains}\left(\sigma ,\pi \right)\iff (\exists f:\mathrm{OrderEmbedding}\left(\mathrm{Fin}\left(k\right),\mathrm{Fin}\left(n\right)\right),\forall i,j:\mathrm{Fin}\left(k\right),(\sigma \left(i\right)<\sigma \left(j\right)\iff \pi \left(f\left(i\right)\right)<\pi \left(f\left(j\right)\right)))$$

Formalization. D5/S1/Words/Patterns/DerangementRatioNonconvergence.Contains (✓ std3).

Source. Repository-derived.

Commentary.

An order embedding selects positions and preserves the relative order of the selected values in both directions.

Definition 1.2 (Permutation classes as downsets).

$$\mathrm{PermClass}=\{C\mid (\mathrm{mem}\left(C\right):(n:\mathbb{N})\to \mathrm{Set}\left(\mathrm{Perm}\left(n\right)\right))\wedge (\mathrm{downset}\left(C\right):\forall k,n:\mathbb{N},\forall \sigma :\mathrm{Perm}\left(k\right),\forall \pi :\mathrm{Perm}\left(n\right),\pi \in \mathrm{mem}\left(C,n\right)⟹\mathrm{Contains}\left(\sigma ,\pi \right)⟹\sigma \in \mathrm{mem}\left(C,k\right))\}$$

Formalization. D5/S1/Words/Patterns/DerangementRatioNonconvergence.PermClass (✓ std3).

Source. Repository-derived.

Commentary.

This record has exactly the family mem and the proof field downset. The displayed record description gives the full type of both fields.

Definition 1.3 (Fixed-point-free permutations).

$$\forall n:\mathbb{N},\forall \pi :\mathrm{Perm}\left(n\right),\mathrm{IsDerangement}\left(\pi \right)\iff (\forall i:\mathrm{Fin}\left(n\right),\pi \left(i\right)\ne i)$$

Formalization. D5/S1/Words/Patterns/DerangementRatioNonconvergence.IsDerangement (✓ std3).

Source. Repository-derived.

Commentary.

This is membership in Mathlib’s derangements set, whose definition is the displayed universal inequality.

Definition 1.4 (The decreasing permutation class).

$$\begin{array}{r}\forall n:\mathbb{N},\mathrm{mem}\left(Av12,n\right)=\{\pi :\mathrm{Perm}\left(n\right)\mid (\forall i,j:\mathrm{Fin}\left(n\right),i<j⟹\pi \left(j\right)<\pi \left(i\right))\}\\ \mathrm{downset}\left(Av12\right):\forall k,n:\mathbb{N},\forall \sigma :\mathrm{Perm}\left(k\right),\forall \pi :\mathrm{Perm}\left(n\right),\pi \in \mathrm{mem}\left(Av12,n\right)⟹\mathrm{Contains}\left(\sigma ,\pi \right)⟹\sigma \in \mathrm{mem}\left(Av12,k\right)\end{array}$$

Formalization. D5/S1/Words/Patterns/DerangementRatioNonconvergence.Av12 (✓ std3).

Source. Repository-derived.

Commentary.

A pattern of a decreasing permutation is decreasing: the position embedding takes i<j to f(i)<f(j), and the value-order equivalence transfers the reversed inequality back to the pattern. This supplies the downset field. Strict decrease is exactly avoidance of the increasing pattern 12.

Theorem 1.5 (The unique member at every length).

$$\forall n:\mathbb{N},\forall \pi :\mathrm{Perm}\left(n\right),\pi \in \mathrm{mem}\left(Av12,n\right)\iff \pi =\mathrm{rev}\left(n\right)$$

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

Source. Repository-derived.

Commentary.

Composing a decreasing permutation with Fin.rev is strictly increasing. Mathlib’s StrictMono.apply_eq on a finite linear order makes that composition the identity; applying reversal again identifies the permutation.

Theorem 1.6 (The middle-position criterion).

$$\forall n:\mathbb{N},\forall i:\mathrm{Fin}\left(n\right),\mathrm{rev}\left(n\right)\left(i\right)=i\iff 2\times \mathrm{val}\left(i\right)+1=n$$

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

Source. Repository-derived.

Commentary.

The equality of Fin values is n-(i.val+1)=i.val. The bound i.val<n turns this into 2*i.val+1=n, with natural subtraction.

Theorem 1.7 (Parity decides derangements).

$$\forall n:\mathbb{N},\mathrm{IsDerangement}\left(\mathrm{rev}\left(n\right)\right)\iff \mathrm{Even}\left(n\right)$$

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

Source. Repository-derived.

Commentary.

At odd length the proof constructs the position with value n div 2, proves it is in Fin(n), and uses the middle-position criterion to exhibit a fixed point. At even length that criterion is impossible. The empty permutation is a derangement by vacuity.

Theorem 1.8 (One member at every length).

$$\forall n:\mathbb{N},\mathrm{card}\left(\mathrm{mem}\left(Av12,n\right)\right)=1$$

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

Source. Repository-derived.

Commentary.

The membership characterization identifies each length slice with the singleton containing reversal.

Theorem 1.9 (Count of derangements).

$$\forall n:\mathbb{N},\mathrm{card}\left(\{\pi :\mathrm{mem}\left(Av12,n\right)\mid \mathrm{IsDerangement}\left(\mathrm{val}\left(\pi \right)\right)\}\right)=\mathrm{if}\mathrm{Even}\left(n\right)\mathrm{then}1\mathrm{else}0$$

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

Source. Repository-derived.

Commentary.

The underlying length slice is a subsingleton. At even length the proof constructs its derangement member; at odd length any alleged member contradicts the parity criterion.

Definition 1.10 (The derangement ratio).

$$\forall C:\mathrm{PermClass},\forall n:\mathbb{N},\mathrm{ratio}\left(C,n\right)=\frac{\mathrm{real}\left(\mathrm{card}\left(\{\pi :\mathrm{mem}\left(C,n\right)\mid \mathrm{IsDerangement}\left(\mathrm{val}\left(\pi \right)\right)\}\right)\right)}{\mathrm{real}\left(\mathrm{card}\left(\mathrm{mem}\left(C,n\right)\right)\right)}$$

Formalization. D5/S1/Words/Patterns/DerangementRatioNonconvergence.ratio (✓ std3).

Source. Repository-derived.

Commentary.

The numerator counts the subtype of members that are derangements. The denominator counts the entire length slice. Real division is total; for Av(12) the denominator is always one.

Theorem 1.11 (The alternating ratio).

$$\forall n:\mathbb{N},\mathrm{ratio}\left(Av12,n\right)=\mathrm{if}\mathrm{Even}\left(n\right)\mathrm{then}1\mathrm{else}0$$

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

Source. Repository-derived.

Commentary.

Substituting both cardinalities gives one at even length and zero at odd length. Thus the positive-length sequence begins 0,1,0,1.

Theorem 1.12 (Av(12) has no ratio limit).

$$\neg (\exists L:\mathbb{R},\mathrm{Tendsto}\left(\mathrm{ratio}\left(Av12\right),\mathrm{atTop},\mathrm{nhds}\left(L\right)\right))$$

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

Resolves. Problems/vatter-question-4-3-derangement-ratio (refuted) by D5/S1/Words/Patterns/DerangementRatioNonconvergence.vatter_question_4_3_answer_no.

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

Commentary.

Both index maps k to 2k and k to 2k+1 tend to atTop. The corresponding ratio subsequences are constantly one and zero. Uniqueness of real limits would force a putative common limit to equal both, a contradiction.

Theorem 1.13 (The universal question is false).

$$\exists C:\mathrm{PermClass},\neg (\exists L:\mathbb{R},\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/DerangementRatioNonconvergence.exists_permClass_ratio_not_convergent (✓ std3). ∎

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

Commentary.

Choose the downset Av(12). This refutes the question with no additional growth assumption; it makes no claim about restricted variants.

References

• Truth anchor: D5/S1/Words/Patterns/DerangementRatioNonconvergence.Av12
• Truth anchor: D5/S1/Words/Patterns/DerangementRatioNonconvergence.Contains
• Truth anchor: D5/S1/Words/Patterns/DerangementRatioNonconvergence.IsDerangement
• Truth anchor: D5/S1/Words/Patterns/DerangementRatioNonconvergence.PermClass
• Truth anchor: D5/S1/Words/Patterns/DerangementRatioNonconvergence.av12_mem_iff
• Truth anchor: D5/S1/Words/Patterns/DerangementRatioNonconvergence.card_av12
• Truth anchor: D5/S1/Words/Patterns/DerangementRatioNonconvergence.card_derangements_av12
• Truth anchor: D5/S1/Words/Patterns/DerangementRatioNonconvergence.exists_permClass_ratio_not_convergent
• Truth anchor: D5/S1/Words/Patterns/DerangementRatioNonconvergence.ratio
• Truth anchor: D5/S1/Words/Patterns/DerangementRatioNonconvergence.ratio_av12
• Truth anchor: D5/S1/Words/Patterns/DerangementRatioNonconvergence.rev_fixed_iff
• Truth anchor: D5/S1/Words/Patterns/DerangementRatioNonconvergence.rev_isDerangement_iff
• Truth anchor: D5/S1/Words/Patterns/DerangementRatioNonconvergence.vatter_question_4_3_answer_no