Houghton's group H_3 has superpolynomial sofic profile

How many points does a permutation model of a group need? Houghton's group H_3, which is finitely presented and elementary amenable, has a finite piece whose sofic profile lies between exp(Omega(r^c)), with c = 1/(log_2(107)+1), about 0.129, and exp(O(sqrt(r) log r)). So an amenable group can have superpolynomial sofic profile, and every homomorphism from H_m (m at least 3) to a group of polynomial sofic profile, such as a birational group, kills the finitary alternating subgroup. Cornulier's extension theorem fails as stated; we locate the error and prove a corrected, scale-dependent bound. The lower bound rests on a general counting criterion: if finitely many relations make many displaced copies of S_3 commute cheaply, every model is large. We also give unitary versions of the lower bounds, unitary models that beat our permutation models, a polynomial bound on the Dehn function of H_3, and a direct proof that every finite piece of a Baumslag-Solitar group has at most linear profile. Version 1.1 adds the general counting criterion, the Baumslag-Solitar theorem, the fact that every profile is bounded or at least 2r, unitary bounds for every separation margin, the quadratic lower bound for the Dehn function, and an example showing that the kernel and quotient of an extension do not determine its profile. This preprint archive includes the PDF, TeX source, executable verification scripts, finite group-word certificates, and scoped Lean proofs. The verification artifacts do not formally verify the entire manuscript. Exact hypotheses and limitations are stated in the manuscript and verification/README.md.