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

For finite graphs, the simplicial-tree notion agrees with the published finite-tree notion

Statement

Let $X$ be a finite oriented graph with no loops and no parallel geometric edges, and let $∣ X ∣$ be its underlying finite simple graph obtained by forgetting orientations and identifying each pair ${e, \overset{ˉ}{e}}$ to one geometric edge. Then $X$ is a simplicial tree if and only if $∣ X ∣$ is a tree in the published finite-graph sense.

Facts & Assumptions

Given: A finite oriented graph $X$ .

[L1]

On a finite vertex set, the simple-graph walk, path, cycle, connectedness, and component notions agree with the published finite-graph notions. (On a finite vertex set the graph notions agree, and on connected graphs the two path distances agree)

[L2]

A finite nonempty graph is a published tree if and only if every two vertices are joined by a unique path. (Equivalent characterisations of a nonempty tree by unique paths, edge count, minimal connectivity and maximal acyclicity)

[L3]

An oriented graph is a simplicial tree if and only if every two vertices are joined by a unique reduced path. (A simplicial graph is a tree exactly when every two vertices are joined by a unique reduced path)

Proof

technique · direct

1.1

By the no-loop/no-parallel-edge hypothesis and [L1], a reduced simplicial path in $X$ is exactly a path in the underlying finite simple graph $∣ X ∣$ , and connectedness means the same thing in both models. Therefore the uniqueness criterion in [L3] translates verbatim into the uniqueness criterion in [L2].

L1L2L3given

2.1

Applying [L2] and [L3] to the translation from step 1.1 shows that $X$ is a simplicial tree exactly when $∣ X ∣$ is a published finite tree.

L2L3step 1.1∎

Depends on

Used by

Regular Cayley trees of free groups Example
FALSE: the published finite-tree definition already covers Bass-Serre trees False statement

Dependency tree · two levels

21 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

C. Loh, Geometric Group Theory: An Introduction (2015 course version) (standard reference, not scraped)
Jean-Pierre Serre, Trees (standard reference, not scraped)