Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-02
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.

Gallai's identity: ν(G)+ρ(G)=∣V(G)∣ when G has no isolated vertex

Statement

If a finite graph G=(V,E) has no isolated vertex, then its matching and edge-cover numbers satisfy ν(G)+ρ(G)=∣V∣.

Facts & Assumptions

Given: A finite graph G=(V,E) without isolated vertices and a maximum matching M.

[F1]

A matching has pairwise endpoint-disjoint edges, and ∣M∣=ν(G) when M is maximum (Matchings, saturated vertices, maximal and maximum matchings, perfect matchings and ν(G)).

[F2]

An edge cover meets every vertex and ρ(G) is the least cardinality of one (Vertex covers, edge covers and the covering numbers τ(G) and ρ(G)).

Proof

technique · constructive
1.1

The M-exposed vertices are independent, or an edge between two would enlarge M; choose one incident edge for each exposed vertex and adjoin them to M, obtaining an edge cover of ∣M∣+(∣V∣−2∣M∣)=∣V∣−∣M∣ edges.

F1F2construct
1.2

Thus ρ(G)≤∣V∣−ν(G).

F2
1.3

Let F be an inclusion-minimal edge cover. Its graph has no cycle, since a cycle edge could be deleted, and no path of length three, since its middle edge could be deleted; hence every component is a star and choosing one edge from each component is a matching of ∣V∣−∣F∣ edges.

F1
2.1

Therefore ν(G)≥∣V∣−ρ(G) by step 1.3, while step 1.2 gives the reverse inequality, proving ν(G)+ρ(G)=∣V∣.

step 1.2step 1.3discharge-construct∎

Remarks

  • The no-isolated-vertex hypothesis is load-bearing: an isolated vertex has no incident edge, so no edge cover exists.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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