Symbolic einsum certificates

This module constructs Check.CheckedEinsum values when tensor dimensions are symbolic Nat expressions rather than reducible literals. The pattern and operand ranks are still checked by computation. Repeated labels, singleton broadcasting, logical-axis sources, and the expected output shape are then proved against the original symbolic dimensions.

The resulting certificate feeds the same semantic lowering and native kernel compiler used for concrete shapes. Symbolic dimensions change how the checked plan is built, not what einsum means.

def TorchLean.Tensor.Internal.Elab.Impl.einsumAxisExpression? (assignments : List (Check.EinsumAxis × Lean.Expr)) (axis : Check.EinsumAxis) : Option Lean.Expr

Find the symbolic length assigned to a reflected einsum axis.

theorem TorchLean.Tensor.Internal.Elab.Impl.einsum_axis_source_of_occurrence (axisLength : Check.EinsumAxis → ℕ) (axis : Check.EinsumAxis) (length : ℕ) (before after : List (Check.EinsumAxis × ℕ)) (hLength : length = axisLength axis) : (axisLength axis == 1 || (before ++ (axis, length) :: after).any fun (occurrence : Check.EinsumAxis × ℕ) => occurrence.1 == axis && occurrence.2 == axisLength axis) = true

An explicit occurrence certifies that a logical axis length has an input source. Keeping the witness outside List.any lets symbolic elaboration prove only the dimension equality instead of simplifying every earlier occurrence.

def TorchLean.Tensor.Internal.Elab.Impl.symbolicCheckedEinsumExpr (source : String) (pattern : Syntax.EinsumPattern) (inputDimensions : List (List Lean.Expr)) (expectedType? : Option Lean.Expr) : Lean.Elab.TermElabM (Lean.Expr × List (Check.EinsumAxis × Lean.Expr) × Lean.Expr × Lean.Expr)

Construct a checked einsum directly from symbolic natural-number dimensions.

The executable checker validates the complete rank and pattern structure on same-rank singleton witnesses. The actual dimensions are then used in every proof-valued field of CheckedEinsum. An expected output tensor shape, when available, names the corresponding logical output lengths and is checked by the same broadcasting and source-occurrence invariants.