Alphabeta Math
LemmaStatement: 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.

Finite groups acting on trees have a global fixed vertex after subdivision

Statement

Let a finite group G act on a simplicial tree T. Then the induced action on the barycentric subdivision T fixes a vertex.

Facts & Assumptions

Given: A finite group G acting on a simplicial tree T.

[L1]

Barycentric subdivision preserves the tree and removes edge inversions. (Barycentric subdivision removes edge inversions while preserving the tree)

[L2]

The path metric on a simplicial tree is geodesic and integer-valued. (The path metric on a simplicial tree is geodesic and integer-valued)

Proof

technique · direct
1.1

Replace T by its barycentric subdivision T using [L1]. Choose a vertex v of T. Because G is finite, the orbit Gv is finite, and the union of the geodesics joining pairs of orbit vertices is therefore a finite G-invariant subtree UT.

L1L2givenconstruct
2.1

Let D be the diameter of U, choose vertices x,yU with d(x,y)=D, and let m be the midpoint of the unique geodesic from x to y. In a finite tree every diameter geodesic has the same midpoint: if two diameters had different midpoints, the unique path joining those midpoints would extend one of them past length D, contradicting maximality. So m depends only on U, not on the chosen diameter.

L2step 1.1algebra
3.1

Any automorphism of U sends diameter geodesics to diameter geodesics, so it fixes the intrinsic midpoint m from step 2.1. If D is even, m is a vertex of U and is fixed. If D is odd, m is the midpoint of a unique geometric edge of U, so every element of G preserves that edge setwise. The action on T is without inversions by [L1], hence no element can swap the two endpoints; both endpoints are fixed. In either case the induced action on T fixes a vertex.

L1L2step 2.1algebra

Depends on

Used by

Dependency tree · two levels

6 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