Character.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The character inequality from the three-sector degeneration

The retained tensor has three branches sharing its actual first-input space. Their two remaining coordinate intervals determine matching branch labels. The uniform three-branch tag inequality and polynomial degeneration then yield the character inequality of Section 5.2 before symmetrization.

def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.branchFamily line 27
Source documentation
The actual three retained tensors in their original ambient spaces.
```
def branchFamily (a h : ℕ) (b : Fin 3) :
    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.branchFamily_zero line 31
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.branchFamily_one line 34
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.branchFamily_two line 37
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.yLabel line 41
Source documentation
Label a second-leg coordinate by its interval.
```
def yLabel (a h : ℕ) (j : YIndex a h) : Fin 3 :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.zLabel line 45
Source documentation
Label a third-leg coordinate by its corresponding interval.
```
def zLabel (a h : ℕ) (k : ZIndex a h) : Fin 3 :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.branchFamily_labels line 49
Source documentation
Every nonzero branch coefficient lies in the two matching labelled sectors.
```
theorem branchFamily_labels (a h : ℕ) (b : Fin 3) (i : Fin a)
    (j : YIndex a h) (k : ZIndex a h) (hn : branchFamily a h b i j k ≠ 0) :
    yLabel a h j = b ∧ zLabel a h k = b := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.branchFamily, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.yLabel, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.zLabel
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.sum_branchFamily line 74
Source documentation
The branch family sums to exactly the retained tensor.
```
theorem sum_branchFamily (a h : ℕ) :
    (∑ b : Fin 3, branchFamily a h b) = retained a h := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.branchFamily, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.retained
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.value_retained_le_source line 80
Source documentation
The character comparison uses the actual polynomial degeneration.
```
theorem value_retained_le_source (χ : Character) (a h : ℕ) :
    χ.value (retained a h) ≤ χ.value (source a h) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.retained, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.source
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.value_sharedFirst_branchFamily line 86
Source documentation
Both interval labels can be recovered without changing the common first input, so the tagged branch tensor has precisely the retained tensor's value.
```
theorem value_sharedFirst_branchFamily (χ : Character) (a h : ℕ) :
    χ.value (sharedFirstTensor (branchFamily a h)) = χ.value (retained a h) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character, OAI.MatrixMultiplication.AuxiliarySeparation.sharedFirstTensor, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.branchFamily, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.retained
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.branchFamily_nonzero line 91
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.uniform_branchFamily_product line 99
Source documentation
The uniform branch product combines the two outer convolution values.
```
theorem uniform_branchFamily_product (χ : Character) (a h : ℕ)
    (ha : 0 < a) (hh : 0 < h) :
    (∏ b, χ.value (branchFamily a h b) ^ (FiniteLaw.uniform (Fin 3)).mass b) =
      χ.value (convolution a h) ^ (2 / 3 : ℝ) *
        χ.value (exchangedConvolution a h) ^ (1 / 3 : ℝ) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.branchFamily, OAI.MatrixMultiplication.AuxiliarySeparation.convolution, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.exchangedConvolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.convolution_tripling_tag line 123
Source documentation
The per-character three-sector inequality, before multiplication over the six tensor-leg permutations. All tensor values are actual convolution values, with only the middle branch exchanging its last two legs.
```
theorem convolution_tripling_tag (χ : Character) (a h : ℕ)
    (ha : 0 < a) (hh : 0 < h) :
    (3 : ℝ) ^ χ.pX * χ.value (convolution a h) ^ (2 / 3 : ℝ) *
      χ.value (fun i s r => convolution a h i r s) ^ (1 / 3 : ℝ) ≤
        χ.value (convolution a (3 * h + a - 1)) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character, OAI.MatrixMultiplication.AuxiliarySeparation.convolution