Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

The symmetric Lovász Local Lemma under ep(d+1)1

Statement

Let dN and p0. Let (Ai)iI have a dependency digraph of maximum out-degree at most d. If P(Ai)p for every i and ep(d+1)1, then P(iAic)>0.

Facts & Assumptions

Given: A finite event family, its dependency digraph, and p,d satisfying the Statement.

[L1]

The asymmetric Local Lemma applies when P(Ai)xiij(1xj) with 0xi<1 (The asymmetric Lovász Local Lemma for finitely many events).

[L3]

exp(u+v)=exp(u)exp(v); natural powers preserve order on nonnegative bases; and positive inequalities may be multiplied and inverted using the ordered-field laws (The exponential addition formula exp(x+y)=exp(x)exp(y), Integer powers am, Laws of integer exponents, Monotonicity of xxn and of nan, The reals form a totally ordered field).

Proof

technique · cases
1.1

Suppose d=0 and set every xi=1/e. Applying [L2] at y=1 gives 2e, so 0<xi<1. The hypothesis gives p1/e=xi, and the empty neighbour product is 1, so [L1] applies.

assume-case zeroL1L2algebra
1.2

Suppose d1 and set every xi=1/(d+1). From [L2] at y=1/d and [L3], (1+1/d)de, hence (11/(d+1))d=(d/(d+1))d1/e.

assume-case positiveL2L3algebra
2.1

Each vertex has at most d out-neighbours, so xiij(1xj)1/(e(d+1))p by the hypothesis. Thus [L1] applies.

step 1.2L1L3algebra
3.1

The cases d=0 and d1 are exhaustive and both give positive probability that no bad event occurs.

step 1.1step 2.1cases-exhaustive

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 119 results over 31 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