Other results

Results named in the rest of Tau Ceti's TauCeti.QuantumGroups modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe Biedenharn–Elliott pentagon identity#

The Biedenharn–Elliott pentagon identity for the α₀ = 1 change-of-decomposition (F-matrix) entries sixJ of clebschGordanInclusion across all signed ladder modules L_a^ε ⊗ L_b^δ ⊗ L_c^ζ ⊗ L_d^θ at generic q.

TauCeti.UqSl2.sixJ_pentagon {q : ℂ} (hq : TauCeti.IsGenericQuantumParameter q) (ε δ ζ θ : ℤˣ)
  (a b c d e u w x y : ℕ) :
  TauCeti.UqSl2.sixJ hq ε δ (ζ * θ) a b y e u x * TauCeti.UqSl2.sixJ hq (ε * δ) ζ θ u c d e w y =
    ∑ z ∈ Finset.range (b + c + 1),
      TauCeti.UqSl2.sixJ hq δ ζ θ b c d x z y * TauCeti.UqSl2.sixJ hq ε (δ * ζ) θ a z d e w x *
        TauCeti.UqSl2.sixJ hq ε δ ζ a b c w u z

Lean

Formalized in Tau Ceti as TauCeti.UqSl2.sixJ_pentagon.

Sources

• Tau Ceti documentation: TauCeti.UqSl2.sixJ_pentagon
• Source of TauCeti.UqSl2.sixJ_pentagon in TauCeti/QuantumGroups/UqSl2/ClebschGordan/Pentagon.lean

LeanTauCeti.UqSl2.sixJ_pentagon

Uses 2

Statement usesTauCeti.UqSl2.LadderModule

Proof usesSchur's lemma, vanishing form

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.