StateObstruction.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

+# 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 OAI.MatrixMultiplication.AuxiliarySeparation.StateConstraint line 28
Source documentation
The homogeneous inequalities defining a normalized additive state. Both signs of the additive relation are included.
```
inductive StateConstraint (S : Type*) [Preorder S] where
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.stateConstraintVector line 37
Source documentation
Integer coefficient vector of a homogeneous state constraint.
```
def stateConstraintVector (R : S → ℕ) (d : S) (k : ℕ)
    (c : StateConstraint S) : S →₀ ℤ := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.StateConstraint
def OAI.MatrixMultiplication.AuxiliarySeparation.statePairing line 49
Source documentation
Evaluation of a finite integer coefficient vector on a real-valued function.
```
def statePairing (f : S → ℝ) : (S →₀ ℤ) →ₗ[ℤ] ℝ :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.statePairing_apply line 53
theorem OAI.MatrixMultiplication.AuxiliarySeparation.statePairing_single line 58
theorem OAI.MatrixMultiplication.AuxiliarySeparation.continuous_statePairing line 63
theorem OAI.MatrixMultiplication.AuxiliarySeparation.normalizedStates_iff_stateConstraint line 68
def OAI.MatrixMultiplication.AuxiliarySeparation.stateConstraintLower line 104
Source documentation
The ordinary monotonicity difference in a state constraint.
```
def stateConstraintLower (c : StateConstraint S) : S :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.StateConstraint
def OAI.MatrixMultiplication.AuxiliarySeparation.stateConstraintUpper line 111
def OAI.MatrixMultiplication.AuxiliarySeparation.stateConstraintDetector line 119
Source documentation
The multiplier of the distinguished detector difference.
```
def stateConstraintDetector (c : StateConstraint S) : S :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.StateConstraint
theorem OAI.MatrixMultiplication.AuxiliarySeparation.stateConstraintLower_le_upper line 124
theorem OAI.MatrixMultiplication.AuxiliarySeparation.stateConstraintVector_completion line 138
Source documentation
Interpreting a constraint in the group completion separates its ordinary order difference from its detector difference.
```
theorem stateConstraintVector_completion (R : S → ℕ) (d : S) (k : ℕ)
    (c : StateConstraint S) :
    Finsupp.linearCombination ℤ (Algebra.GrothendieckAddGroup.of (M := S))
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.StateConstraint

theorem OAI.MatrixMultiplication.AuxiliarySeparation.no_stateConstraint_certificate line 156

Source documentation

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

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

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.StateConstraint, OAI.MatrixMultiplication.AuxiliarySeparation.stateConstraintVector

theorem OAI.MatrixMultiplication.AuxiliarySeparation.finite_stateConstraint_solution line 179

Source documentation

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

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

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.StateConstraint, OAI.MatrixMultiplication.AuxiliarySeparation.stateConstraintVector, OAI.MatrixMultiplication.AuxiliarySeparation.statePairing

theorem OAI.MatrixMultiplication.AuxiliarySeparation.bounded_finite_stateConstraint_solution line 227

Source documentation

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

theorem bounded_finite_stateConstraint_solution (R : S → ℕ) (d : S) (k : ℕ)
    (hzero : ∀ x : S, 0 ≤ x) (hbound : ∀ x : S, x ≤ (R x : S))
    (hadd : ∀ a b c e : S, a ≤ b → c ≤ e → a + c ≤ b + e)
    (hno : ∀ (D s : S) (m : ℕ), 0 < m →
      ¬D + (m : S) + d * s ≤ D + (k : S) * s)
    (F : Finset (StateConstraint S)) :
    ∃ f : S → ℝ, (∀ x, 0 ≤ f x ∧ f x ≤ R x) ∧ f 1 = 1 ∧
      ∀ c ∈ F, 0 ≤ statePairing f (stateConstraintVector R d k c) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.StateConstraint, OAI.MatrixMultiplication.AuxiliarySeparation.statePairing, OAI.MatrixMultiplication.AuxiliarySeparation.stateConstraintVector

theorem OAI.MatrixMultiplication.AuxiliarySeparation.normalizedStates_nonempty_of_no_catalyst line 277

Source documentation

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

theorem normalizedStates_nonempty_of_no_catalyst (R : S → ℕ) (d : S) (k : ℕ)
    (hzero : ∀ x : S, 0 ≤ x) (hbound : ∀ x : S, x ≤ (R x : S))
    (hadd : ∀ a b c e : S, a ≤ b → c ≤ e → a + c ≤ b + e)
    (hno : ∀ (D s : S) (m : ℕ), 0 < m →
      ¬D + (m : S) + d * s ≤ D + (k : S) * s) :
    (normalizedStates (fun x ↦ (R x : ℝ)) d k).Nonempty := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.normalizedStates