feat: add exceptional Lie tensor square decomposition eval problems

[kim-em]

Summary

Two paired benchmark problems about tensor square decompositions of specific irreducible representations of the exceptional Lie algebras g₂ and e₈, both defined via Mathlib's Serre construction (LieAlgebra.g₂, LieAlgebra.e₈):

• g2_irrep_tensor_square_decomp: a 64-dim irrep V exists (V(ω₁+ω₂)) whose tensor square decomposes into 14 isotypic components.
• e8_irrep_tensor_square_decomp: a 779247-dim irrep V exists (V(ω₁+ω₈)) whose tensor square decomposes into 40 isotypic components.

Both dimensions and isotypic counts were verified externally with LiE. The 64-dim and 779247-dim irreps are unique at those dimensions, so the count of distinct isomorphism classes is well-defined.

Statement design

isotypicComponents lives in Mathlib/RingTheory/SimpleModule/Isotypic.lean and is defined for modules over a ring. To apply it to a Lie module M, we transport the action through the universal enveloping algebra: a LieModule R L M extends to a Module (UniversalEnvelopingAlgebra R L) M via the universal property. Mathlib doesn't currently provide this as an instance, so the statement uses an inline letI to construct the canonical Module (U(g)) (V ⊗[ℂ] V) action — keeping the statement self-contained when extracted into the generated Challenge.lean.

Difficulty

Both proofs require essentially all of semisimple Lie algebra representation theory: Serre's theorem giving finite-dimensionality, the existence and uniqueness of irreducible representations indexed by dominant weights (none of which is currently in Mathlib), Weyl's complete reducibility, and tensor-product decomposition machinery. The g₂ version is the smaller training wheel; the e₈ version is the headline.

Test plan

• lake exe lean-eval validate-manifest passes
• lake exe lean-eval check-problem-build passes (only sorry warnings remain)
• lake exe lean-eval generate --problem g2_irrep_tensor_square_decomp succeeds and the workspace builds
• lake exe lean-eval generate --problem e8_irrep_tensor_square_decomp succeeds and the workspace builds

🤖 Prepared with Claude Code