+# Finite obstructions to normalized additive states

The state equations are homogeneous integer inequalities, except for the normalization at the unit. Their finite certificates are interpreted in the additive group completion, preserving catalysts in the original semiring.

inductive MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.StateConstraint (S : Type u_2) [Preorder S] : Type u_2

The homogeneous inequalities defining a normalized additive state. Both signs of the additive relation are included.

• lower {S : Type u_2} [Preorder S] (x : S) : StateConstraint S
• upper {S : Type u_2} [Preorder S] (x : S) : StateConstraint S
• addPos {S : Type u_2} [Preorder S] (x y : S) : StateConstraint S
• addNeg {S : Type u_2} [Preorder S] (x y : S) : StateConstraint S
• order {S : Type u_2} [Preorder S] (x y : S) (h : x ≤ y) : StateConstraint S
• detector {S : Type u_2} [Preorder S] (x : S) : StateConstraint S

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.stateConstraintVector {S : Type u_1} [CommSemiring S] [Preorder S] (R : S → ℕ) (d : S) (k : ℕ) (c : StateConstraint S) : S →₀ ℤ

Integer coefficient vector of a homogeneous state constraint.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.statePairing {S : Type u_1} (f : S → ℝ) : (S →₀ ℤ) →ₗ[ℤ] ℝ

Evaluation of a finite integer coefficient vector on a real-valued function.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.statePairing f = Finsupp.linearCombination ℤ f

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.statePairing_apply {S : Type u_1} (f : S → ℝ) (v : S →₀ ℤ) : (statePairing f) v = ∑ x ∈ v.support, ↑(v x) * f x

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.statePairing_single {S : Type u_1} (f : S → ℝ) (x : S) (n : ℤ) : (statePairing f) (Finsupp.single x n) = ↑n * f x

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.continuous_statePairing {S : Type u_1} (v : S →₀ ℤ) : Continuous fun (f : S → ℝ) => (statePairing f) v

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalizedStates_iff_stateConstraint {S : Type u_1} [CommSemiring S] [Preorder S] (R : S → ℕ) (d : S) (k : ℕ) (f : S → ℝ) : f ∈ normalizedStates (fun (x : S) => ↑(R x)) d ↑k ↔ f 1 = 1 ∧ ∀ (c : StateConstraint S), 0 ≤ (statePairing f) (stateConstraintVector R d k c)

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.stateConstraintLower {S : Type u_1} [CommSemiring S] [Preorder S] (c : StateConstraint S) : S

The ordinary monotonicity difference in a state constraint.

Equations

• One or more equations did not get rendered due to their size.
• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.stateConstraintLower (MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.StateConstraint.lower x) = 0
• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.stateConstraintLower (MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.StateConstraint.upper x) = x
• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.stateConstraintLower c = 0

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.stateConstraintUpper {S : Type u_1} [CommSemiring S] [Preorder S] (R : S → ℕ) (c : StateConstraint S) : S

The semiring element providing the upper endpoint of a state constraint.

Equations

• One or more equations did not get rendered due to their size.
• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.stateConstraintUpper R c = 0

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.stateConstraintDetector {S : Type u_1} [CommSemiring S] [Preorder S] (c : StateConstraint S) : S

The multiplier of the distinguished detector difference.

Equations

• One or more equations did not get rendered due to their size.
• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.stateConstraintDetector c = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.stateConstraintLower_le_upper {S : Type u_1} [CommSemiring S] [Preorder S] (R : S → ℕ) (hzero : ∀ (x : S), 0 ≤ x) (hbound : ∀ (x : S), x ≤ ↑(R x)) (c : StateConstraint S) : stateConstraintLower c ≤ stateConstraintUpper R c

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.stateConstraintVector_completion {S : Type u_1} [CommSemiring S] [Preorder S] (R : S → ℕ) (d : S) (k : ℕ) (c : StateConstraint S) : (Finsupp.linearCombination ℤ ⇑Algebra.GrothendieckAddGroup.of) (stateConstraintVector R d k c) = Algebra.GrothendieckAddGroup.of (stateConstraintUpper R c) - Algebra.GrothendieckAddGroup.of (stateConstraintLower c) + Algebra.GrothendieckAddGroup.of (d * stateConstraintDetector c) - k • Algebra.GrothendieckAddGroup.of (stateConstraintDetector c)

