The largest independent subset of a sphere or a ball in a free group: exact values, and the coincidence with the maximum rank

The largest independent subset of the sphere S₁ in Fᵣ has exactly r elements, for EVERY rank r: IsGreatest (sphSizes r 1) r. Lower bound: the free basis, independent by the homomorphism killing all generators but xᵢ and sending xᵢ to a transposition. Upper bound: a word of norm one is xᵢ⁺⁻¹ for a unique i and an independent set holds at most one of x, x⁻¹, so recording the letter injects the set into the r generators.

The same for the ball: IsGreatest (balSizes r 1) r for every rank r. The identity lies in B₁ but in no independent set (1 belongs to every subgroup), so the ball answers as the sphere does.

r = 2, n = 2: the largest independent subset of S₂ and of B₂ in F₂ has exactly 3 elements – IsGreatest (sphSizes 2 2) 3 and IsGreatest (balSizes 2 2) 3. Witness a⁻2, ab, ab⁻1 with three S₃ certificates; upper bound by 7 (resp. 17 + the identity) certified circuits over the 6 (resp. 8) inverse classes, kernel-checked with no native_decide.

r = 3, n = 2: the largest independent subset of S₂ and of B₂ in F₃ has exactly 5 elements – IsGreatest (sphSizes 3 2) 5 and IsGreatest (balSizes 3 2) 5. Witness a⁻2, ab, ab⁻1, ac, ac⁻1 (the paper's own Q₃(1) up to inverting one element); upper bound by 197 (resp. 288 + the identity) certified circuits over the 15 (resp. 18) inverse classes.

r = 2, n = 3: the largest independent subset of the sphere S₃ in F₂ has exactly 6 elements – IsGreatest (sphSizes 2 3) 6. Witness the six length-three words a⁻3, (aba)⁻1, (ab⁻1a)⁻1, (bab)⁻1, (ba⁻1b)⁻1, b⁻3; upper bound by certified circuits over the 18 inverse classes.

r = 2, n = 3, ball: 6 is realised by an independent subset of B₃ in F₂, i.e. 6 in balSizes 2 3. Immediate from FI5 because S₃ is contained in B₃; recorded separately because the matching upper bound is NOT kernel-bound here (see FI8).

In every cell settled here the answer to the source's Problem coincides exactly with the answer to Dotsenko's problem: the largest independent subset of Sₙ and of Bₙ has exactly rho(r,n) elements, where rho is the maximum RANK of a subgroup generated by elements of Bₙ as computed in the source's maximum-rank theorem (source label thm:max rank). Verified at (r,1) for every r and at (2,2), (3,2), (2,3) (ball at (2,3) as a lower bound). In particular the floor(log₂ v(r,n)) slack in the upper bound the source states without proof is never used; independence is strictly weaker than being a basis (a², a³ is independent of rank one, proved in Controls), so the coincidence is not formal.

Measured: the largest independent subset of the ball B₃ in F₂ has exactly 6 elements (exhaustive search over the 26 inverse classes with a Stallings-folding membership oracle, 2176 search nodes, 1.5 s), but only the lower bound is kernel-bound. The Lean-side upper bound enumerates Finset (Fin N) index sets; measured at N = 19 it costs 225 s end to end, so N = 26 is 2⁷ times larger, about 8 CPU-h – over the cap and parked. Also measured and parked: the largest independent subset of S₄ in F₂ (54 inverse classes, rho = 9), whose plain depth-first search over inverse classes was killed at 1800 s of one core with no answer.

Negative controls: 4 is not in sphSizes 2 2 nor in balSizes 2 2 (the value is not larger); 2 is not the greatest (the value is not smaller); the three sphere classes a⁻2, ab, a⁻1 b are NOT independent, and neither is x, x⁻1 nor x, x², so Independent is a real restriction on subsets of the very sphere in question; the identity is in every ball, in no sphere of positive radius and in no independent set; the combinatorial core of each upper bound does not prove a smaller bound (it is tight); and a², a³ is independent while generating the cyclic subgroup <a>, so an independent set can be larger than the rank of what it generates – which is what makes FI7 a statement rather than a tautology.