Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

A cycle graph is not finite type

Statement refuted

Every finite connected graph is the Dynkin diagram of a finite-type Cartan matrix, so positive definiteness imposes no restriction on connected diagrams.

Facts & Assumptions

Given: An integer m3, the cycle graph G on m vertices, and the matrix A=2IAdj(G).

[L1]

A finite-type Cartan matrix is symmetrizable to a positive definite matrix: there is a diagonal D with positive diagonal entries such that DAD1 is symmetric positive definite (Properties of finite-type Cartan matrices).

[L2]

The Cartan matrix of a based root system has aijaji=1 on each simple edge and 0 on nonedges, so the diagram of A would be G (Dynkin diagram with edge multiplicity and arrow convention).

Proof

technique · explicit witness
1.1

The matrix A=2IAdj(G) is symmetric and satisfies aii=2, aij=1 for adjacent ij and aij=0 otherwise; its diagram, as in [L2], is the cycle G on m3 vertices.

L2algebra
1.2

The nonzero vector x=(1,,1) satisfies Ax=0, because every row has diagonal entry 2 and exactly two entries 1. Equivalently xTAx=2m2m=0. Hence A is not positive definite; moreover every diagonal conjugate DAD1 has the nonzero null vector Dx, so no symmetric diagonal conjugate can be positive definite.

givenalgebra
2.1

By [L1] a finite-type Cartan matrix must be symmetrizable to a positive definite matrix; A is not. Moreover, [L2] makes A the only Cartan matrix with this unoriented simple-edge cycle: on each edge the nonpositive integral entries have product 1, so both are 1. Thus the cycle is not a finite-type Dynkin diagram even though it is finite and connected. This explicit family suffices to refute the claimed statement; no broader tree assertion is needed.

L1L2step 1.1step 1.2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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