Perfect restricted bases of size s + 1 force cyclicity

B. Bajnok, C. Berson and H. A. Just, On Perfect Bases in Finite Abelian Groups, Involve 15 (2022), 525–536, arXiv:2211.13675v1, Question 6:

Are there any noncyclic groups that have a perfect restricted s-basis of size s + 1?

The paper works with finite abelian groups and positive integers $s$. Its definition is:

A is a perfect restricted s-basis of G if each element of G can be written uniquely as the sum of at most s distinct elements of A.

Uniqueness disregards the order of the summands. The empty subset contributes the empty sum $0$.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Finite abelian group $G$ | G : Type, AddCommGroup G, Fintype G | Additive notation; no order or prime-order assumption. | | Positive integer $s$ | s : ℕ, 1 ≤ s | Exact positive range. | | A subset $A$ of size $s+1$ | A : Finset G, A.card = s + 1 | Distinct elements, without an ordering. | | At most $s$ distinct summands | A unique T : Finset G with T ⊆ A, T.card ≤ s and sum equal to the given element | Includes the empty sum. | | No noncyclic example | result : claim, concluding IsAddCyclic G | Universal negative answer to Question 6. | | Decidable equality | DecidableEq G | Computational representation of finsets; every finite group admits it classically. |

The settling declaration is D5/S3/FiniteGroups/BajnokBersonJustPerfectRestrictedBasis.result, under preregistration #19526. Its admission basis is open-problem-resolution (#19526; Proved) and its utility is none.

The source's Proposition 5 supplies cyclic examples of order $2^{s+1}-1$. Question 6 asks whether noncyclic groups also occur.

Counting proper subsets gives the order $2^{s+1}-1$, but odd order alone does not force cyclicity. The extra relation is the parity of subset sums within each coset of a subgroup generated by a basis element.

Write $m=|A|=s+1$. Proper-subset sums biject onto $G$, so $|G|=2^m-1$ is odd. Fix $a\in A$ and put $H=\langle a\rangle$. Toggling $a$ pairs all subsets whose sums lie in any fixed coset of $H$. This is a fixed-point-free involution, so each such fiber has even cardinality. If that coset does not contain the full-set sum, every subset in it is admissible and its fiber bijects with $H$. Lagrange makes $|H|$ odd, a contradiction. A proper subgroup has a coset avoiding the full-set sum, so $H=G$.

The Lean proof uses the frozen D5.S3.PrimeForms.Crossing.GlideCrossingParity.glide_crossing_count_even for the involution parity step. The remaining constructions are proper-subset and coset-fiber equivalences, with Mathlib cardinality, subgroup and cyclicity interfaces.

A finite abelian group with positive $s$, a finset $A$ of cardinality $s+1$, unique admissible subset sums, and no additive generator would contradict result. Changing to exactly $s$ summands, omitting uniqueness, or changing the size of $A$ gives a different problem.

The kernel-checked settling theorem is D5.S3.FiniteGroups.BajnokBersonJustPerfectRestrictedBasis.result. Its public definitions are IsPerfectRestrictedBasis and claim; the Blueprint displays their full bodies and the expanded settling proposition. The source note is bajnokbersonjust2022perfectrestricted.

The escape audit for the public result is unfinished: #19735. No validated four-slot registration is claimed. The missing evidence is a complete source reconstruction and realization bridge, whole-family variation and sensitivity, and actual observational dependence for the enrolled dependent-family interface.

The experiment is the-omega-institute/trureturing-experiments, pinned directory. Measured command: python3 /Users/auric/trureturing-experiments/docs/reports/bajnok-berson-just-2022-perfect-restricted-basis-question-6/check.py; exit 0, RESULT PASS. Script SHA-256: b89bd080af5dfc7e0a60f39b85a7d7b59d418886e07a3136692e98b5b1fb6dbd. It exhaustively enumerates candidate bases in the six abelian groups of order $2^m-1$ for $m=2,\ldots,6$: $\mathbb Z_3$, $\mathbb Z_7$, $\mathbb Z_{15}$, $\mathbb Z_{31}$, $\mathbb Z_{63}$ and $\mathbb Z_3\times\mathbb Z_{21}$. The five cyclic basis counts are respectively $1,2,2,6,6$, and every element of every listed basis generates its group. The noncyclic group has zero perfect restricted $5$-bases of size $6$. These are finite computations, not a proof of an unbounded classification.

What the settlement shows

• Kernel-checked: result proves cyclicity for every finite abelian group satisfying the source assumptions, including composite-order groups. The question's negative answer is unrestricted in the group order.
• Proved in prose: every $a\in A$ generates $G$. For that chosen $a$, the Route argument applies to each coset of $H=\langle a\rangle$. If $H$ were proper, select a coset other than the coset of $\sum A$; its subset fiber would have cardinality $|H|$, both odd by Lagrange and even by toggling $a$. Thus $H=G$. This strengthened statement is explanatory mathematics, not a separately published Lean theorem.
• Proved in prose: the sole inadmissible subset is $A$ itself; proper-subset uniqueness gives $|G|=2^{s+1}-1$. Together with the source's Proposition 5, the possible groups at size $s+1$ are exactly the cyclic groups of this order. The existence direction is literature evidence; it is not a new Lean theorem here.
• Computed: in the exact finite scope of the Evidence experiment, the cyclic basis counts are $1,2,2,6,6$, all basis elements are generators, and the sole noncyclic group in scope has count $0$.
• Proved in prose: for $m\ge2$ and $N=2^m-1$, the unit multiples of $B={1,2,4,\ldots,2^{m-1}}$ give $\varphi(N)/m$ distinct perfect restricted $(m-1)$-bases. Proper binary subset sums are precisely $0,\ldots,N-1$, each once. Multiplication by $2$ cyclically permutes $B$ modulo $N$; its order is $m$, since $0<2^k-1<N$ for $0<k<m$. A unit stabilizing $B$ must send $1$ to a member of $B$, so the stabilizer is exactly these $m$ powers of $2$. Orbit-stabilizer gives the count. For $m=2,\ldots,6$, $\varphi(N)=2,6,8,30,36$, so these counts agree with the experiment.
• Open: whether every perfect restricted $(m-1)$-basis of size $m$ is such a unit multiple for arbitrary $m$. Finite agreement does not establish this universal basis classification.
• Open: the source's Questions 7, 10 and 11, concerning $s+2\le m\le2s$, $m=2s+1$ and $m\ge2s+2$, respectively. The full-set omission used here no longer describes the inadmissible subsets in those ranges. Proposition 5 remains the existence direction; the settlement closes its immediately following Question 6 without supplying the other classifications.
• Literature status: no published settlement was located in the inspected material recorded in #19526. Completeness is ASSUMED-UNVERIFIED.

The literature screen recorded in #19526 covers the source's arXiv v1, Bajnok's survey arXiv:2211.01893 Section 3, Bajnok–Beatty arXiv:2406.04045, and the relevant Greene–Higgins and Hang Yu material. The journal full text and a complete forward-citation inventory were not independently audited. No mathematical-priority claim follows from this partial screen. The experimental scope ends at $m=6$; the universal unit-multiple classification and the neighbouring source questions remain open here.