Pair-selecting sequences for an involution of the alphabet
Abstract
Let σ be a self-inverse permutation of the alphabet ℤₖ, acting letterwise on k-ary n-tuples. A pair-selecting sequence for σ of span n is a cyclic sequence whose n-windows are pairwise distinct and contain at most one tuple out of each pair {a,σ a}. Its period is at most (kⁿ-fⁿ)/2, where f is the number of letters fixed by σ. Mitchell and Wild asked whether this bound is always attained and recorded a single failure, at k=2, n=2. We answer the question negatively: for every fixed-point-free σ with k ≡ 2 (mod 4) the bound fails at span 2, and at k=6,10,14 the true maximum is exactly k²/2-1. We then show that this is the only obstruction of its kind, by proving that every parity obstruction coming from a σ-reversed two-colouring of the de Bruijn vertices is vacuous at every span at least 3. In the positive direction we exhibit, for every alphabet, every fixed-point-free σ and every span at least 3, an explicit balanced σ-transversal of the de Bruijn graph, which reduces the question at those spans to connectivity alone; and we prove that at every odd span the bound is attained exactly, for every alphabet and every fixed-point-free σ. At even span we prove that no rotation-closed selection rule can attain the bound, which explains why no general method was available there, and we give a general lower bound with an exact deficit. Finally we settle the five smallest even cases at k=2 that Mitchell and Wild leave open and record exact maxima in 37 further cases. All statements are machine-checked in Lean 4.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-08-30 15:34 UTC
File fingerprint
0b55f3b79736bb9dfa90ec336dae07d1240960729a13d8f84acdfc7ede8b58d7
Claim ledger
Stated results
perm-01known2026-08-22
trivial bound 2m + #fixed <= kⁿ at an arbitrary self-inverse conflict map
perm-02routine2026-08-22
the question depends only on the conjugacy class of sigma
perm-03candidate2026-08-26
bound NOT attained at n = 2 for every fixed-point-free involution with k = 2 (mod 4) – section 7's question answered negatively
perm-04candidate2026-08-23
exact maxima k²/2 - 1 at k = 6, 10, 14, n = 2
perm-05candidate2026-08-23
k = 2 swap attained at n = 6, 8, 10, 12, 14 – section 7's named open cells
perm-06candidate2026-08-23
37 exact cells for involution classes the paper never treats, 3 <= k <= 10
perm-07known2026-08-22
k = 2 swap at odd n and n = 4
perm-08routine2026-08-22
sigma = negFin recovers IsNAS definitionally; k = 10, t = 4 reproduces the landed 48, 496
perm-09candidate2026-08-23
the cut criterion: a σ-reversed 2-colouring of the vertices with 4 ∤ cut count forbids the trivial bound, at every span
perm-10candidate2026-08-23
no cut obstruction exists at any span ≥ 3, for any alphabet and any involution
perm-11candidate2026-08-23
an explicit balanced σ-transversal at every span ≥ 3, every fixed-point-free involution, every k
perm-12known2026-08-22
span-2 classification swept to k = 14: attained iff not (f = 0 and k ≡ 2 (mod 4)), 49 involution classes, 0 disagreements
This ledger entry is reported in prose and is not bound to a Lean theorem.perm-13routine2026-08-22
spans 3 and 4, every involution class with k ≤ 12: 72 cells, all attained
This ledger entry is reported in prose and is not bound to a Lean theorem.perm-14known2026-08-22
the source's own k = 2 data reproduced from its definitions: 32 sequences at n = 4 forming one class up to rotation/reversal/complement ([11110010]), none at n = 2
This ledger entry is reported in prose and is not bound to a Lean theorem.perm-16candidate2026-08-23
the trivial bound is attained at every odd span, for every alphabet and every fixed-point-free involution — §7's question answered for f = 0
perm-17routine2026-08-23
Euler for a rotation-closed edge set: any rotation-closed, connected, conflict-free set of n-tuples is the window set of a pair-selecting sequence
perm-18routine2026-08-23
balance is free: a rotation-closed edge set is balanced in the de Bruijn graph
perm-19candidate2026-08-23
no rotation-closed selection can attain the bound at even span, for any involution with a transposition
perm-20candidate2026-08-23
the construction at every span, with an exact deficit: 2·period + #(ψ-balanced tuples) = kⁿ
perm-21candidate2026-08-23
cells past the search frontier, from the theorem rather than a witness: k = 12, n = 3; k = 6, n = 5; k = 2, n = 15, 21
perm-22routine2026-08-23
controls: no reversing colouring for an involution with a fixed point; the majority rule is short at even span
perm-23routine2026-08-26
negative controls for the section-7 predicate: every clause of IsPAS isolated by a sequence that only that clause rejects, the headline refuted one step in each direction, the parity obstruction shown not to overreach where 4 divides k, and the sigma-parameterization shown to be genuine
N1known2026-08-22
The closed-form upper bound on the period, for every alphabet size and every span at once
N2known2026-08-22
36 maximal witnesses: a negative avoiding sequence of period exactly (kⁿ - s)/2 at 36 parameter pairs
N3known2026-08-22
Headline: the exact maximum period at 36 cells, largest 9841
N4known data2026-08-22
Validation: the source's own three sequences, and the bound reproduced by brute force at two cells
N5routine2026-08-22
Negative controls: each clause of the predicate isolated, and the headline refuted at m+1 and m-1
N6routine2026-08-22
Frontier: generation is free, the wall is the quadratic Lean witness check, and memory never binds
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Sigma-avoiding sequences over Zₖ: cyclic sequences whose n-windows are pairwise distinct and never conflict under a self-inverse conflict map sigma. The case sigma = negation is the negative avoiding sequences of arXiv:2603.25286 (Mitchell-Wild), solved there in closed form and carried here to 36 exact cells; a general self-inverse sigma is the question that paper's section 7 poses open, and this family answers it in several directions. All Lean lives in LeanProblemSpec/NegAvoid/, sorry-free.
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7