Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26
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 graph with at least two vertices is prime exactly when it is not obtained by substituting one graph on at least two vertices for a vertex of another graph on at least two vertices

Statement

Let G be a finite simple graph with V(G)2. Then G is prime (Prime graphs: those whose only modules are the trivial ones) if and only if there is no substitution G1[aG2] (Substituting one graph for a vertex of another) with V(G1)2 and V(G2)2 such that GG1[aG2].

Facts & Assumptions

Given: A finite simple graph G with V(G)2.

[F1]

G is prime when every module of G is trivial; equivalently, when G has no module M with 2M and MV(G)1 (Prime graphs: those whose only modules are the trivial ones).

[F2]

M is a module of G when the pair ({v},M) is pure for every vV(G)M (Modules of a graph, and the trivial modules).

[F3]

The vertex set of G1[aG2] is (V(G1){a})V(G2), a disjoint union; two vertices of V(G1){a} are adjacent there exactly when they are adjacent in G1, two vertices of V(G2) exactly when they are adjacent in G2, and uV(G1){a} is adjacent to xV(G2) exactly when u is adjacent to a in G1 (Substituting one graph for a vertex of another).

[L2]

For a module M of G: for all x,yM and all vV(G)M, vxE(G) if and only if vyE(G) (Three equivalent descriptions of a module: purity of every outside vertex, equality of outside neighbourhoods, and indistinguishability of the members).

[F4]

G[W]=(W,E(G)[W]2) (Subgraphs, induced subgraphs and spanning subgraphs).

[F5]

A graph isomorphism is a bijection φ:VW such that, for all distinct u,vV, {u,v}E if and only if {φ(u),φ(v)}F (Graph isomorphisms, automorphisms and graph complements).

[F6]

A bijection transports finiteness and cardinality: if A is finite and f:AB is a bijection then B=A (The cardinality A of a finite set).

Proof

technique · direct
1.1

Let θ:V(H)V(G) be an isomorphism and let M be a module of H. For vV(G)θ[M] the vertex θ1(v) lies outside M, so it is adjacent in H to every vertex of M or to none; since θ preserves and reflects adjacency, v is adjacent in G to every vertex of θ[M] or to none. Hence θ[M] is a module of G, and θ[M]=M, V(G)=V(H) and θ[M]=V(G) exactly when M=V(H).

F2F5F6
1.2

For the direction from a substitution to non-primality, suppose GG1[aG2] with V(G1)2 and V(G2)2, and write H=G1[aG2] and M=V(G2). Then M is a module of H by [L1], M2, and V(H)M=V(G1){a} is nonempty because V(G1)2, so MV(H).

L1F3given
1.3

For the converse direction, suppose G is not prime, so by [F1] it has a module M with 2M and MV(G)1; fix xM and put G2=G[M] and G1=G[(V(G)M){x}].

F1F4choose
2.1

In the first direction, step 1.1 applied to an isomorphism HG turns M into a module M of G with M=M2 and MV(G), so MV(G)1 and G is not prime by [F1].

step 1.1step 1.2F1F6
2.2

In the converse direction, V(G1){x}=V(G)M is disjoint from V(G2)=M and is nonempty because MV(G)1, and V(G2); so G1[xG2] is a substitution, its vertex set is (V(G)M)M=V(G), and V(G2)=M2 while V(G1)=V(G)M+12.

step 1.3F3F6
3.1

Still in the converse direction, take distinct p,qV(G). If both lie in V(G)M then {p,q} is an edge of G1[xG2] exactly when it is an edge of G1, hence exactly when it is an edge of G; if both lie in M the same holds with G2 in place of G1; and if pV(G)M and qM then {p,q} is an edge of G1[xG2] exactly when {p,x}E(G1), that is exactly when {p,x}E(G), which by [L2] applied to the module M with x,qM and pM holds exactly when {p,q}E(G).

step 1.3step 2.2F3F4L2
4.1

So in the converse direction G1[xG2] and G have the same vertex set and the same edges, hence G=G1[xG2] is a substitution with both factors on at least two vertices.

step 2.2step 3.1
5.1

Step 2.1 shows that a graph isomorphic to such a substitution is not prime, and step 4.1 shows that a graph that is not prime is such a substitution; these are the two directions of the stated equivalence.

step 2.1step 4.1

Depends on

Used by

Dependency tree · two levels

20 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