Characters decrease under polynomial degeneration

Finite interpolation expresses a polynomial's leading coefficient as a sum of evaluations. Applying it after tensor powering gives only a linear overhead, which disappears in the exponential growth rate. No continuity assumption on the character is used.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_scale_le {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (c : K) (T : Foundation.Tensor K X Y Z) : (χ.value fun (x : X) (y : Y) (z : Z) => c * T x y z) ≤ χ.value T

Scalar multiplication is a restriction, including when the scalar is zero.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_scale {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (c : K) (hc : c ≠ 0) (T : Foundation.Tensor K X Y Z) : (χ.value fun (x : X) (y : Y) (z : Z) => c * T x y z) = χ.value T

Nonzero scalar multiplication preserves a character.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_sum_le {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] {ι : Type} [Fintype ι] (T : ι → Foundation.Tensor K X Y Z) : (χ.value fun (x : X) (y : Y) (z : Z) => ∑ i : ι, T i x y z) ≤ ∑ i : ι, χ.value (T i)

Adding tensors is a restriction of their independent direct sum.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_coefficient_le {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] [IsAlgClosed K] (P : Foundation.Tensor (Polynomial K) X Y Z) (d D : ℕ) (hdegree : ∀ (x : X) (y : Y) (z : Z), (P x y z).degree ≤ ↑D) : (χ.value fun (x : X) (y : Y) (z : Z) => (P x y z).coeff d) ≤ ∑ i : Fin (D + 1), χ.value fun (x : X) (y : Y) (z : Z) => Polynomial.eval (interpolationNode K D i) (P x y z)

Exact interpolation bounds any polynomial coefficient by the sum of the character values of finitely many evaluation tensors.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_le_of_polynomialApproximation {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] [IsAlgClosed K] {U : Foundation.Tensor K X Y Z} {r d D : ℕ} (A : U.PolynomialApproximation r d D) {b : ℝ} (hb : 0 ≤ b) (hbound : ∀ (t : K), t ≠ 0 → (χ.value fun (x : X) (y : Y) (z : Z) => Polynomial.eval t (A.polynomial x y z)) ≤ b) : χ.value U ≤ b

A uniform bound on nonzero evaluations bounds the leading tensor. The proof uses tensor powers and removes their linear interpolation overhead.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_polynomialRestrictionDegeneration_le {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] [IsAlgClosed K] {X' Y' Z' : Type} [Fintype X'] [Fintype Y'] [Fintype Z'] {T : Foundation.Tensor K X Y Z} {U : Foundation.Tensor K X' Y' Z'} {k Lx Ly Lz : ℕ} (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) : χ.value U ≤ χ.value T

The character axioms imply monotonicity under polynomial degeneration. Continuity of the character is neither assumed nor used.