Houghton's group H_3 has superpolynomial sofic profile

Houghton's finitely presented elementary amenable group H_3 has a finite chunk with superpolynomial sofic profile. We prove a lower bound exp(Omega(r^c)), where c = 1/(log_2(107)+1), and an upper bound exp(O(sqrt(r) log r)). The upper bound holds for every fixed finite chunk of H_3. The paper gives a scale-dependent correction to the extension estimate discussed in the text, polynomial far-commutator fillings and a full Dehn-function upper bound, quantitative unitary approximation bounds, and consequences for homomorphisms into groups with polynomial sofic 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.