# yaml-language-server: $schema=https://raw.githubusercontent.com/mathlib-initiative/formalization.yaml/main/schema/formalization.schema.json version: "v0.4" # This submission selects Palomar/comparator-surjunctive-nonsofic.json only. project: name: A Surjunctive Group That Is Not Sofic description: >- We formalize the existence of a finitely generated surjunctive group that is not sofic. This answers negatively the converse to the Gromov-Weiss surjunctivity theorem, recorded as open problem OP-11 by Ceccherini-Silberstein and Coornaert and as Problem 1.1 by Bowen and Chapman. The witness is the symmetric double G *_Gamma G, 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), with the action given by monomial substitution. Kun and Thom constructed this pair and proved the double nonsofic. The new ingredient here is a surjunctivity theorem for symmetric doubles of surjunctive groups. The Lean development proves both halves for this witness, including the required permutation centralizer normalization theorem. The challenge states surjunctivity through finite-memory cellular automata and soficity through finite normalized-Hamming models. The two selected declarations assert the finitely generated counterexample and the failure of the universal converse. authors: [Sauers] responsible_maintainers: [SauersML] license: Apache-2.0 classification: arxiv: [math.GR, math.DS] msc2020: ["20F69", "37B15", "20E06"] sources: - title: A surjunctive group that is not sofic type: original-proof relationship: other contributors: - name: Astra role: developed the original surjunctivity argument using a custom proof tool under the author's direction - name: Claude (Anthropic) role: produced the Lean development and original exposition under the author's direction - name: Codex (OpenAI) role: prepared the submission metadata and account of sources, and audited the submission package note: >- The original contribution is surjunctivity of the previously constructed Kun-Thom nonsofic witness. The proof uses finite quotients of finite free factors of the fold kernel, transplants cellular automata to coset sets, and cancels lower support strata in a fixed subset order. The remaining map acts on finitely many cosets of a stabilizer intersection, whose surjunctivity supplies an inverse. The unconditional formal endpoint is GroupApproximation.SurjunctiveNonsofic.exists_fg_surjunctive_not_isSofic. The group's construction and its nonsoficity are credited to Kun and Thom below. A September 13 literature review found no earlier separation proof or applicable permanence theorem making the separation an immediate corollary; this is a bounded search, not a certification of absolute priority. - title: Cellular Automata and Groups authors: [Tullio Ceccherini-Silberstein, Michel Coornaert] year: 2010 type: book id: https://doi.org/10.1007/978-3-642-14034-1 location: Open Problems, OP-11 relationship: background note: >- Records the converse question. The second edition, Open Problems, p. 527, explicitly says its list appeared in the first edition and retains OP-11. This supports a 2010 occurrence, not an identification of the first person to pose the question. Chapters 1 and 3 supply standard cellular-automaton and surjunctivity facts. - title: Cellular Automata and Groups, second edition authors: [Tullio Ceccherini-Silberstein, Michel Coornaert] year: 2024 type: book id: https://doi.org/10.1007/978-3-031-43328-3 location: Open Problems, p. 527, OP-11; Chapter 3 historical notes relationship: background note: >- The authors' retrospective confirmation of the first-edition problem list. The publisher dates the eBook to January 2024; its copyright year is 2023. - title: Surjunctivity does not characterize cosoficity of invariant random subgroups authors: [Lewis Bowen, Michael Chapman] year: 2025 type: paper id: https://arxiv.org/abs/2511.06586 location: Problem 1.1 and Theorem 1.2 relationship: background note: >- Problem 1.1 asks whether all surjunctive groups are sofic. Their Theorem 1.2 answers the analogous question for invariant random subgroups; it does not supply a surjunctive nonsofic group. The challenge uses their finite-list definition of a cellular automaton. - title: On approximation properties of semidirect products of groups authors: [Goulnara Arzhantseva, Światosław R. Gal] year: 2020 type: paper id: https://doi.org/10.5802/ambp.386 location: p. 127; Theorems 1 and 7, Lemma 6 relationship: background note: >- Annales Mathematiques Blaise Pascal 27(1), 125-130. Preprint arXiv:1312.7682 first posted December 30, 2013. Proves surjunctivity for split extensions with finitely generated residually finite kernel and surjunctive quotient, and finite-index permanence. The finite-generation hypothesis on the kernel prevents direct application to the infinite-rank free fold kernel used here. - title: Some general dynamical notions authors: [Walter H. Gottschalk] year: 1973 type: paper id: https://doi.org/10.1007/BFb0061728 location: Lecture Notes in Mathematics 318, 120-125 relationship: background note: >- Origin of surjunctivity and the question whether every group is surjunctive. That question is distinct from the converse to Gromov-Weiss and is not settled here. - title: Note on symbolic transformation groups authors: [Wayne M. Lawton] year: 1972 type: paper location: Notices of the American Mathematical Society 19, abstract relationship: other note: >- Credit for residual-finiteness surjunctivity and subgroup heredity, as attributed in the historical notes of Cellular Automata and Groups, Chapter 3. The original abstract was not directly inspected; the cited sources disagree on its page, so none is asserted here. - title: Endomorphisms and automorphisms of the shift dynamical system authors: [Gustav A. Hedlund] year: 1969 type: paper id: https://doi.org/10.1007/BF01691062 location: Mathematical Systems Theory 3, 320-375 relationship: other note: >- Classical source for the Curtis-Hedlund-Lyndon theorem. The proof uses its arbitrary-group finite-alphabet form and the finite-memory inverse of a bijective cellular automaton; see Cellular Automata and Groups, Chapter 1, for that formulation. - title: Endomorphisms of symbolic algebraic varieties authors: [Mikhail Gromov] year: 1999 type: paper id: https://doi.org/10.1007/PL00011162 relationship: background note: The implication from soficity to surjunctivity whose converse is answered here. - title: Sofic groups and dynamical systems authors: [Benjamin Weiss] year: 2000 type: paper id: https://www.jstor.org/stable/25051326 relationship: background note: >- Sankhya Series A 62, 350-359. Develops soficity and proves surjunctivity of sofic groups. The present result concerns the converse. - title: Nonsofic wreath products of residually finite groups authors: [Gabor Kun, Andreas Thom] year: 2026 type: paper id: https://arxiv.org/abs/2608.06222v3 location: Theorems A, E, and 4.1 relationship: other note: >- Supplies the existing nonsofic double and its polynomial/Laurent polynomial pair. Our witness is q = 2 and r = d = 3 in Theorem E; EL_3(Z) equals SL_3(Z). Theorem A supplies the nonsoficity argument, and Theorem 4.1 is its centralizer normalization input. The required results are proved in the Lean development, not added as axioms. This is credit for an ingredient of the new separation theorem, not a claim to have originated their construction or nonsoficity proof. - title: Centralizers of sofic approximations of Kazhdan groups authors: [Vadim Alekseev, Andreas Thom] year: 2026 type: paper id: https://arxiv.org/abs/2608.05362 relationship: other note: >- The component and almost-automorphism machinery used in the Kun-Thom normalization argument. Its needed estimates are developed in the formal proof. - title: Property (T) for noncommutative universal lattices authors: [Mikhail Ershov, Andrei Jaikin-Zapirain] year: 2010 type: paper id: https://doi.org/10.1007/s00222-009-0218-2 location: Theorem 1.1 relationship: other note: >- Supplies property (T) for elementary groups over finitely generated unital rings. The instances used by the witness are proved in Lean. - title: On sofic approximations of Property (T) groups authors: [Gabor Kun] year: 2016 type: paper id: https://arxiv.org/abs/1606.04471v5 relationship: background note: >- Expander-decomposition ancestry of the nonsoficity machinery. First posted in 2016; the cited fifth version is dated July 30, 2019. - title: Inapproximability of actions and Kazhdan's property (T) authors: [Gabor Kun, Andreas Thom] year: 2019 type: paper id: https://arxiv.org/abs/1901.03963v3 relationship: background note: >- Almost-automorphism and cluster-group ancestry of the centralizer machinery. First posted in 2019; the cited third version is dated August 4, 2026. These background credits supplement the direct Kun-Thom and Alekseev-Thom inputs above. automation: methods: - method: agent models: [Astra, Claude (Anthropic), Codex (OpenAI)] framework: Custom proof tool, Claude Code, and Codex tool_setup: >- AI-assisted mathematical exploration and Lean proof development, followed by submission preparation and remote verification. notes: >- Astra developed the original argument under the author's direction. Claude produced the original exposition and Lean development. Codex prepared this submission's metadata and exposition and checked its correspondence with the challenge and the source literature. These AI credits do not replace the human author's responsibility. review: status: self-assessed notes: >- AI reviews on September 12 and 13 examined statement fidelity, the finite-memory induction, the double model, the normalization hypothesis, and the prior literature. No human expert review or Palomar editorial acceptance is claimed. Comparator with NanoDa and the statement/axiom checks passed for commit 6738ce3d092e23a5976f6d45042f4d92c12bf5b0 in GitHub Actions runs 34785942633 and 34785945798. After the descriptive rename, run 34790950434 at acfbb7877804a60efc08f3c26f79919dfcb32f1e passed the build, definition checks, statement comparison and axiom audit. Verification for a selected revision is recorded separately in that revision's GitHub Actions runs; earlier runs certify only their named revisions. The previous Palomar submission was withdrawn. The prepared revision 232c77f169ec66b27fd480d5c19474f519d359b7 was submitted to Palomar as e8sd7sbrpcxh on September 14, 2026 UTC, for automated verification and review. Its submission record identifies the exact verification runs. repository: role: substantive-development status: scope: >- The two declarations selected by Palomar/comparator-surjunctive-nonsofic.json assert a finitely generated surjunctive nonsofic group and the negation of the universal implication from surjunctivity to soficity. main_results: - declaration: SurjunctiveNonsofic.not_all_surjunctive_groups_sofic file: Palomar/SurjunctiveNonsoficSolution.lean sorry_count: 0 axioms: [propext, Classical.choice, Quot.sound] comparator_config: Palomar/comparator-surjunctive-nonsofic.json - declaration: SurjunctiveNonsofic.exists_finitelyGenerated_surjunctive_not_sofic file: Palomar/SurjunctiveNonsoficSolution.lean sorry_count: 0 axioms: [propext, Classical.choice, Quot.sound] comparator_config: Palomar/comparator-surjunctive-nonsofic.json fidelity: divergences: >- Groups and finite palettes range over Type 0, which contains the concrete witness. Cellular automata are given by finite lists of memory elements and an arbitrary local rule; repetitions and empty memory are allowed. This is the standard full-shift notion. The development uses continuous shift-equivariant maps; the solution explicitly converts every challenge automaton to such a map. Soficity is the finite-set normalized-Hamming criterion, with models on nonempty finite carriers, multiplicative error at most epsilon, and pairwise separation at least 1 - epsilon. These are exactly the development's conditions, as proved by isSoficGroup_iff_isSofic. Finite generation is an explicit finite generating subset. This submission asserts finite generation only. It does not assert finite presentation, simplicity, or nonhyperlinearity, and does not settle Gottschalk's conjecture that all groups are surjunctive. alignment: statements: - source: Not every surjunctive group is sofic; the converse to the Gromov-Weiss theorem fails. lean: SurjunctiveNonsofic.not_all_surjunctive_groups_sofic module: Palomar.SurjunctiveNonsoficChallenge status: proved - source: There exists a finitely generated surjunctive group that is not sofic. lean: SurjunctiveNonsofic.exists_finitelyGenerated_surjunctive_not_sofic module: Palomar.SurjunctiveNonsoficChallenge status: proved acknowledgements: Built on Lean 4 and Mathlib; the mathematical ingredients are credited in sources.