Certified transform index compilation

This module compiles the flat-index function of a checked rearrangement or repeat while elaborating the surrounding expression. The generated program contains only the resulting row-major arithmetic; parser data, axis lookup, and checked-plan interpretation remain in erased correctness proofs.

Symbolic dimensions remain symbolic arithmetic in the generated expression; the returned theorem still identifies that program with the independent coordinate semantics.

def TorchLean.Tensor.Internal.Elab.Impl.explicitComposition (domain outer inner : Lean.Expr) : Lean.MetaM Lean.Expr

Build function composition as an explicit lambda.

Generated index maps are executable programs. Lambda form exposes their stored composition without unfolding checked-plan definitions.

partial def TorchLean.Tensor.Internal.Elab.Impl.flatIndexProgramCost (map : Lean.Expr) (fuel : ℕ := 1024) : ℕ

Estimate arithmetic complexity in a generated flat-index map.

Only value-level arithmetic contributes to the estimate. Dependent bounds, types, and correctness proofs are deliberately ignored because they are erased before execution. Unrecognized expressions contribute zero; this is not a cost model for arbitrary functions. The estimate chooses between composing a shape-only chain and materializing its certified native result.

def TorchLean.Tensor.Internal.Elab.Impl.maxFusedFlatIndexCost : ℕ

Heuristic cost limit for fusing an inherited flat-index map.

The weighted estimate reflects native arithmetic cost: quotient and remainder are more expensive than addition or multiplication. The threshold is independent of tensor rank and transformation kind. It is not a timing guarantee.

def TorchLean.Tensor.Internal.Elab.Impl.shouldFuseFlatIndex (map : Lean.Expr) : Bool

Report whether an inherited flat-index map should remain fused.

def TorchLean.Tensor.Internal.Elab.Impl.checkedFlatProjection (checked hAxes : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Compile a checked output-to-input flat projection.

The executable result is specialized row-major arithmetic when the reflected plan reduces. Its proof connects that arithmetic directly to linearization of the plan's independent coordinate projection, without unfolding the checked plan's proof fields.