Alphabeta Math
LemmaStatement: AI-adaptedProof: 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.

The induced copies of H1 in G are counted by summing, over the induced embeddings of H1v, the number of vertices that extend them at v

Statement

Let H1 be a finite simple graph with h1=V(H1)1, let vV(H1), write H1v for the induced subgraph H1[V(H1){v}], and let G be a finite simple graph with n=V(G). For an induced embedding φ of H1v into G define its extension set

Xφ:={uV(G)φ[V(H1){v}]:the map extending φ by vu is an induced embedding of H1 into G}.

Then, writing Ψ for the set of induced embeddings of H1v into G,

indH1(G)=φΨXφ,Ψnh11.

Facts & Assumptions

Given: A finite simple graph H1 with h1=V(H1)1, a vertex vV(H1), and a finite simple graph G with n=V(G); the sets Φ of induced embeddings of H1 into G and Ψ of induced embeddings of H1v into G.

[F1]

An induced embedding of H in G is an injection φ:V(H)V(G) such that, for all distinct x,yV(H), xyE(H) if and only if φ(x)φ(y)E(G) (Induced embeddings and induced copies of a graph).

[F2]

indH(G) is the number of induced embeddings of H into G (The induced-embedding count indH(G)).

[F3]

H1[W]=(W,E(H1)[W]2), so two vertices of W are adjacent in H1[W] exactly when they are adjacent in H1 (Subgraphs, induced subgraphs and spanning subgraphs).

[L1]

For finite sets X,Y and a relation RX×Y with row fibres Rx and column fibres Ry, one has xXRx=R=yYRy (Double counting: xXRx=R=yYRy for a relation between finite sets, A relation RX×Y between finite sets, its row fibres Rx and its column fibres Ry).

[F4]

For a finite index set S and a constant c, iSc=Sc (The sum iSai over a finite index set, and its product form).

[L2]

For finite sets A and B, the set AB of functions BA is finite with AB=AB (The set AB of functions BA between finite sets is finite, with AB=AB).

Proof

technique · direct
1.1

If ψΦ then its restriction ψ to V(H1){v} is injective, and for distinct x,yV(H1){v} the condition xyE(H1v) is the condition xyE(H1), which holds exactly when ψ(x)ψ(y)E(G); so ψΨ, and it is the only member of Ψ that ψ restricts to.

F1F3
1.2

Let RΨ×Φ consist of the pairs (φ,ψ) whose second entry restricts to the first. Both Φ and Ψ are sets of functions between finite sets, hence finite.

F1L2L3
2.1

The column fibre of R at ψΦ has exactly one element by step 1.1, so ψΦRψ=Φ.

step 1.1step 1.2F4
2.2

The row fibre of R at φΨ is carried bijectively onto Xφ by ψψ(v): the map is injective because ψ is determined by φ together with ψ(v), and its image is exactly Xφ, because a vertex u arises as some ψ(v) precisely when extending φ by vu gives an induced embedding of H1, and injectivity of that extension is exactly the requirement uφ[V(H1){v}].

step 1.2F1given
3.1

Double counting R therefore gives φΨXφ=R=Φ=indH1(G).

step 2.1step 2.2L1F2
4.1

Every member of Ψ is a function from V(H1){v}, a set of h11 elements, to V(G), so Ψ is a subset of a set of size nh11 and Ψnh11.

step 3.1F1L2L3

Depends on

Used by

Dependency tree · two levels

33 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