Metadata

slug: tf2112
bibkey: teimoorifaal2021sums
doi: 10.48550/arXiv.2112.09744
url: https://arxiv.org/abs/2112.09744v1
triage: theorem
motivation_gids:
  - D5/S3/Combinatorics/Graph/CliquePolynomial/TeimooriFaalK4FreeCliqueRoots.result

A connected K₄-free graph with nonreal clique roots

Problem

Hossein Teimoori Faal, Sums of Polynomials and Clique Roots, arXiv:2112.09744v1, Conjecture 4.1, page 5:

Let G be a connected K₄-free graphs, then G has only clique roots.

Section 2, page 3, defines a clique root as a real root of the clique polynomial. Thus the conjecture asserts that every complex zero is real. The source note gives the locators; #22515 contains the preregistered literal statement. The conjecture is Refuted.

Statement echo

Source clause	Lean counterpart	Fidelity
Finite simple undirected graphs	`V`, `Fintype V`, `SimpleGraph V` in `claim`	All finite vertex types, symmetric irreflexive adjacency
Connected	`SimpleGraph.Connected`	Includes nonemptiness
K₄-free	`SimpleGraph.CliqueFree 4`	No four distinct pairwise adjacent vertices
Ordinary clique polynomial, empty clique counted once	Existing `TeimooriFaalFlatCliqueRoots.cliquePoly`	Integer coefficients count vertex subsets; terms through the vertex count, with higher clique counts zero
Only clique roots	Every complex zero has imaginary part zero	Quantifies over every complex zero
Finite decidability instances	`DecidableEq V`, `DecidableRel G.Adj`	No additional finite graph restriction
Negative answer	`result`	Negates the complete assertion

The public definition claim mirrors the quoted conjecture literally using the preregistered polynomial owner; there is no duplicate clique-polynomial definition.

Motivation

Connectedness and exclusion of four-vertex cliques do not force the cubic clique polynomial to split over the reals. A seven-vertex graph already exhibits the obstruction.

Gap

The literature screen in #22515 covers the versioned source, the author’s later graph/root papers, exact arXiv phrase and identifier queries, citing-work indexes, MathOverflow, Zenodo, MathDB and repository records. No settlement was located within that screen. Several services rate-limited requests and some broad result sets were only partially read. Literature completeness is ASSUMED-UNVERIFIED; absence of a journal version is not established.

Route

The private witness F7 on Fin 7 has edges $03, 04, 05, 06, 13, 14, 15, 16, 23, 25, 34, 35, 46, 56$ . The spanning path is $[0, 3, 1, 4, 6, 5, 2]$ . Finite kernel decisions establish K₄-freeness and clique counts $[1, 7, 14, 9, 0, 0, 0, 0]$ . The existing TeimooriFaalFlatCliqueRoots.cliquePoly counts these cliques, giving $p (X) = 1 + 7 X + 14 X^{2} + 9 X^{3}$ . The module uses Cubic.discr_eq_prod_three_roots to show that a real splitting would make the discriminant nonnegative; its actual value is $- 31$ . The module then uses Polynomial.Splits.of_splits_map and IsAlgClosed.splits to contradict the assertion that every complex zero is real.

Falsifier

A formal refutation must exhibit a finite connected K₄-free graph and a complex zero of its integer clique polynomial with nonzero imaginary part. The theorem result proves the negation of the full universal claim. It imposes no additional hypotheses on that claim.

Evidence

The settling node is D5/S3/Combinatorics/Graph/CliquePolynomial/TeimooriFaalK4FreeCliqueRoots.result. The module has one public theorem and private consumed helpers. The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9).

Experiment

The immutable experiment is clique-roots-k4free at 9cabbd8bde46e73d7b1277bb548168561fc43c84. check.py has SHA-256 e6388e5e172bb0a6defc419d7092933261213afd49af8772fa745f72627af438. Its immutable blob was checked with git cat-file -e and extracted unchanged; python3 /Users/auric/.sshx/efc322433ab71b54c7953443/attempt-1/check.py exited 0 with ALL_CHECKS_OK, using SymPy 1.14.0 and exact arithmetic. Finite family checks cover $m = 2, \dots, 8$ ; exhaustive deletion checks cover $m = 2, \dots, 5$ only. Symbolic checks verify the displayed coefficient, discriminant, affine-substitution, derivative and critical-value identities. The same script checks all connected labelled triangle-free graphs through six vertices and paths on two through ten vertices. These are computations, not uniform Lean theorems.

Triage

Item	Status	Evidence
F7 is connected and K₄-free	proved	Kernel-checked private `F7_connected` and `F7_cliqueFree`
F7 clique counts and polynomial bridge	proved	Kernel-checked private `F7_c0` through `F7_c7`, and `cliquePoly_F7`
F7 polynomial has a nonreal complex root	proved	Kernel-checked private `p_not_splits`, `p_has_nonreal_root`, and public `result`
Uniform Gₘ family for every m≥2 with unbounded vertex connectivity	open	Uniform Lean declaration absent; the preregistration supplies a prose construction, and the experiment checks only the stated finite/symbolic scope
Checker finite and symbolic computations m=2..8	computed	The immutable experiment above, exit 0, `ALL_CHECKS_OK`; lower-connectivity deletion enumeration only m=2..5
Triangle-free and chordal neighbouring subclasses	open	No uniform theorem about these subclasses in this module; finite triangle-free checks are computations only

What the settlement shows

Proved in this module: the connected K₄-free hypotheses permit the seven-vertex witness and a cubic clique polynomial with a nonreal complex zero. The obstruction is negative discriminant, rather than the absence of a real zero. The polynomial identity and nonsplitting statements are the private declarations named above; no root approximation is required.

Computed: the proposed graphs $G_{m}$ have clique coefficients $[1, 6 m + 1, 12 m^{2} + m, 8 m^{3}]$ for $m = 2, \dots, 8$ , are K₄-free, have one real root and no repeated root, and possess the displayed cut of size $m$ . Connectivity under every deletion of fewer than $m$ vertices is checked only for $m = 2, 3, 4, 5$ , over $14, 191, 2626, 36457$ deletion sets respectively.

Open in Lean: a uniform $G_{m}$ construction and its exact connectivity, clique counts and root conclusions for all $m \geq 2$ . The single F7 witness establishes no unbounded-connectivity theorem.

Literature boundary: the source’s Proposition 3.3 states a positive triangle-free result; its hypotheses exclude the triangles in F7. The chordal questions impose additional structure absent from the settled claim. They are not proved or refuted here. Conjecture 4.1 occurs in the source’s final open-questions section; no earlier proved result in that source depends on its truth. Its refutation supplies no conclusion about the other conjectures or chordal questions.

ASSUMED-UNVERIFIED

Literature completeness, exhaustive novelty and absence of an unlocated journal version remain ASSUMED-UNVERIFIED. The uniform family and the neighbouring subclasses have no Lean settlement in this delivery. The external experiment’s verified finite and symbolic scope is the scope stated above.

Keyboard shortcuts

trureturing — Discovering truth