The Six-Neuron Counterexample to the Target-Free Clique Conjecture Is Minimal

Abstract

This record presents an exact, independently replayable computer-assisted proof that every legal combinatorial threshold-linear network (CTLN) on at most five neurons satisfies the algebraic target-free clique classification. Consequently, every nondegenerate legal CTLN on at most five neurons has exactly its target-free cliques as stable fixed-point supports. Together with Jesse Geneson's six-neuron counterexample, this establishes that six is the minimum counterexample order. The proof enumerates the 9,608 directed-graph isomorphism classes on five vertices. Of the 9,607 noncliques, 8,902 admit no parameter interval on which full support is permitted. The remaining graphs yield 706 permission components, of which 317 are excluded by a rank-one determinant argument and 389 by exact Bernstein/Farkas certificates. An independent certificate interpreter, a separate graph-to-certificate ledger, complete verification through support size four, and an induced-support orbit audit close the passage from full support to arbitrary supports. The accompanying archive replays the complete proof with “python verify.py” using Python 3.12 or later and only the Python standard library. Every theorem-bearing calculation uses exact integer or rational arithmetic; no floating-point result, solver status, or timeout is used as a proof step. This work was carried out as part of the Conjecture Prover and Autoformalization Project of the Stanford Lean Club, which is led by Donald D. Poindexter, Jr. The project investigates open mathematical problems through AI-assisted proof search, exact computational certification, independent auditing, and formalization. Research assistance from OpenAI GPT-5.6 Sol Ultra and the use of other models for auditing and editorial assistance are disclosed in the manuscript. The six-neuron construction is due to Jesse Geneson and is used here as a cited upper-bound witness; no priority or authorship is claimed for that construction. Independent computational replay is not equivalent to journal peer review. Licensing is assigned by file scope: the manuscript and explanatory documentation are released under CC BY 4.0, while source code, certificates, ledgers, catalogues, and manifests are released under the MIT License. See LICENSE inside the archive. Release ZIP SHA-256: 622e0cdff953fe20086711894ad85e2f4df0428f64723c9e068303ec428018d7 Standalone manuscript SHA-256: 63f2c6e141cb7d25276579beb4924a4be794f5a36009dae1588d5fbeb9b0bc16 Internal manifest SHA-256: 6c80d7be43a8513881f9fa0f44a20bf6a3c3e4e403b115f2f8689b5944419b50