Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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)∣\nu(G)+\rho(G)=|V(G)| when GG has no isolated vertex

Statement

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

Facts & Assumptions

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

[F1]

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

[F2]

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

Proof

technique · constructive
1.1

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

F1F2construct
1.2

Thus ρ(G)≤∣V∣−ν(G)\rho(G)\le|V|-\nu(G).

F2
1.3

Let FF 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∣|V|-|F| edges.

F1
2.1

Therefore ν(G)≥∣V∣−ρ(G)\nu(G)\ge|V|-\rho(G) by step 1.3, while step 1.2 gives the reverse inequality, proving ν(G)+ρ(G)=∣V∣\nu(G)+\rho(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 · next 3 levels

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