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

Energy lies in $[0, 1]$ and cannot decrease under refinement

Statement

For every vertex partition $P$ of a finite graph, $0 \leq q (P) \leq 1.$ If $Q$ refines $P$ , then $q (Q) \geq q (P) .$

Facts & Assumptions

Given: A finite graph and vertex partitions $P, Q$ with $Q$ refining $P$ .

[L1]

The energy is the weighted mean of the squares of the densities of ordered pairs of parts (The mean-square density, or energy, of a vertex partition).

[L2]

For a finite random variable $Z$ , Cauchy--Schwarz gives $(E Z)^{2} \leq E (Z^{2})$ (Cauchy-Schwarz for finite random variables: $E [X Y]^{2} \leq E [X^{2}] E [Y^{2}]$ ).

Proof

technique · direct

1.1

Every density belongs to $[0, 1]$ , and the nonnegative weights $∣ A ∣ ∣ B ∣ / n^{2}$ in [L1] sum to $1$ when the graph has order $n > 0$ . Thus $0 \leq q (P) \leq 1$ ; the null-graph convention gives the same conclusion when $n = 0$ .

L1algebra

1.2

Fix $A, B \in P$ . Choose an ordered pair $(x, y)$ uniformly from $A \times B$ , and let $Z$ be the density between the two $Q$ -parts containing $x$ and $y$ . Double-counting the relevant ordered edge incidences gives $E Z = d (A, B)$ .

givenL1algebra

2.1

By [L2], the weighted mean square of the refined densities inside $A \times B$ is at least $d (A, B)^{2}$ .

step 1.2L2

3.1

Multiply step 2.1 by $∣ A ∣ ∣ B ∣ / n^{2}$ and sum over all ordered $A, B \in P$ . The two sides become $q (Q)$ and $q (P)$ by [L1], proving monotonicity.

step 2.1L1algebra∎

Depends on

Used by

Dependency tree · next 3 levels

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

Y. Zhao, Graph Theory and Additive Combinatorics, Lemma 2.1.12 (standard reference, not scraped)

Energy lies in [0,1][0,1] and cannot decrease under refinement