A SURJUNCTIVE GROUP THAT IS NOT SOFIC Author: Sauers. Maintainer: SauersML. Status: submitted to Palomar as e8sd7sbrpcxh on September 14, 2026 UTC, at commit 232c77f169ec66b27fd480d5c19474f519d359b7. The earlier submission remains withdrawn. Palomar's automated verification: https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/34794577299 RESULT There exists a finitely generated surjunctive group that is not sofic. A group is surjunctive when every injective cellular automaton on its full shift over a finite alphabet is surjective. Soficity means that finite multiplication patterns admit asymptotically faithful finite permutation models in normalized Hamming distance. The question was recorded as OP-11 in Ceccherini-Silberstein and Coornaert, Cellular Automata and Groups (2010): https://doi.org/10.1007/978-3-642-14034-1 Their second edition, p. 527, explicitly confirms that the listed questions appeared in the first edition. This substantiates a 2010 formulation, without identifying the first proposer. Bowen and Chapman restate it as Problem 1.1 (2025): https://arxiv.org/abs/2511.06586 Their result concerns invariant random subgroups and leaves this group question open. WITNESS AND PROOF Take the symmetric double of G over Gamma, where Gamma = EL_3(F_2[x_1,x_2,x_3]) and G = EL_3(F_2[x_1^+-1,x_2^+-1,x_3^+-1]) semidirect EL_3(Z). The action is monomial substitution. Kun and Thom constructed this pair and proved its double nonsofic, in Theorems A and E: https://arxiv.org/abs/2608.06222v3 The new argument proves that the symmetric double of any surjunctive group over any subgroup is surjunctive. It uses finite quotients of finite free factors of the fold kernel and transfers an injective automaton to coset sets. Successive corrections cancel lower support strata in a fixed subset order. The residual map is supported on finitely many cosets of a stabilizer intersection. Surjunctivity of that subgroup supplies an inverse; finite-pattern separation and compactness yield surjectivity on the double. Here G is residually finite, hence surjunctive, and finitely generated. The two vertex groups therefore finitely generate the double. Classical inputs include Lawton's residual-finiteness and subgroup results, the Curtis-Hedlund-Lyndon theorem, and Gromov-Weiss surjunctivity. The Arzhantseva-Gal extension theorem requires a finitely generated kernel; the infinite-rank free fold kernel here does not satisfy that hypothesis. The nonsoficity machinery credits Kun-Thom and Alekseev-Thom, and the property-(T) input credits Ershov and Jaikin-Zapirain. Detailed sources, their roles, and the exact statement comparison are retained in metadata/palomar-surjunctive-nonsofic.yaml. FORMAL SCOPE AND VERIFICATION Configuration: Palomar/comparator-surjunctive-nonsofic.json Statements: Palomar/SurjunctiveNonsoficChallenge.lean Proof: Palomar/SurjunctiveNonsoficSolution.lean Selected declarations: SurjunctiveNonsofic.not_all_surjunctive_groups_sofic SurjunctiveNonsofic.exists_finitelyGenerated_surjunctive_not_sofic Both declarations are unconditional and use only propext, Classical.choice, and Quot.sound. Finite presentation is outside this selected formal result. Gottschalk's universal surjunctivity conjecture is not settled. Comparator, Lean, NanoDa, and statement/axiom checks passed for commit 6738ce3d092e23a5976f6d45042f4d92c12bf5b0: https://github.com/SauersML/group-approximation/actions/runs/34785942633 https://github.com/SauersML/group-approximation/actions/runs/34785945798 The renamed modules passed the build, definition checks, statement comparison and axiom audit at acfbb7877804a60efc08f3c26f79919dfcb32f1e: https://github.com/SauersML/group-approximation/actions/runs/34790950434 The selected candidate must also pass Comparator with NanoDa; its verification is recorded in the GitHub Actions runs for that exact revision. These are repository verification runs; Palomar processes the submitted revision separately. Astra developed the original argument using a custom proof tool under the author's direction. Claude (Anthropic) produced the Lean development and original exposition. Codex (OpenAI) reviewed the proof, literature, and credits and prepared these materials. License: Apache-2.0.