{"id":"palomar/PALOMAR-2026-10-01-000014","url":"https://github.com/ulfarsson/public-12453/tree/d6133070300db0fd1d229f3e4566067ef1fc6efa/formal/Av12453","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-01-000014-v1.json","repo":"https://github.com/ulfarsson/public-12453","tags":["math.CO","msc:05A05","msc:05A15","msc:68W40","msc:68V15","permutation-patterns","enumerative-combinatorics","recurrences","formalization"],"score":0,"title":"Counting recurrences for the permutation classes Av(1342) and Av(12453)","trust":"high","domain":"math.CO","source":"palomar","authors":["Henning Arnór Skeggi Úlfarsson"],"reviews":0,"subject":"math.CO","summary":"For a permutation pattern τ, let Av_n(τ) be the set of permutations of length n that avoid τ. This formalization proves, for every n, that four recurrences from the source paper compute |Av_n(1342)| and |Av_n(12453)|. For 1342 they are the one-threshold recurrence W and the scalar kernel recurrence G, and for 12453 the literal two-threshold recurrence H and the transfer-kernel recurrence G. These are the cases d = 1 and d = 2 of the paper's counting recurrences for the classes Av(12...d ⊕ 231), the direct sum of an increasing pattern and 231, whose kernel form gives polynomial-time…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-01","reactions":{},"formalized":true,"formalizes":[{"title":"Protected tails and polynomial-time enumeration of permutations avoiding a direct sum of an increasing pattern and 231","identifier":"arXiv:2609.15642","relationship":"formalizes"}]}