Counting Survivor Sets: Exponential Equivalence with Prime-Admissible Sets
Mario Raso, Daniele Venturi
math.NT
Sep 8, 2026 · v1
math.CO
TL;DR
The combinatorial private-composite-coordinates argument in the prime-admissible comparison theorem is formalized in Lean 4/Mathlib.
Abstract
For each integer $n\geq 1$, let $N(n)$ denote the number of distinct subsets of $\{2,\ldots,n+1\}$ obtained by choosing one forbidden residue class modulo each integer from $2$ to $n$; this is OEIS sequence A396595 (
https://oeis.org/A396595). Equivalently, $N(n)$ is the initial-restriction complexity of the family of global residue-profile survivor sequences. We derive a closed formula, depending on the parity of $n$, for the number of locally distinct residue profiles, and an exact inclusion–exclusion formula for profiles realizing a prescribed survivor set. We prove that $\log N(n)$ has order $n/\log n$, with any possible leading constant between $\log 2$ and $2\log 2$. For prime traces, the logarithm of their number is asymptotic to $(\log 2)n/\log n$. Our main comparison theorem shows that $N(n)$ is exponentially equivalent to the block complexity of prime-admissible subsets of an interval of length $n$. The combinatorial component of the private composite coordinates argument used in the comparison theorem is formalized in Lean 4/Mathlib. We also establish an exact structural recurrence, characterize extendibility by a residue-class covering criterion, and give a dynamic enumeration algorithm. As further illustrations of the model, we exhibit purely periodic global profiles generating prime-valued survivor sequences for which we have not identified corresponding OEIS entries.
Problem
For each n, N(n) counts distinct survivor subsets of {2,...,n+1} obtained by forbidding one residue class modulo each integer 2 to n. The goal is to determine its exact representation, asymptotic growth, and relationship to prime-admissible sets.
Approach
Local elimination sets are counted to give an explicit product formula P(n), and an inclusion-exclusion formula gives the exact number of profiles realizing each survivor set. Sieve and prime-number-theorem estimates bound log N(n) at order n/log n. A comparison theorem relates N(n) to the block complexity of prime-admissible subsets, whose combinatorial core (the private composite coordinates argument) is formalized in Lean 4/Mathlib.
Results
log N(n) has order n/log n with leading constant between log 2 and 2 log 2, and log of the number of prime traces is asymptotic to (log 2) n/log n. N(n) is shown exponentially equivalent to the block complexity of prime-admissible sets, with a structural recurrence N(n+1)=N(n)+E(n) and a dynamic enumeration algorithm.