Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13
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.

Every finite graph H with χ(H)=r is an ordinary subgraph of Kr[s] for some s

Statement

If a finite graph H has χ(H)=r, then H is an ordinary subgraph of Kr[s] for some s≥1. For the null graph, r=0 and the assertion uses the convention K0[1] is null.

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

A proper k-vertex-colouring is a map c:V→k with c(u)≠c(v) for every edge {u,v}, its fibres are the colour classes, and χ(G)=min⁡{k∈N:G is k-colourable} (Proper vertex colourings and chromatic number).

[F2]

The balanced blowup H[s] replaces each vertex by an independent s-set and each edge by all cross edges between the corresponding parts (Ordinary-subgraph extremal number ex⁡(n,H), Turán graph Tn,r, and balanced blowup H[s]).

[F3]

Every finite set has a unique natural-number cardinality (The cardinality ∣A∣ of a finite set).

Proof

technique · place colour classes into blowup parts
1.1

If H is null, it embeds in K0[1]. Otherwise choose a proper colouring with colours 1,…,r and let s≥1 be the largest colour-class size. Inject each colour class into the corresponding size-s independent part of Kr[s].

givenF1F2F3
2.1

Every edge of H joins vertices of different colours, and all cross-part edges occur in Kr[s]. The combined injection therefore preserves every edge and is an ordinary-subgraph embedding.

step 1.1givenF1F2∎

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