Branches.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

Coordinate identifications of the three retained sectors

Each outer branch is a zero extension of C(a,h), using the same first-leg coordinates. The middle branch is a zero extension after reversing the first coordinate and exchanging the second and third tensor legs.

def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftY line 24
Source documentation
Embed the left second-leg interval.
```
def leftY (a h : ℕ) (r : Fin h) : YIndex a h :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftZ line 28
Source documentation
Embed the left third-leg interval.
```
def leftZ (a h : ℕ) (s : Fin (a + h - 1)) : ZIndex a h :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleY line 32
Source documentation
Embed the middle second-leg interval, which carries the convolution output.
```
def middleY (a h : ℕ) (s : Fin (a + h - 1)) : YIndex a h :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleZ line 36
Source documentation
Embed the middle third-leg interval, which carries the second input.
```
def middleZ (a h : ℕ) (r : Fin h) : ZIndex a h :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightY line 40
Source documentation
Embed the right second-leg interval.
```
def rightY (a h : ℕ) (r : Fin h) : YIndex a h :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightZ line 45
Source documentation
Embed the right third-leg interval.
```
def rightZ (a h : ℕ) (s : Fin (a + h - 1)) : ZIndex a h :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftY_injective line 49
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftZ_injective line 54
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleY_injective line 59
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleZ_injective line 66
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightY_injective line 73
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightZ_injective line 80
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor_pullback line 88
Source documentation
Pulling back the left block gives ordinary convolution.
```
theorem leftTensor_pullback (a h : ℕ) :
    Tensor.pullback id (leftY a h) (leftZ a h) (leftTensor a h) =
      convolution a h := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftY, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftZ, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor, OAI.MatrixMultiplication.AuxiliarySeparation.convolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor_pullback line 101
Source documentation
Pulling back the translated right block also gives ordinary convolution.
```
theorem rightTensor_pullback (a h : ℕ) :
    Tensor.pullback id (rightY a h) (rightZ a h) (rightTensor a h) =
      convolution a h := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightY, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightZ, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor, OAI.MatrixMultiplication.AuxiliarySeparation.convolution
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.exchangedConvolution line 117
Source documentation
Exchange the two outer convolution legs while retaining the original input order in the displayed coefficient equation.
```
def exchangedConvolution (a h : ℕ) :
    Tensor ℂ (Fin a) (Fin (a + h - 1)) (Fin h) :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor_pullback line 123
Source documentation
The middle branch is exactly convolution with its last two legs exchanged; the first-leg reversal occurs solely in this individual branch identification.
```
theorem middleTensor_pullback (a h : ℕ) :
    Tensor.pullback Fin.rev (middleY a h) (middleZ a h) (middleTensor a h) =
      exchangedConvolution a h := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleY, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleZ, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.exchangedConvolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor_support line 140
Source documentation
All nonzero left-branch coordinates lie in the displayed embeddings.
```
theorem leftTensor_support (a h : ℕ) (i : Fin a) (j : YIndex a h)
    (k : ZIndex a h) (hn : leftTensor a h i j k ≠ 0) :
    (∃ r, leftY a h r = j) ∧ (∃ s, leftZ a h s = k) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftY, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftZ
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor_support line 152
Source documentation
All nonzero right-branch coordinates lie in the translated embeddings.
```
theorem rightTensor_support (a h : ℕ) (i : Fin a) (j : YIndex a h)
    (k : ZIndex a h) (hn : rightTensor a h i j k ≠ 0) :
    (∃ r, rightY a h r = j) ∧ (∃ s, rightZ a h s = k) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightY, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightZ
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor_support line 166
Source documentation
All nonzero middle-branch coordinates lie in the exchanged embeddings.
```
theorem middleTensor_support (a h : ℕ) (i : Fin a) (j : YIndex a h)
    (k : ZIndex a h) (hn : middleTensor a h i j k ≠ 0) :
    (∃ u, Fin.rev u = i) ∧ (∃ s, middleY a h s = j) ∧
      (∃ r, middleZ a h r = k) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleY, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleZ
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor_eq_extension line 183
Source documentation
The left block is the zero extension of the ordinary convolution tensor.
```
theorem leftTensor_eq_extension (a h : ℕ) :
    leftTensor a h = Tensor.restrict
      (fun x i => if i = x then 1 else 0)
      (fun y r => if leftY a h r = y then 1 else 0)
      (fun z s => if leftZ a h s = z then 1 else 0) (convolution a h) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftY, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftZ, OAI.MatrixMultiplication.AuxiliarySeparation.convolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor_eq_extension line 201
Source documentation
The right block is the zero extension along the translated coordinates.
```
theorem rightTensor_eq_extension (a h : ℕ) :
    rightTensor a h = Tensor.restrict
      (fun x i => if i = x then 1 else 0)
      (fun y r => if rightY a h r = y then 1 else 0)
      (fun z s => if rightZ a h s = z then 1 else 0) (convolution a h) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightY, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightZ, OAI.MatrixMultiplication.AuxiliarySeparation.convolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor_eq_extension line 220
Source documentation
The middle block is the zero extension of the exchanged convolution, with one reversible change of basis on its first leg.
```
theorem middleTensor_eq_extension (a h : ℕ) :
    middleTensor a h = Tensor.restrict
      (fun x i => if Fin.rev i = x then 1 else 0)
      (fun y s => if middleY a h s = y then 1 else 0)
      (fun z r => if middleZ a h r = z then 1 else 0) (exchangedConvolution a h) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleY, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleZ, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.exchangedConvolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.value_leftTensor line 234
Source documentation
Every character assigns the left branch the value of C(a,h).
```
theorem value_leftTensor (χ : Character) (a h : ℕ) :
    χ.value (leftTensor a h) = χ.value (convolution a h) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor, OAI.MatrixMultiplication.AuxiliarySeparation.convolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.value_rightTensor line 241
Source documentation
Translation of the outer coordinates preserves the right-branch value.
```
theorem value_rightTensor (χ : Character) (a h : ℕ) :
    χ.value (rightTensor a h) = χ.value (convolution a h) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor, OAI.MatrixMultiplication.AuxiliarySeparation.convolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.value_middleTensor line 248
Source documentation
The middle-branch value is the value of the exchanged convolution tensor.
```
theorem value_middleTensor (χ : Character) (a h : ℕ) :
    χ.value (middleTensor a h) = χ.value (exchangedConvolution a h) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.exchangedConvolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.exchangedConvolution_nonzero line 255
Source documentation
Exchanging two tensor legs preserves nonzeroness.
```
theorem exchangedConvolution_nonzero {a h : ℕ} (ha : 0 < a) (hh : 0 < h) :
    exchangedConvolution a h ≠ 0 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.exchangedConvolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor_nonzero line 263
Source documentation
The left retained branch is nonzero in every positive size.
```
theorem leftTensor_nonzero {a h : ℕ} (ha : 0 < a) (hh : 0 < h) :
    leftTensor a h ≠ 0 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor_nonzero line 271
Source documentation
The translated right branch is nonzero in every positive size.
```
theorem rightTensor_nonzero {a h : ℕ} (ha : 0 < a) (hh : 0 < h) :
    rightTensor a h ≠ 0 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor_nonzero line 279
Source documentation
The exchanged middle branch is nonzero in every positive size.
```
theorem middleTensor_nonzero {a h : ℕ} (ha : 0 < a) (hh : 0 < h) :
    middleTensor a h ≠ 0 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor