Einsum reports

This module reports checked axes, contraction work, generated loops, and the correctness chain for concrete einsum certificates.

def TorchLean.Tensor.Internal.Report.Impl.concreteEinsumReport (checked scalarType : Lean.Expr) (correctnessTheorem : String) : Lean.MetaM (Option String)

Decode a concrete einsum certificate into its axis analysis, semantic stages, generated loops, and correctness chain.