Perfect restricted bases of size s + 1

Abstract

Every finite abelian group with a perfect restricted basis of size s + 1 is cyclic.

Definition 1.1 (Perfect restricted s-bases).

$$\forall G\in Type\ast ,[\mathrm{AddCommGroup}\left(G\right)][\mathrm{DecidableEq}\left(G\right)]\forall s\in \mathbb{N},\forall A\in \mathrm{Finset}\left(G\right),(\mathrm{IsPerfectRestrictedBasis}\left(s,A\right))\iff (\forall g\in G,\mathrm{ExistsUnique}\left((T:\mathrm{Finset}\left(G\right)),(T\subseteq A)\wedge ((Finset.card\left(T\right)\le s)\wedge (\sum _{x\in T}x=g))\right))$$

Formalization. D5/S3/FiniteGroups/BajnokBersonJustPerfectRestrictedBasis.IsPerfectRestrictedBasis (✓ std3).

Citation. B. Bajnok, C. Berson and H. A. Just (2022). On Perfect Bases in Finite Abelian Groups. DOI: 10.2140/involve.2022.15.525. URL: https://arxiv.org/abs/2211.13675v1.

Commentary.

The paper states (abstract, p. 1): “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.” The Lean predicate uses a finset T of distinct elements, requires T ⊆ A and T.card ≤ s, and records the sum over T. The empty finset supplies the empty sum.

Definition 1.2 (The cyclic conclusion for Question 6).

$$(\mathrm{claim}\left(\right))\iff (\forall G\in Type,[\mathrm{AddCommGroup}\left(G\right)][\mathrm{Fintype}\left(G\right)][\mathrm{DecidableEq}\left(G\right)]\forall s\in \mathbb{N},\forall A\in \mathrm{Finset}\left(G\right),(1\le s)\Rightarrow ((Finset.card\left(A\right)=s+1)\Rightarrow ((\mathrm{IsPerfectRestrictedBasis}\left(s,A\right))\Rightarrow (\mathrm{IsAddCyclic}\left(G\right)))))$$

Formalization. D5/S3/FiniteGroups/BajnokBersonJustPerfectRestrictedBasis.claim (✓ std3).

Citation. B. Bajnok, C. Berson and H. A. Just (2022). On Perfect Bases in Finite Abelian Groups. DOI: 10.2140/involve.2022.15.525. URL: https://arxiv.org/abs/2211.13675v1.

Commentary.

Question 6 (p. 8) asks: “Are there any noncyclic groups that have a perfect restricted s-basis of size s + 1?” The displayed proposition answers the question for finite abelian groups: positive s, a basis with cardinality s + 1, and the perfect restricted basis condition imply IsAddCyclic.

Theorem 1.3 (Question 6 has a negative answer).

$$\forall G\in Type,[\mathrm{AddCommGroup}\left(G\right)][\mathrm{Fintype}\left(G\right)][\mathrm{DecidableEq}\left(G\right)]\forall s\in \mathbb{N},\forall A\in \mathrm{Finset}\left(G\right),(1\le s)\Rightarrow ((Finset.card\left(A\right)=s+1)\Rightarrow ((\mathrm{IsPerfectRestrictedBasis}\left(s,A\right))\Rightarrow (\mathrm{IsAddCyclic}\left(G\right))))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/BajnokBersonJustPerfectRestrictedBasis.result (✓ std3). ∎

Resolves. Problems/bajnok-berson-just-2022-perfect-restricted-bases-question-6 (proved) by D5/S3/FiniteGroups/BajnokBersonJustPerfectRestrictedBasis.result.

Source. Repository-derived.

Acknowledgement. B. Bajnok, C. Berson and H. A. Just (2022). On Perfect Bases in Finite Abelian Groups. DOI: 10.2140/involve.2022.15.525. URL: https://arxiv.org/abs/2211.13675v1.

Commentary.

The proof first identifies the admissible subsets with the proper subsets of A, giving the odd cardinality 2 raised to A.card minus 1 for G. For each a in A, the map that toggles a is a fixed-point-free involution on every selected coset of the subgroup generated by a, so each such fiber has even cardinality. Lagrange’s divisibility and the proper-subset count make the subgroup cardinality odd; excluding the coset containing the full subset forces that subgroup to be all of G.

References

• Truth anchor: D5/S3/FiniteGroups/BajnokBersonJustPerfectRestrictedBasis.IsPerfectRestrictedBasis
• Truth anchor: D5/S3/FiniteGroups/BajnokBersonJustPerfectRestrictedBasis.claim
• Truth anchor: D5/S3/FiniteGroups/BajnokBersonJustPerfectRestrictedBasis.result
• Dependency: D5/S3/PrimeForms/Crossing/GlideCrossingParity