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 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. Version 1.1.1 hardens the certificate verifiers (an exact certificate inventory, explicit checks, and mutation tests in normal and optimized Python), cites the companion papers at their published versions, collects the conversions between the Hamming and Hilbert-Schmidt scales in one place, and notes that the correction of the extension theorem needs only the unweighted bound. The mathematical results are unchanged. Version 1.1.2 corrects attributions and framing. The overview no longer reports Cornulier's derivation that elementary amenable groups have polynomial profile, which this paper refutes, and opens instead with the gap between bounded and linear profile. The birational consequences, known in characteristic zero from Jordan-type theorems, are moved out of Corollary 1.3. The embedding of Houghton groups into Thompson's group V is credited to Roever, the normal-subgroup lemma to Cornulier, Guyot and Pitsch, the Dehn-function scheme to Lee, and the Baumslag-Solitar statements to Cornulier; Slofstra's quantitative bounds are stated; a standard fact about representations is moved to a remark. The mathematical results and the numbering are unchanged. 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.