bibkey: kagey2024a378495
authors: Peter Kagey
year: 2024
title: "OEIS A378495: derangements with no k-cycles"
doi: null
url: https://oeis.org/A378495
claim: "On source-agreeing columns 2<=k<=n, T(n,k) counts derangements in S_n with no k-cycles; the source sets T(n,1)=0, and two FORMULA conjectures concern T(n,n-2)-T(n,n) and T(n,n-1)-T(n,n-2)."
strata_touched:
  - D5/S3/Combinatorics/Derangements/TerminalDifference
  - D5/S3/Combinatorics/Derangements/AdjacentDifferenceRefutation
license: citation-only
triage: anchor

The derangement triangle A378495

Verified locator

Source: https://oeis.org/A378495

Source and exact questions

The internal entry, revision 70, defines the triangle read by rows: on the source-agreeing columns $2\le k\le n$, $T(n,k)$ is the number of derangements in $S_n$ with no $k$-cycles. The source separately sets its first column $T(n,1)$ to zero. Its offset is 1,5. The author line attributes the entry to Peter Kagey, 29 November 2024. The FORMULA field states:

Conjecture: T(n,n-2) - T(n,n) = (n-3)!(n-4)(n-1)/2 for n >= 5.

Conjecture: T(n,n-1) - T(n,n-2) = abs(A238474(n-4)) for n >= 4.

The history records the adjacent formula in revision 59 and the terminal formula in revision 60. Revision 70 retains both as conjectures. The second question uses the zero-offset sequence in Lang’s note.

Mathematical correspondence

TerminalDifference.D is the finite set of permutations of Fin n moving every label. Relabelling Fin n by $\{1,\dots ,n\}$ gives the source’s symmetric group without changing cycle lengths or cardinalities. T filters this actual set by absence of a cycle factor of support size $k$; noCycle_iff identifies that predicate with absence of $k$ from the multiset of nontrivial cycle lengths. The filter agrees with the source for $2\le k\le n$. At $k=1$, the source convention is the explicit value zero, while this total formal extension has $T(n,1)=|D(n)|$ because fixed points are already excluded. The terminal target columns $n-2,n$ are at least three for $n\ge 5$, and the adjacent target columns $n-1,n-2$ are at least two for $n\ge 4$, so both identities use source-agreeing columns.

The two source differences use rational subtraction after casting the natural cardinalities. Factorials and index subtractions are natural operations; division by two and the formula for A238474 use the rationals. No conjectured cardinality formula is assumed in defining $T$.

Suppliers and search scope

At repository pin 0a10157da355f1825f38212dd4c2869925ae6785, the bounded qualification found no exact A378495/A238474 result in D5, Blueprint, Library or Problems, including relevant private helpers. Existing ArrowWilfCountingCore.card_noFixed and PerfectMatchingCount.card_fixedPointFreeInvolution concern different counts and do not settle either displayed formula.

The actual suppliers are Mathlib’s derangement predicate, Equiv.Perm.cycleType_of_card_le_mem_cycleType_add_two, Equiv.Perm.card_of_cycleType_singleton and Equiv.Perm.card_of_cycleType_mul_eq at revision 56a005855ea17e0b0958f73ec801ae140b0a1679, with Lean v4.35.0. They are applied directly in the existing proofs. No additional Lean package or adapted third-party source is used. Mathlib is Apache-2.0; this note quotes source statements only.

The bounded external screen recorded in #23899 and #23900 found no exact answer in the searched GitHub issues, formal-conjectures, MathDB or Crossref results. OpenAlex’s direct record W7221756528 reported zero citations. OpenAlex search and Semantic Scholar returned HTTP 429; those are search gaps, not negative results. The qualification identifier is 6ae3b4a25ddca22148d0ce74.

Kallat v1, section 9.2 and the supplementary catalogue’s sec:open, leaves these stronger identities outside its proved results. Its identifier also appears in unrelated repository dossiers; no whole-paper absence claim is justified.

Result and limits

The terminal formula is proved for every $n\ge 5$. The literal adjacent formula is refuted by $n=5$, where the two sides are 20 and 6. These are separate questions. The result does not refute Kallat’s proved congruences, establish a corrected shift, or supply a global novelty or priority claim. The detailed statements, admission boundaries and unfinished audit are in the two Problems dossiers. Literature completeness remains ASSUMED-UNVERIFIED.