Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Non-chordal graphs with unstable restricted clique polynomials

Abstract

For every r ≥ 1, the join of a complete graph on max(r−2,0) vertices with a four-cycle is r-connected, K_{r+3}-free and non-chordal. Marking one cycle vertex gives a clique polynomial with a zero in the product of the upper half-planes.

Definition 1.1 (The restricted clique polynomial).

Formalization. D5/S3/Combinatorics/Graph/CliquePolynomial/FaalNonStable.C_B (✓ std3).

Citation. H. Teimoori Faal (2026). A Bivariate B-Restricted Clique Polynomial: From Local Neighborhoods to Global Expansion. URL: https://arxiv.org/abs/2602.24151v1.

Commentary.

Definition 2.1, page 4: “For G=(V,E) and B ⊆ V, define” C_B(G;x,y) := ∑_{K ⊆ V, K clique} x^{|K|} y^{|K ∩ B|}. Cliques are Mathlib SimpleGraph.IsClique on the set underlying a Finset. Finset.univ.powerset.filter enumerates every clique once, including the empty clique, which contributes 1 as in Example 2.3. The complex-valued function is evaluation of this real-coefficient polynomial.

Definition 1.2 (Real stability).

Formalization. D5/S3/Combinatorics/Graph/CliquePolynomial/FaalNonStable.RealStable (✓ std3).

Citation. H. Teimoori Faal (2026). A Bivariate B-Restricted Clique Polynomial: From Local Neighborhoods to Global Expansion. URL: https://arxiv.org/abs/2602.24151v1.

Commentary.

Definition 2.4, page 4: “A polynomial f(x,y) ∈ ℝ[x,y] is real stable if it is not identically zero and” f(x,y) ≠ 0 “for all (x,y) ∈ ℂ² such that Im(x) > 0 and Im(y) > 0.” Here RealStable is this evaluation predicate on a function ℂ → ℂ → ℂ. It is applied to C_B, whose coefficients are real nonnegative integers. The first conjunct states that the function is not identically zero.

Definition 1.3 (Vertex connectivity).

Formalization. D5/S3/Combinatorics/Graph/CliquePolynomial/FaalNonStable.RConnected (✓ std3).

Citation. H. Teimoori Faal (2026). A Bivariate B-Restricted Clique Polynomial: From Local Neighborhoods to Global Expansion. URL: https://arxiv.org/abs/2602.24151v1.

Commentary.

Definition 4.2, page 7: “A graph is r-connected if removal of fewer than r vertices leaves it connected.” The finite graph also has more than r vertices, the standard vertex-connectivity size convention. Deletion is Mathlib SimpleGraph.induce on the set of vertices outside S; connectedness is SimpleGraph.Connected.

Definition 1.4 (A chord of a closed walk).

Formalization. D5/S3/Combinatorics/Graph/CliquePolynomial/FaalNonStable.HasChord (✓ std3).

Source. Repository-derived.

Acknowledgement. H. Teimoori Faal (2026). A Bivariate B-Restricted Clique Polynomial: From Local Neighborhoods to Global Expansion. URL: https://arxiv.org/abs/2602.24151v1.

Commentary.

A chord joins two nonconsecutive vertices of the closed walk. Positions i and j are in Fin p.length, so the repeated terminal vertex is omitted. The inequality i.val + 1 < j.val orders the positions and excludes successive edges; the additional negation excludes the closing edge from the first to the last position. Walk.getVert takes a natural index: val explicitly displays the coercion from Fin p.length to ℕ.

Definition 1.5 (Chordal graphs).

Formalization. D5/S3/Combinatorics/Graph/CliquePolynomial/FaalNonStable.Chordal (✓ std3).

Citation. H. Teimoori Faal (2026). A Bivariate B-Restricted Clique Polynomial: From Local Neighborhoods to Global Expansion. URL: https://arxiv.org/abs/2602.24151v1.

Commentary.

Definition 4.3, page 7: “A graph is chordal if every induced cycle has length 3.” The same source, page 9, says “every cycle of length >3 has a chord.” The displayed definition uses the latter literal cycle-and-chord formulation. Cycles are Mathlib SimpleGraph.Walk.IsCycle, and every closed cycle of length at least four must have a chord.

Definition 1.6 (Faal’s existence question).

Formalization. D5/S3/Combinatorics/Graph/CliquePolynomial/FaalNonStable.claim (✓ std3).

Citation. H. Teimoori Faal (2026). A Bivariate B-Restricted Clique Polynomial: From Local Neighborhoods to Global Expansion. URL: https://arxiv.org/abs/2602.24151v1.

Commentary.

Section 7, Open Problems, item 1, page 18: “Necessity of Conditions: Are the conditions of r-connectivity and chordality also necessary? Is there an r-connected K_{r+3}-free non-chordal graph for which C_B(G;x,y) fails to be real-stable?” The claim answers the second sentence for every natural r ≥ 1. V is a finite vertex type, G has decidable adjacency, and B is a Finset of vertices. Clique-freeness is Mathlib SimpleGraph.CliqueFree (r + 3); the final two conjuncts negate chordality and real stability.

Theorem 1.7 (A family for every positive connectivity).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/CliquePolynomial/FaalNonStable.result (✓ std3). ∎

Resolves. Problems/teimoori-faal-2026-b-restricted-clique-real-stability (proved) by D5/S3/Combinatorics/Graph/CliquePolynomial/FaalNonStable.result.

Source. Repository-derived.

Acknowledgement. H. Teimoori Faal (2026). A Bivariate B-Restricted Clique Polynomial: From Local Neighborhoods to Global Expansion. URL: https://arxiv.org/abs/2602.24151v1.

Commentary.

Put a = max(r−2,0), take G = K_a ∨ C₄, and mark the cycle vertex of index 0. Cliques of a join split uniquely into cliques of its two factors. The complete factor contributes (1+x)^a and the marked four-cycle contributes (1+2x)(1+x+xy). Thus C_B = (1+x)^a(1+2x)(1+x+xy), which vanishes at x=i and y=−1+i, both with imaginary part 1. After deletion of fewer than r vertices, a remaining complete-graph vertex connects all survivors; if no such vertex remains, at most one cycle vertex was deleted. The induced four-cycle has no chord, and every clique has size at most a+2 < r+3. Natural subtraction r−2 denotes max(r−2,0). For r=1 and r=2 the family is C₄; the assertion is r-connectedness and makes no exact-connectivity claim.

References