Inversion monotonicity and asymptotic enumeration of 1324-avoiding permutations with few inversions

Let A(n,k) count the 1324-avoiding permutations of length n with k inversions, and let a(k) = sumj=0k p(j)p(k-j), where p is the partition function. We prove A(n,k) ≤ A(n+1,k) for 0 ≤ k ≤ floor(n2 / [20 log2(n+1)]), for every n ≥ 1. We also prove A(n,k)/a(k) = 1 + O(log log n / log n), uniformly for 0 ≤ k ≤ π2n2 / [12(log n − (1/2)log log n + 2)2], as n tends to infinity. The same error bounds the proportion of indecomposable avoiders. For every fixed 0 < c ≤ π2/12, the error in the range k ≤ c n2/log2n is Oc(n2−π/√(3c)/log n). All logarithms are natural. The monotonicity proof extends the injection of Linusson and Verkama using a computer-assisted finite classification and explicit partition estimates. The asymptotic results have an independent proof based on partition pairs and a two-entry deletion recurrence. Finally, the weighted Schröder recurrence proves inversion monotonicity for Av(1324,1342) and its three symmetry-equivalent classes for all lengths and inversion numbers, answering Problem 8.1 of Claesson, Linusson, Ulfarsson and Verkama. The full monotonicity conjecture remains open; the larger asymptotic range does not assert monotonicity there. Version 2.0 combines and supersedes the monotonicity manuscript, version 1.1 (10.5281/zenodo.22764164), and the separately circulated asymptotic-enumeration preprint (10.5281/zenodo.22843412). Earlier versions in this series remain available. The archive contains the PDF, LaTeX source, proof notes, verification programs, recorded output, and a SHA-256 manifest. The command python -B verify_release.py repeats the finite checks. Large language models assisted with mathematical arguments, drafting, code development, and computational checks.