Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-28
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 Laplacian is positive semidefinite and sends the all-ones vector to zero

Statement

Let G be a finite simple graph on n vertices, let L(G) be its Laplacian matrix, and let 1Rn be the all-ones column vector. Then:

  1. xTL(G)x0 for every xRn;
  2. L(G)1=0.

In particular, L(G) is positive semidefinite.

Facts & Assumptions

Given: A finite simple graph G with Laplacian L and an oriented incidence matrix B.

[F1]

Every column of an oriented incidence matrix has one 1 and one 1 (An oriented incidence matrix of a finite simple graph).

Proof

technique · direct
1.1

For every xRn, [L1] gives xTLx=xTBBTx=(BTx)T(BTx). The right-hand side is a sum of squares of real numbers, so it is nonnegative.

L1algebra
1.2

Let 1 be the all-ones vector. Because each column of B has one 1 and one 1, [F1] implies that every column sum of B is 0, so BT1=0. Using [L1] again gives L1=BBT1=B0=0.

F1L1algebra
2.1

Step 1.1 proves positive semidefiniteness, and step 1.2 proves that the all-ones vector lies in the kernel.

step 1.1step 1.2

Depends on

Used by

Dependency tree · two levels

7 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