Irredundant bases for finite almost simple groups

In this thesis, we study maximum irredundant base sizes I(G, Γ) of three types of finite primitive permutation groups G, where two of the three types are almost simple. The maximum irredundant base size is equal to the length of the longest strictly descending chain of pointwise stabilisers of G on Γ, and its value has implications for the relational complexity of the permutation group. We start against the backdrop of Kelsey and Roney-Dougal (2022) showing that that if G is not large-base, then I(G, Γ) < 5 log |Γ|. While no 𝒪(log |Γ|) bounds on I(G, Γ) exist for large-base G, we give a pair of lower and upper bounds that are attained by infinitely many large-base groups. We then turn to almost simple permutation groups and study the non-standard actions of Sₙ and Aₙ. In this case, we give best possible upper bounds on I(G, Γ) in terms of n. We also show that an 𝒪(log |Γ| / log log |Γ|) bound holds and in most cases an 𝒪((log log |Γ|)²) bound holds. The third type of primitive permutation groups is almost simple classical groups over finite fields. If such a group G is of rank r over a field of characteristic p and order pᵉ, the best known upper bound is 𝒪(r⁸ + log e), shown by Gill and Liebeck (2023). We construct large explicit irredundant bases for the primitive actions of the symplectic, unitary, and orthogonal groups on sets of subspaces, complementing the construction by Kelsey and Roney-Dougal (2022) for linear groups. The lower bounds on I(G, Γ) deduced from these constructions suggest that an 𝒪(r² + log e) bound, if shown to be true, would be best possible for each of the four families of classical groups. The thesis ends with an exploration of computer-assisted formalisation of mathematics. We present the formalisation – in the programming language Lean – of a key result on wreath products used to find I(G, Γ) for some large-base groups.