Interpreting a constraint in the group completion separates its ordinary order difference from its detector difference.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.no_stateConstraint_certificate {S : Type u_1} [CommSemiring S] [Preorder S] (R : S → ℕ) (d : S) (k : ℕ) (hzero : ∀ (x : S), 0 ≤ x) (hbound : ∀ (x : S), x ≤ ↑(R x)) (hadd : ∀ (a b c e : S), a ≤ b → c ≤ e → a + c ≤ b + e) (hno : ∀ (D s : S) (m : ℕ), 0 < m → ¬D + ↑m + d * s ≤ D + ↑k * s) {I : Type u_2} [Fintype I] (cs : I → StateConstraint S) : ¬∃ (m : ℕ), 0 < m ∧ ∃ (n : I → ℕ), ∑ i : I, n i • stateConstraintVector R d k (cs i) = -↑m • Finsupp.single 1 1

In the absence of a catalytic obstruction, no positive multiple of the negative unit is a natural combination of state-constraint vectors.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.finite_stateConstraint_solution {S : Type u_1} [CommSemiring S] [Preorder S] (R : S → ℕ) (d : S) (k : ℕ) (hzero : ∀ (x : S), 0 ≤ x) (hbound : ∀ (x : S), x ≤ ↑(R x)) (hadd : ∀ (a b c e : S), a ≤ b → c ≤ e → a + c ≤ b + e) (hno : ∀ (D s : S) (m : ℕ), 0 < m → ¬D + ↑m + d * s ≤ D + ↑k * s) {I : Type u_2} [Finite I] (cs : I → StateConstraint S) (H : Finset S) (hOne : 1 ∈ H) (hH : ∀ (i : I), (stateConstraintVector R d k (cs i)).support ⊆ H) : ∃ (f : S → ℝ), f 1 = 1 ∧ (∀ (i : I), 0 ≤ (statePairing f) (stateConstraintVector R d k (cs i))) ∧ ∀ x ∉ H, f x = 0

Every finite family of constraints supported on H has a normalized solution that vanishes outside H, provided no positive catalyst exists.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.bounded_finite_stateConstraint_solution {S : Type u_1} [CommSemiring S] [Preorder S] (R : S → ℕ) (d : S) (k : ℕ) (hzero : ∀ (x : S), 0 ≤ x) (hbound : ∀ (x : S), x ≤ ↑(R x)) (hadd : ∀ (a b c e : S), a ≤ b → c ≤ e → a + c ≤ b + e) (hno : ∀ (D s : S) (m : ℕ), 0 < m → ¬D + ↑m + d * s ≤ D + ↑k * s) (F : Finset (StateConstraint S)) : ∃ (f : S → ℝ), (∀ (x : S), 0 ≤ f x ∧ f x ≤ ↑(R x)) ∧ f 1 = 1 ∧ ∀ c ∈ F, 0 ≤ (statePairing f) (stateConstraintVector R d k c)

A finite collection of state constraints can be solved while keeping all coordinates in their rank intervals.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalizedStates_nonempty_of_no_catalyst {S : Type u_1} [CommSemiring S] [Preorder S] (R : S → ℕ) (d : S) (k : ℕ) (hzero : ∀ (x : S), 0 ≤ x) (hbound : ∀ (x : S), x ≤ ↑(R x)) (hadd : ∀ (a b c e : S), a ≤ b → c ≤ e → a + c ≤ b + e) (hno : ∀ (D s : S) (m : ℕ), 0 < m → ¬D + ↑m + d * s ≤ D + ↑k * s) : (normalizedStates (fun (x : S) => ↑(R x)) d ↑k).Nonempty

Absence of positive scalar-gain catalysts guarantees the existence of a normalized additive monotone state satisfying the detector inequality.