Alphabeta Math
TheoremStatement: AI-adaptedProof: Literature-sourced
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.

Block incidence tree and containment contract

Statement

In a finite connected graph with an edge, distinct nontrivial blocks meet in at most one vertex; any common vertex is a cutvertex. Every edge belongs to one block. The bipartite incidence graph of blocks and cutvertices is a tree. Any 2-connected subgraph is contained in a block.

External input

Diestel defines a block as a maximal connected subgraph without a cutvertex, and explicitly identifies its three possibilities: a maximal 2-connected subgraph, a bridge with its endpoints, or an isolated vertex (printed p. 64). A connected graph with an edge has no isolated vertex, so his blocks are exactly the nontrivial blocks in Cutvertices, 2-connected pieces and nontrivial blocks. The same paragraph states that distinct blocks overlap in at most one vertex, which is then a cutvertex of the ambient graph, and that every edge lies in a unique block.

The block graph is defined on printed p. 65 using disjoint vertex classes consisting of the blocks and cutvertices, with adjacency precisely when the cutvertex belongs to the block. Lemma 3.1.4 on printed p. 66 states that this graph is a tree for a connected graph. Here a tree means a connected acyclic simple graph, as in Cycles, trees and forests in a simple graph on an arbitrary vertex set. Block nodes are formal labels distinct from vertex nodes, so the incidence graph is bipartite even if graph vertices themselves are sets.

The containment clause is independently established by Finite maximal extension of a 2-connected subgraph, using finiteness and subgraph containment as in Subgraphs, induced subgraphs and spanning subgraphs. The edge-partition clause is independently established by Every edge belongs to exactly one nontrivial block, through its cycle, union and nonbridge prerequisites. These local proofs supplement the source; the overlap/cutvertex and incidence-tree assertions remain explicitly imported. No local proof or independent audit of those residual assertions is claimed.

Depends on

Used by · 2

Dependency tree · 2 levels

Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.

External dependencies

Reinhard Diestel, Graph Theory, sixth edition, Chapter 3 · Section 3.1, printed p. 64 block definition/overlap paragraph; p. 65 block graph definition; p. 66 Lemma 3.1.4

In a finite connected graph with an edge, distinct nontrivial blocks meet in at most one vertex; any common vertex is a cutvertex. Every edge belongs to one block. The bipartite incidence graph of blocks and cutvertices is a tree. Any 2-connected subgraph is contained in a block.

Hypotheses: Finite connected graph with an edge; 2-connected means at least three vertices; blocks here omit isolated vertices, irrelevant under these hypotheses.

Reading limits: For this repair, read the extracted text of the chapter preview at printed pp. 64–66: the block definition, overlap/cutvertex and edge-partition paragraph, the bipartite block graph definition and Lemma 3.1.4. Rendered page images were requested but were not available as inspectable images through the tool response. Lemma 3.1.4 is stated without proof in this preview; its proof is not claimed reconstructed or audited. The 2-connected containment and edge-partition clauses also have the local intermediate proofs linked below. No other chapter proofs or original-article prerequisites are imported.

Sources