TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

A $k$ -uniform hypergraph is $2$ -colourable when every edge meets at most $d$ other edges and $e (d + 1) \leq 2^{k - 1}$

Statement

Let $k \geq 1$ and $d \in N$ . Suppose every edge of a finite $k$ -uniform hypergraph meets at most $d$ other edges and $e (d + 1) \leq 2^{k - 1} .$ Then the hypergraph is two-colourable.

Facts & Assumptions

Given: A finite $k$ -uniform hypergraph satisfying the Statement.

[L1]

A $k$ -uniform edge contains exactly $k$ vertices ( $r$ -uniform hypergraphs and complete balanced $r$ -partite $r$ -graphs $K_{s, \dots, s}^{(r)}$ ).

[L2]

Product weights factor coordinatewise, and finite Fubini factors sums over disjoint coordinate blocks (The finite product of finite probability spaces, Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

[L3]

A dependency graph requires each bad event to be independent of every conjunction of complements indexed by its non-neighbours (Dependency digraphs for a finite family of bad events).

[L4]

If bad events have probability at most $p$ , a dependency graph of maximum degree $d$ , and $e p (d + 1) \leq 1$ , then they can all be avoided with positive probability (The symmetric Lovász Local Lemma under $e p (d + 1) \leq 1$ ).

[L5]

An event of positive probability in a finite probability space is nonempty (An event of positive probability in a finite probability space is nonempty).

[L6]

For every real $x$ , $1 + x \leq \exp (x)$ ; in particular $e = \exp (1) \geq 2$ ( $1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$ ).

Proof

technique · direct

1.1

Colour vertices independently and fairly. For each edge $F$ , let $A_{F}$ be the event that $F$ is monochromatic. The two monochromatic assignments are disjoint and each has product weight $2^{- k}$ , so $P (A_{F}) = 2^{1 - k}$ .

L1L2

1.2

Join two bad events when their edges meet. If all edges indexing a complement conjunction are disjoint from $F$ , that conjunction depends only on coordinates outside $F$ ; finite Fubini in [L2] factors its intersection probability with $A_{F}$ . Thus [L3] makes the edge-intersection graph a dependency graph, and its degree is at most $d$ .

L2L3

2.1

The numerical hypothesis is $e 2^{1 - k} (d + 1) \leq 1$ , so [L4] gives positive probability that no edge is monochromatic.

step 1.1step 1.2L4algebra

3.1

By [L5], the positive-probability event in step 2.1 contains a colouring, and that colouring is proper. For $k = 1$ , [L6] gives $e (d + 1) \geq 2 > 1 = 2^{k - 1}$ , so the numerical hypothesis cannot hold; the empty-edge case for admissible parameters is immediate.

step 2.1L5L6algebra∎

Depends on

Used by

Checking the symmetric local-lemma condition for a sparse uniform hypergraph Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 111 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Matousek and J. Vondrak, The Probabilistic Method, Section 5.2 (standard reference, not scraped)

A kk-uniform hypergraph is 22-colourable when every edge meets at most dd other edges and e(d+1)≤2k−1e(d+1)≤2k−1