Degeneration.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

The actual three-sector polynomial degeneration

The interval weights of SectorWeights act by diagonal local maps on the coefficient tensor C(a, 3h+a-1). Shifting every third-leg weight by one makes the local maps polynomial. Their restriction is exactly X * retained + X^2 * erased, so the existing polynomial-restriction degeneration interface applies with leading order one and local degree bounds (0,1,1).

abbrev OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex line 26
abbrev OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex line 27
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.source line 30
Source documentation
The source coefficient tensor, with its actual shared first-input space.
```
def source (a h : ℕ) : Tensor ℂ (Fin a) (YIndex a h) (ZIndex a h) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.source_ne_zero_iff line 33
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.retained line 44
Source documentation
The weight-zero part in the original coordinate spaces.
```
def retained (a h : ℕ) : Tensor ℂ (Fin a) (YIndex a h) (ZIndex a h) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.erased line 48
Source documentation
The positive-weight part, all of whose supported terms have weight one.
```
def erased (a h : ℕ) : Tensor ℂ (Fin a) (YIndex a h) (ZIndex a h) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor line 52
Source documentation
The left retained branch, still in the common ambient coordinate spaces.
```
def leftTensor (a h : ℕ) : Tensor ℂ (Fin a) (YIndex a h) (ZIndex a h) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor line 56
Source documentation
The middle retained branch; its first leg is the actual shared first leg.
```
def middleTensor (a h : ℕ) : Tensor ℂ (Fin a) (YIndex a h) (ZIndex a h) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor line 60
Source documentation
The right retained branch in the original coordinate spaces.
```
def rightTensor (a h : ℕ) : Tensor ℂ (Fin a) (YIndex a h) (ZIndex a h) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.retained_eq_three_branches line 65
Source documentation
The retained tensor is exactly the sum of the three stated branches, with coefficient one on each and the original first-leg coordinates shared.
```
theorem retained_eq_three_branches (a h : ℕ) :
    retained a h = leftTensor a h + middleTensor a h + rightTensor a h := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.retained, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.source_eq_retained_add_erased line 91
Source documentation
Every source term belongs either to the retained tensor or the erased one.
```
theorem source_eq_retained_add_erased (a h : ℕ) :
    source a h = retained a h + erased a h := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.source, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.retained, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.erased
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.normalizedPolynomial line 100
Source documentation
The normalized polynomial family appearing in the unshifted weights.
```
def normalizedPolynomial (a h : ℕ) :
    Tensor (Polynomial ℂ) (Fin a) (YIndex a h) (ZIndex a h) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftMap line 105
Source documentation
The first local map fixes the common input basis.
```
def leftMap (a : ℕ) (output input : Fin a) : Polynomial ℂ :=
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleMap line 109
Source documentation
The second local map assigns weight one to the middle interval.
```
def middleMap (a h : ℕ) (output input : YIndex a h) : Polynomial ℂ :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightMap line 114
Source documentation
Shift the third-leg weights by one, giving weight zero to the middle interval and weight one to the two outer intervals.
```
def rightMap (a h : ℕ) (output input : ZIndex a h) : Polynomial ℂ :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.polynomial line 118
Source documentation
One simultaneous polynomial restriction of the whole source tensor.
```
def polynomial (a h : ℕ) :
    Tensor (Polynomial ℂ) (Fin a) (YIndex a h) (ZIndex a h) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.polynomial_apply line 123
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.polynomial_identity line 131
Source documentation
The shifted polynomial restriction has precisely two possible degrees.
```
theorem polynomial_identity (a h : ℕ) (i : Fin a) (j : YIndex a h)
    (k : ZIndex a h) :
    polynomial a h i j k =
      X * C (retained a h i j k) + X ^ 2 * C (erased a h i j k) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.polynomial, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.retained, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.erased
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.polynomial_eq_X_mul_normalized line 144
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.polynomial_coeff line 150
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftMap_degree line 160
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleMap_degree line 164
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightMap_degree line 169
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.restriction line 176
Source documentation
The three-sector construction is an actual polynomial restriction degeneration in the existing tensor API, with leading order one.
```
def restriction (a h : ℕ) :
    Tensor.PolynomialRestrictionDegeneration (source a h) (retained a h) 1 0 1 1 where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.source, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.retained
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.restriction_basePolynomial line 195
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.normalizedPolynomial_eval line 199
Source documentation
Evaluation of the normalized family has exactly the paper's form.
```
theorem normalizedPolynomial_eval (a h : ℕ) (t : ℂ) (i : Fin a)
    (j : YIndex a h) (k : ZIndex a h) :
    (normalizedPolynomial a h i j k).eval t =
      retained a h i j k + t * erased a h i j k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.normalizedPolynomial, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.retained, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.erased
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.normalizedPolynomial_eval_restriction line 208
Source documentation
At nonzero parameters, the unshifted normalized polynomial is still an ordinary restriction: divide the first local map by the parameter.
```
theorem normalizedPolynomial_eval_restriction (a h : ℕ) (t : ℂ) (ht : t ≠ 0) :
    (fun i j k => (normalizedPolynomial a h i j k).eval t) =
      Tensor.restrict
        (fun output input => if input = output then t⁻¹ else 0)
        (fun output input => (middleMap a h output input).eval t)
        (fun output input => (rightMap a h output input).eval t)
        (source a h) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.normalizedPolynomial, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleMap, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightMap, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.source
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.retained_power_rankAtMost line 233
Source documentation
Existing interpolation gives a rank bound with only linear overhead after tensor powering.
```
theorem retained_power_rankAtMost (a h r n : ℕ)
    (hsource : Tensor.RankAtMost (source a h) r) :
    Tensor.RankAtMost (Tensor.power (retained a h) n) ((2 * n + 1) * r ^ n) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.source, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.retained