Certified native flat pullbacks

This module compiles a certified output-to-source flat map into one native output loop and direct source-buffer reads. Rearrangement, repetition, and other shape-only transformations use this operation-independent lowering.

The generated term carries its pointwise equality to Rep.pullFlat. Concrete portable shapes use USize counters and indices; symbolic shapes remain on the existing general lowering.

def TorchLean.Tensor.Internal.Elab.Impl.compileNativePullFlat? (outputShape sourceTensor flatMap : Lean.Expr) (nativeSourceDimensions? : Option (List Lean.Expr) := none) : Lean.Elab.TermElabM (Option (Lean.Expr × Lean.Expr))

Compile one flat pullback to a certified native tensor fill when the output length is a portable concrete value.

def TorchLean.Tensor.Internal.Elab.Impl.compileNativeTransform? (checked hAxes inputFlatMap sourceTensor reference hSemanticReference : Lean.Expr) (hasPrecedingTransform : Bool) (concreteChecked? : Option Check.CheckedTransform := none) : Lean.Elab.TermElabM (Option Lean.Expr)

Compile a checked rearrangement or repeat, including any preceding shape-only chain, to one certified native output loop.