Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-09
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.

Local special copy trichotomy

Statement

Let H be a nonempty finite graph, gV(H), h=H, b,c>0, and a=b+(1+c)h. Let 0<x1/2 and let A,B be disjoint vertex subsets of a finite graph G, such that every vA has at least xB nonneighbors in B. At least one of the following holds:

  • Some BB has BxB and indHg(G[B])<xbBh1.
  • indH(G)xaABh1.
  • Some AA, BB have AxaA, BxaB and eG(A,B)2xcAB.

Integer powers use the empty-function convention 00=1.

Facts & Assumptions

Given: H,g,h,b,c,a,x,A,B,G as in the statement, with the stated nonneighbor bound.

[F1]
[F2]

For finite sets X,Y and a relation RX×Y, xXRx  =  R  =  yYRy. (Double counting: xXRx=R=yYRy for a relation between finite sets).

Proof

1.1

If A=, the second lower bound is zero. If B= and h2, it is also zero. If h=1, then indH(G)=GAxaA even when B is empty. Hence assume A,B nonempty and h2, and that the first and second alternatives both fail.

given
2.1

List the edges at g as gh1,,ghd, and let Hr retain precisely the first r of them, with all other adjacencies unchanged. Count special induced embeddings of Hr taking g to A and other labels to B; denote the number by τr. For each vA, its nonneighbor set Bv has BvxB. Failure of the first alternative gives at least xbBvh1xb+h1Bh1 embeddings of Hg there. Extending by gv and summing disjoint fibres by [F2] yields τ0xb+h1M, where M=ABh1>0.

F2step 1.1
3.1

Failure of the second alternative gives τd<xaMxb+h1+cdM, since dh1. Thus d>0 and there is a first r{1,,d} with τr<xb+h1+crM. Its predecessor satisfies τr1xb+h1+c(r1)M2xaM>0, since a(b+h1+c(r1))=1+c(hr+1)1 and x1/2. Also τr<xcτr1.

step 2.1algebra
4.1

Put w=hr. For each induced embedding ψ of H{g,w} into B, let UψBimψ contain the valid images of w for Hg. Let VψA contain the valid images of g for Hr1w, using this intermediate graph, not Hw. Let nψ and eψ count respectively nonedges and edges between Vψ,Uψ. The only remaining pair is gw: a nonedge completes Hr1 and an edge completes Hr. Conversely every special embedding restricts to exactly one such ψ. Therefore [F2] gives nψ=τr1 and eψ=τr.

F2step 3.1
5.1

There are at most Bh2 possible ψ by [F1]. Discard those with nψ<τr1/(2Bh2). Their total is at most τr1/2, so the retained family has total at least τr1/2>0. If every retained ψ had eψ>2xcnψ, summing would give τr>xcτr1, impossible. Some retained ψ therefore has eψ2xcnψ.

F1step 3.1step 4.1
6.1

For this ψ, UψVψnψτr1/(2Bh2)xaAB. Since UψB and VψA, this implies VψxaA and UψxaB. Moreover eψ2xcnψ2xcUψVψ. Set A=Vψ, B=Uψ. These satisfy the third alternative and complete the proof.

step 5.1step 3.1algebra

Source notes

Proof/convention locator: Bucic, Nguyen, Scott and Seymour, Induced subgraph density I, 3.1 complete proof.

Depends on

Used by

Dependency tree · two levels

28 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