Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16
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 small energy increment makes fine-pair densities close to their coarse densities almost everywhere

Statement

Let Q refine a vertex partition P of an n-vertex graph. For x,y∈V(G), let Px,Py be their P-parts and Qx,Qy their Q-parts. If q(Q)−q(P)≤ϵ3, then fewer than or equal to ϵn2 ordered pairs (x,y) satisfy ∣d(Qx,Qy)−d(Px,Py)∣>ϵ.

Facts & Assumptions

Given: Partitions and a parameter satisfying the Statement.

[L1]

Energy is the weighted mean square of part-pair densities, and refinement cannot lower it (The mean-square density, or energy, of a vertex partition, Energy lies in [0,1] and cannot decrease under refinement).

[L2]

For a nonnegative finite random variable X and a>0, Markov's inequality gives Pr⁡(X≥a)≤EX/a (Markov's inequality on a finite probability space).

Proof

technique · direct
1.1givenL1algebra

Choose an ordered vertex pair (x,y) uniformly and set ZP=d(Px,Py) and ZQ=d(Qx,Qy). On each coarse pair, double-counting gives E(ZQ∣Px,Py)=ZP.

2.1step 1.1L1algebra

Expanding the square and using the conditional identity in step 1.1 gives E((ZQ−ZP)2)=E(ZQ2)−E(ZP2)=q(Q)−q(P)≤ϵ3.

3.1step 2.1L2algebra

Apply [L2] to (ZQ−ZP)2 with threshold ϵ2. The probability that ∣ZQ−ZP∣>ϵ is at most ϵ3/ϵ2=ϵ.

4.1step 3.1algebra∎

Multiplying this probability by the n2 ordered vertex pairs proves the asserted exceptional-pair bound.

Depends on

Used by

Dependency tree · two levels

8 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