Lowered rearrangement equivalence

Compiler-level congruence theorems connect checked row-major index certificates to primitive tensor programs.

theorem TorchLean.Tensor.Internal.Lowering.rearrangeTensor_apply_eq_of_linearIndex_eq {α : Type u_1} [Storage α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.rearrange) (inputTensor : checked.InputTensor α) (outputCoordinate : Coord checked.value.output) (inputCoordinate : Coord checked.value.normalized.input) (hLinearIndex : rearrangeLinearIndex checked.value.axisLength checked.value.normalized.inputAxes checked.value.normalized.outputAxes ↑outputCoordinate.linearize = ↑inputCoordinate.linearize) : Rep.get (rearrangeTensor checked hKind inputTensor) outputCoordinate = Rep.get inputTensor inputCoordinate

Evaluate a checked rearrangement at any input coordinate selected by its verified row-major index map.

This pointwise form avoids unfolding grouped coordinate equivalences in downstream correspondence theorems. It applies to arbitrary ranks, grouping, ungrouping, ellipses, and symbolic axis lengths.

theorem TorchLean.Tensor.Internal.Lowering.rearrangeTensor_eq_of_equivalent {α : Type u} [Storage α] (first second : Check.CheckedTransform) (hFirstKind : first.value.normalized.kind = Check.TransformKind.rearrange) (hSecondKind : second.value.normalized.kind = Check.TransformKind.rearrange) (hInputShape : first.value.normalized.input = second.value.normalized.input) (hOutputShape : first.value.output = second.value.output) (hEquivalent : first.RearrangeEquivalent second hFirstKind hSecondKind hInputShape hOutputShape) (inputTensor : first.InputTensor α) : rearrangeTensor first hFirstKind inputTensor = cast ⋯ (rearrangeTensor second hSecondKind (cast ⋯ inputTensor))

Equivalent checked rearrangements compile to equal primitive tensor programs. This is the compiler-level congruence theorem used by proof automation for differently spelled but extensionally equal patterns.

theorem TorchLean.Tensor.Internal.Lowering.rearrangeTensor_eq_of_linearIndex_eq {α : Type u_1} [Storage α] (first second : Check.CheckedTransform) (hFirstKind : first.value.normalized.kind = Check.TransformKind.rearrange) (hSecondKind : second.value.normalized.kind = Check.TransformKind.rearrange) (hInputShape : first.value.normalized.input = second.value.normalized.input) (hOutputShape : first.value.output = second.value.output) (hLinearIndex : ∀ (outputIndex : Fin first.value.output.size), rearrangeLinearIndex first.value.axisLength first.value.normalized.inputAxes first.value.normalized.outputAxes ↑outputIndex = rearrangeLinearIndex second.value.axisLength second.value.normalized.inputAxes second.value.normalized.outputAxes ↑((finCongr ⋯) outputIndex)) (inputTensor : first.InputTensor α) : rearrangeTensor first hFirstKind inputTensor = cast ⋯ (rearrangeTensor second hSecondKind (cast ⋯ inputTensor))

Two checked rearrangements compile to the same tensor program when their compact row-major index maps agree.

Unlike enumerating all concrete coordinates, the premise is a single arithmetic formula over an arbitrary output index. This is suitable both for general hand-written proofs and for reducing reflected literal plans inside the einops tactic.

theorem TorchLean.Tensor.Internal.Lowering.rearrangeTensor_comp_eq_of_linearIndex_eq {α : Type u_1} [Storage α] (first second direct : Check.CheckedTransform) (hFirstKind : first.value.normalized.kind = Check.TransformKind.rearrange) (hSecondKind : second.value.normalized.kind = Check.TransformKind.rearrange) (hDirectKind : direct.value.normalized.kind = Check.TransformKind.rearrange) (hMiddleShape : first.value.output = second.value.normalized.input) (hInputShape : first.value.normalized.input = direct.value.normalized.input) (hOutputShape : second.value.output = direct.value.output) (hLinearIndex : ∀ (outputIndex : Fin second.value.output.size), rearrangeLinearIndex first.value.axisLength first.value.normalized.inputAxes first.value.normalized.outputAxes (rearrangeLinearIndex second.value.axisLength second.value.normalized.inputAxes second.value.normalized.outputAxes ↑outputIndex) = rearrangeLinearIndex direct.value.axisLength direct.value.normalized.inputAxes direct.value.normalized.outputAxes ↑((finCongr ⋯) outputIndex)) (inputTensor : first.InputTensor α) : rearrangeTensor second hSecondKind (cast ⋯ (rearrangeTensor first hFirstKind inputTensor)) = cast ⋯ (rearrangeTensor direct hDirectKind (cast ⋯ inputTensor))

Two successive checked rearrangements equal one direct rearrangement when the composite of their compact row-major index maps equals the direct map.

All three plans and all physical-shape transports are arbitrary. The theorem therefore covers transpositions, grouping and ungrouping, ellipses, and their compositions without introducing a separate representation of composed plans.