Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated
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.

Pentagon in fusion-tree coordinates

Statement

Let a,b,c,d be four simple input charges and t a simple total charge. The root associator identity

αa,b,c⊗d∘αa⊗b,c,d=(id⁡a⊗αb,c,d)∘αa,b⊗c,d∘(αa,b,c⊗id⁡d)

has equal matrices along its two routes in the fusion-tree bases. If A1,A2,A3 are the three successive matrices on the right and A4,A5 the two successive matrices on the left, then

A3A2A1=A5A4.

Each matrix coefficient sums over every intermediate simple charge and every multiplicity-basis index.

Facts & Assumptions

Given: a unitary fusion category, simple objects a,b,c,d, and a simple total charge t.

[F1]

Monoidal category: the associator satisfies the pentagon equation displayed in the Statement for all objects, including tensor products that are not simple.

[F2]

F-symbol as a recoupling matrix: an associator move between two fusion-tree bases has matrix F, with the row/column convention and all vertex multiplicity indices specified there.

[F3]

Fusion-tree basis and dimension recursion: each parenthesized tree basis is a complete orthonormal basis indexed by all admissible internal charges and vertex multiplicity indices.

Proof

1.1F1F2F3construct

Fix the source and target parenthesized tensor products in the pentagon. For each intermediate parenthesization, decompose every tensor product into simple summands and choose the tree basis of [F3]. Each associator in [F1] acts on these coordinates by the appropriate direct sum of F blocks from [F2], with identity factors on vertices it does not change. Thus the two sides of [F1] have coordinate matrices A3A2A1 and A5A4, respectively.

2.1F1F2F3step 1.1algebra

For fixed endpoint basis indices x and z, let u,v range over the complete composite indices of the two intermediate trees on the three-move route, and let w range over the complete composite indices of the intermediate tree on the two-move route. Matrix multiplication gives ∑u,v(A3)z,v(A2)v,u(A1)u,x=∑w(A5)z,w(A4)w,x. Here each composite index consists of every simple internal charge together with every multiplicity-basis index at its vertices. Equality follows because the morphisms in [F1] are equal and [F3] supplies bases of the same Hom space; coordinates in a basis are unique.

3.1F3step 2.1∎

The endpoint indices x,z were arbitrary, so all entries of the two route matrices agree, proving A3A2A1=A5A4 with all intermediate charge and multiplicity sums included. All sums are finite by finite semisimplicity.

Pentagon diagram

The vertices are the five parenthesizations of a⊗b⊗c⊗d; each arrow is the indicated associator. The diagram encodes exactly the two composites stated and proved above; the proof uses the equations and coordinate expansion, not the drawing.

diagram failed to render:
((a\otimes b)\otimes c)\otimes d
  \arrow[r,"\alpha_{a\otimes b,c,d}"]
  \arrow[d,"\alpha_{a,b,c}\otimes\operatorname{id}_d"']
& (a\otimes b)\otimes(c\otimes d)
  \arrow[r,"\alpha_{a,b,c\otimes d}"]
& a\otimes(b\otimes(c\otimes d)) \\
(a\otimes(b\otimes c))\otimes d
  \arrow[r,"\alpha_{a,b\otimes c,d}"']
& a\otimes((b\otimes c)\otimes d)
  \arrow[ru,"\operatorname{id}_a\otimes\alpha_{b,c,d}"']
&

Depends on

Used by

Dependency tree · two levels

13 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