Parallel lowering for generated einsum outputs

This module selects and constructs exact task-parallel output traversal for large concrete einsums. Each task receives a contiguous range of the outer output axis and calls the arbitrary-rank output compiler. Scalar contractions remain unchanged, so their reduction order is preserved.

def TorchLean.Tensor.Internal.Elab.Impl.einsumOutputTaskCount (_factored : Bool) (outputShape : Shape) (contractionEntries : ℕ) : ℕ

Choose an arbitrary positive output-task count from static work.

The estimate counts source contraction terms because it is available for every scalar type and lowering strategy. Measurements show that task overhead still dominates a 512-by-512 contraction, while four output chunks substantially improve a 1024-by-1024 contraction. Once parallel execution is worthwhile, the count grows logarithmically with work and is bounded by the outer axis, so every generated chunk is nonempty.

The initial parallel width is a scheduling policy, not a correctness boundary: the executor and its proof accept every list length.

def TorchLean.Tensor.Internal.Elab.Impl.compileParallelEinsumOutput? (scalarType storage outputBufferType reference : Lean.Expr) (outputLengths : List Lean.Expr) (contractionEntries? : Option ℕ) (factored : Bool) (buildOutputLoops : List Lean.Expr → List Lean.Expr → Lean.Expr → Lean.Elab.TermElabM (Lean.Expr × Lean.Expr × Lean.Expr)) (compileNativeOutputFold : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Name → Lean.Elab.TermElabM (Lean.Expr × Lean.Expr)) : Lean.Elab.TermElabM (Option (Lean.Expr × Lean.Expr))

Compile any positive number of balanced contiguous ranges of a concrete output shape.

buildOutputLoops is the ordinary arbitrary-rank output compiler. compileNativeOutputFold replaces a finite outer fold with its certified native-counter implementation when the chunk length is portable. The result is none when shapes are symbolic or the static work policy rejects task launch.