Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-28
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A split set with both a complete and an anticomplete outside vertex yields a nontrivial module

Statement

Let G be a bull-free graph and let SV(G) be a split set. Suppose there are vertices c,aV(G)S such that c is complete to S and a is anticomplete to S. Then G has a nontrivial module.

Facts & Assumptions

Given: A bull-free graph G, a split set SV(G), and vertices c,aV(G)S with c complete to S and a anticomplete to S.

[F1]

A set is split exactly when every outside vertex mixed on it has one of the two witnesses from the definition: either an induced three-vertex path, or a three-vertex configuration with exactly one edge among the three vertices (A split set in a bull-free graph).

[F2]

A module is a vertex set to which every outside vertex is complete or anticomplete (Modules of a graph, and the trivial modules).

[L1]

Bull-freeness is preserved by complementation (A graph is bull-free if and only if its complement is bull-free).

Proof

technique · direct
1.1

First claim: if xV(G)S is neither complete nor anticomplete to S, then either c is adjacent to a and x is adjacent to c, or c is nonadjacent to a and x is nonadjacent to a. Indeed, let S1 be the neighbors of x in S and S2=SS1; both are nonempty. By [F1], either there are u,vS1 and wS2 with u-v-w an induced path, or there are uS1 and v,wS2 with uwE(G) while uv,vwE(G). In the first case bull-freeness rules out both x-a and xc simultaneously, because otherwise {a,x,u,v,w} and then {x,v,w,c,a} would be bulls. In the second case bull-freeness similarly rules out both xc and x-a, because otherwise {x,u,w,c,v} and then {a,x,u,c,v} would be bulls.

F1givenalgebra
2.1

Let C be the set of vertices complete to S, let A be the set of vertices anticomplete to S, and let X=V(G)(SCA). Either every vertex of C has a neighbor in A, or every vertex of A has a nonneighbor in C: otherwise a vertex of C anticomplete to A and a vertex of A complete to C would contradict each other. Replacing G by G if necessary preserves bull-freeness, splitness, and modules by [L1], [F1], and [F2], so assume that every vertex of C has a neighbor in A. Step 1.1 then makes C complete to X. Let A be the set of vertices of A lying on an induced path x-a1--ak with xX and all aiA. We prove by induction on k that ak is complete to C. For k=1, if ca1 were a nonedge for some cC, step 1.1 applied to x,c,a1 would force xa1 to be a nonedge, a contradiction. For k>1, put a0=x and assume the result through ak1. Choose sS nonadjacent to ak2 when k=2, which is possible because x is mixed on S; for k>2 any sS works because ak2A. If some cC were nonadjacent to ak, then {s,c,ak2,ak1,ak} would be a bull: c,ak2,ak1 form its triangle, while s and ak are pendant at c and ak1. Hence A is complete to C.

step 1.1L1F1F2chooseinduction
3.1

Put Z=SXA. Every vertex of AA is anticomplete to Z: it is anticomplete to S by definition, and any path from it to XA through A has a shortest, hence induced, subpath that would put it in A. Every vertex of C is complete to Z by step 2.1 and the definition of C. Thus every outside vertex is complete or anticomplete to Z, so Z is a module by [F2]. The set Z is nontrivial because SZ and S>1, while cCZ, so ZV(G).

step 2.1F2

Depends on

Used by

Dependency tree · two levels

15 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources