Verified einsum scalar product generation

This module assembles direct operand reads into the source-ordered scalar product used by a checked einsum. Factoring contraction-invariant prefixes and suffixes requires a Semiring instance; it is not a floating-point reassociation optimization. Each result retains a pointwise certificate.

def TorchLean.Tensor.Internal.Elab.Impl.compileEinsumInputProduct (checked inputTensorFamily scalarType : Lean.Expr) (inputTensors : List Lean.Expr) (inputViews : List (Option (Lean.Expr × Lean.Expr × Lean.Expr))) (inputDimensions : List (List Lean.Expr)) (inputAxes : List (List Check.EinsumAxis)) (outputAxes semanticContractedAxes contractedAxes : List Check.EinsumAxis) (outputLengths semanticContractedLengths contractedLengths : List Lean.Expr) (contractionCoordinateMap? : Option Lean.Expr) : Lean.Elab.TermElabM (Lean.Expr × Lean.Expr × Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr))

Generate the direct scalar product used by a literal einsum and an erased pointwise proof that it equals the generic verified implementation.

Output coordinates are computed before the contraction lambda. Eligible multi-term output-index bases are hoisted from the contraction loop. With multiple contracted axes, every operand's outer-axis contributions are combined into a base that the loop compiler floats outside the innermost contraction loop. Over a semiring, maximal source-order prefixes and suffixes that do not use a contracted axis are also returned as optional factors.