Two-independence and upper two-star formation differ

Abstract

A bipartite graph on ten vertices has a minimal two-star-forming set of size six, but every two-independent set has size at most five.

Let G be a finite simple graph on V, with decidable adjacency. Write d(G,S,v) for the number of neighbours of v in S. All sets below are finite vertex sets. The definitions are those of Rafik Sahbi, Upper k-Star-Forming Sets, k-Independence, and Upper Domination, arXiv:2610.03785v2, Definition 2.1 and Conjecture 4.2.

Definition 1.1 (Selected induced degree is less than k).

$$\mathrm{IsKIndependent}\left(G,k,I\right)\iff \left(\forall v\in V,\mathrm{Member}\left(v,I\right)\Rightarrow d\left(G,I,v\right)<k\right)$$

Formalization. D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.IsKIndependent (✓ std3).

Source. Repository-derived.

Commentary.

Each selected vertex has fewer than k selected neighbours. For k equal to two, the induced graph is a disjoint union of edges and isolated vertices.

Definition 1.2 (Maximum k-independent cardinality).

$$\mathrm{beta}\left(G,k\right)=\mathrm{supCard}\left(\{I\in \mathrm{powerset}\left(\mathrm{univ}\left(V\right)\right)\mid \mathrm{IsKIndependent}\left(G,k,I\right)\}\right)$$

Formalization. D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.beta (✓ std3).

Source. Repository-derived.

Commentary.

Take the maximum cardinality over the k-independent subsets of V. The finite supremum has value zero if the family is empty.

Definition 1.3 (A star containing each outside vertex).

$$\mathrm{IsStarForming}\left(G,k,S\right)\iff \left(\forall v\in V,\left(\neg \mathrm{Member}\left(v,S\right)\right)\Rightarrow \left(\exists c\in V,\exists L\in \mathrm{Finset}\left(V\right),\mathrm{card}\left(L\right)=k\wedge \left(\left(\neg \mathrm{Member}\left(c,L\right)\right)\wedge \left(\mathrm{Subset}\left(\mathrm{insert}\left(c,L\right),\mathrm{insert}\left(v,S\right)\right)\wedge \left(\left(\forall ell\in V,\mathrm{Member}\left(ell,L\right)\Rightarrow \mathrm{Adj}\left(G,c,ell\right)\right)\wedge \mathrm{Member}\left(v,\mathrm{insert}\left(c,L\right)\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.IsStarForming (✓ std3).

Source. Repository-derived.

Commentary.

For every vertex outside S, the graph on S together with that vertex contains a star with k leaves containing the vertex. The centre is distinct from all leaves. Extra edges between leaves are allowed: the star is a subgraph, with no induced-subgraph requirement.

Definition 1.4 (Inclusion-minimal star formation).

$$\mathrm{IsMinimalStarForming}\left(G,k,S\right)\iff \left(\mathrm{IsStarForming}\left(G,k,S\right)\wedge \left(\forall T\in \mathrm{Finset}\left(V\right),\mathrm{ProperSubset}\left(T,S\right)\Rightarrow \left(\neg \mathrm{IsStarForming}\left(G,k,T\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.IsMinimalStarForming (✓ std3).

Source. Repository-derived.

Commentary.

The set is star-forming and no proper subset is star-forming. This is inclusion-minimality rather than minimum cardinality.

Definition 1.5 (Upper k-star-forming number).

$$\mathrm{SF}\left(G,k\right)=\mathrm{supCard}\left(\{S\in \mathrm{powerset}\left(\mathrm{univ}\left(V\right)\right)\mid \mathrm{IsMinimalStarForming}\left(G,k,S\right)\}\right)$$

Formalization. D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.SF (✓ std3).

Source. Repository-derived.

Commentary.

Take the maximum cardinality among all inclusion-minimal k-star-forming sets. The finite supremum has value zero if the family is empty.

Definition 1.6 (Two local alternatives).

$$\mathrm{LocalTwo}\left(G,S\right)\iff \left(\forall v\in V,\left(\neg \mathrm{Member}\left(v,S\right)\right)\Rightarrow \left(2\le d\left(G,S,v\right)\vee \left(\exists u\in V,\mathrm{Member}\left(u,S\right)\wedge \left(\mathrm{Adj}\left(G,v,u\right)\wedge 1\le d\left(G,S,u\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.LocalTwo (✓ std3).

Source. Repository-derived.

Commentary.

Every outside vertex either has two neighbours in S, or has a neighbour in S that itself has a neighbour in S. In the second alternative this further neighbour cannot be the outside vertex.

Theorem 1.7 (The local criterion equals the star definition).

$$\forall V\in Type,\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall S\in \mathrm{Finset}\left(V\right),\mathrm{IsStarForming}\left(G,2,S\right)\iff \mathrm{LocalTwo}\left(G,S\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.starForming_two_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

In a two-leaf star, the outside vertex is either the centre, giving two neighbours in S, or a leaf, giving a centre and another leaf in S. Conversely, two selected neighbours give a star centred at the outside vertex; a selected neighbour with its own selected neighbour gives a star centred at that selected neighbour. The argument works on any vertex type with decidable equality and adjacency.

Definition 1.8 (Equality on all bipartite finite graphs).

$$claim\iff \left(\forall n\in Nat,\forall G\in \mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right),\mathrm{Colorable}\left(G,2\right)\Rightarrow \mathrm{beta}\left(G,2\right)=\mathrm{SF}\left(G,2\right)\right)$$

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

Source. Repository-derived.

Commentary.

Conjecture 4.2 asserts equality for every bipartite finite graph. Graphs on Fin n cover every finite simple graph up to isomorphism. Bipartiteness is expressed by a proper colouring with two colours.

Theorem 1.9 (The equality is false).

$$\neg claim$$

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

Resolves. Problems/sahbi-2026-star-forming-bipartite-refutation (refuted) by D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.result.

Source. Repository-derived.

Commentary.

Use vertices 0 through 9, with sides 0 through 4 and 5 through 9. The neighbourhoods on the first side are {5,6,9}, {5,6,8}, {8,9}, {6,7,8,9}, and {5,7,8,9}, respectively. Colour by side. The set {0,1,2,5,6,7} satisfies the local criterion, while each of its 63 proper subsets fails it. It is therefore minimal two-star-forming, so SF is at least six. Each of the 210 six-element vertex sets contains a vertex with at least two selected neighbours. Any larger two-independent set would contain a two-independent six-element subset, since deletion cannot increase selected degrees. Thus beta is at most five and the asserted equality fails.

References

• Truth anchor: D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.IsKIndependent
• Truth anchor: D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.IsMinimalStarForming
• Truth anchor: D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.IsStarForming
• Truth anchor: D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.LocalTwo
• Truth anchor: D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.SF
• Truth anchor: D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.beta
• Truth anchor: D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.claim
• Truth anchor: D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.result
• Truth anchor: D5/S3/Combinatorics/Graph/StarFormingDissociationRefutation.starForming_two_iff