A SURJUNCTIVE GROUP THAT IS NOT SOFIC
Submitted to Palomar on September 14, 2026 at 01:02:12 UTC.
Submission ID: e8sd7sbrpcxh
Palomar automated verification:
https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/34794577299

Repository: https://github.com/SauersML/group-approximation
Commit: 232c77f169ec66b27fd480d5c19474f519d359b7
Tag: palomar-surjunctive-nonsofic-20260913
Project directory: repository root
Comparator configuration: Palomar/comparator-surjunctive-nonsofic.json
Metadata: formalization.yaml at the specified commit
Author: Sauers
Responsible maintainer: SauersML
License: Apache-2.0

Selected declarations:
SurjunctiveNonsofic.not_all_surjunctive_groups_sofic
SurjunctiveNonsofic.exists_finitelyGenerated_surjunctive_not_sofic

Does surjunctivity imply soficity? No.
Is there a finitely generated surjunctive nonsofic group? Yes.

Verification for this exact commit:
PASSED: build, definition checks, statements, axioms and metadata.
https://github.com/SauersML/group-approximation/actions/runs/34792730705
PASSED: Comparator with independent NanoDa replay and failure-log check.
https://github.com/SauersML/group-approximation/actions/runs/34792724682
Both theorem axiom closures are exactly propext, Classical.choice and Quot.sound.

Kun and Thom constructed the witness and proved its nonsoficity. The new
contribution is its surjunctivity. The metadata records the mathematical
sources and their roles, and the separate Astra, Claude and Codex credits.
The question is documented in 2010; its first proposer remains unconfirmed.

Use the specified immutable commit when submitting. Later commits to main
may contain unrelated work and are not covered by these verification runs.
The former submission remains withdrawn. The new submission is undergoing
Palomar's automated verification and review; registration is a later step.