Obstruction.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The rank obstruction behind the preliminary spectral state

The finite catalyst is kept fixed while first tensor powers, then exponent slack, then the number of copies are varied. The hypotheses below isolate the rank inequalities supplied by the catalytic comparison; they do not assert the existence of a tensor spectrum or the separation argument producing that comparison.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_pow_le line 26
Source documentation
Tensor powers of a fixed exact matrix algorithm retain their exact rank bound after identifying the product coordinates with one matrix dimension.
```
theorem exactMatrixRank_pow_le (u j : ℕ) :
    exactMatrixRank (u ^ j) ≤ exactMatrixRank u ^ j := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank
theorem OAI.MatrixMultiplication.AuxiliarySeparation.floor_rank_power_bounds line 43
Source documentation
A floor approximation uses at most n^j copies of a fixed matrix algorithm and loses at most one factor of its fixed matrix dimension.
```
theorem floor_rank_power_bounds {u n R : ℕ} (hu : 2 ≤ u) (hn : 1 ≤ n)
    {τ : ℝ} (hτ : 0 < τ) (hR : (R : ℝ) ≤ (u : ℝ) ^ τ) (j : ℕ) :
    let l := ⌊(j : ℝ) * Real.logb (u : ℝ) (n : ℝ) / τ⌋₊
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.catalytic_rank_bound_at_slack line 88
Source documentation
At fixed n and exponent slack, every admissible matrix rank budget forces the exponential growth rate of the catalytic comparison. The constant R is fixed before the tensor-power parameter varies.
```
theorem catalytic_rank_bound_at_slack {d n K R : ℕ}
    (hd : 0 < d) (hn : 1 ≤ n)
    (hbound : ∀ j : ℕ, 1 ≤ j → ∀ g : ℕ, exactMatrixRank g ≤ n ^ j →
      exactMatrixRank (d ^ j * g) ≤ R * K ^ j)
    {δ : ℝ} (hδ : 0 < δ) :
    (d : ℝ) ^ exactRankExponent *
      (n : ℝ) ^ (exactRankExponent / (exactRankExponent + δ)) ≤ K := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank, OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent
theorem OAI.MatrixMultiplication.AuxiliarySeparation.catalytic_rank_obstruction line 148
Source documentation
The numerical rank consequence of a single fixed finite catalyst is incompatible with k < d^ν. The same D and R occur for every n and every tensor power. No uniform bound on the approximation block selected after an exponent slack is assumed.
```
theorem catalytic_rank_obstruction {d k D R : ℕ} (hd : 0 < d)
    (hbound : ∀ n : ℕ, 1 ≤ n → ∀ j : ℕ, 1 ≤ j → ∀ g : ℕ,
      exactMatrixRank g ≤ n ^ j →
      exactMatrixRank (d ^ j * g) ≤ R * (n * k + D) ^ j) :
    (d : ℝ) ^ exactRankExponent ≤ k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank, OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent

theorem OAI.MatrixMultiplication.AuxiliarySeparation.not_catalytic_rank_bounds_of_lt line 161

Source documentation

Contradiction form for the finite-obstruction argument.

theorem not_catalytic_rank_bounds_of_lt {d k D R : ℕ} (hd : 0 < d)
    (hk : (k : ℝ) < (d : ℝ) ^ exactRankExponent) :
    ¬ (∀ n : ℕ, 1 ≤ n → ∀ j : ℕ, 1 ≤ j → ∀ g : ℕ,
      exactMatrixRank g ≤ n ^ j →
      exactMatrixRank (d ^ j * g) ≤ R * (n * k + D) ^ j) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent, OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank

theorem OAI.MatrixMultiplication.AuxiliarySeparation.catalytic_power_comparison line 172

Source documentation

Iteration and absorption of a fixed catalyst require no cancellation of the tensor factor s. Monotonicity is explicit so the lemma applies to the restriction order on a tensor semiring, where additive cancellation fails.

theorem catalytic_power_comparison {S : Type*} [CommSemiring S] [Preorder S]
    (hadd : ∀ {a b c e : S}, a ≤ b → c ≤ e → a + c ≤ b + e)
    (hmul : ∀ {a b c e : S}, a ≤ b → c ≤ e → a * c ≤ b * e)
    (hzero : ∀ a : S, 0 ≤ a)
    (D t s : S) (k C : ℕ)
    (hcat : D + t * s ≤ D + (k : S) * s)
    (hD : D ≤ (C : S) * s) (n j : ℕ) :
    (n : S) ^ j * t ^ j * s ≤ ((n * k + C : ℕ) : S) ^ j * s := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.catalytic_semiring_obstruction line 217

Source documentation

A rank-compatible ordered tensor semiring converts a single finite catalytic inequality into the actual exact-rank obstruction. The hypotheses name the required tensor interpretation and scalar rank domination explicitly; no additive rank formula or cancellation property is assumed.

theorem catalytic_semiring_obstruction {S : Type*} [CommSemiring S] [Preorder S]
    (hadd : ∀ {a b c e : S}, a ≤ b → c ≤ e → a + c ≤ b + e)
    (hmul : ∀ {a b c e : S}, a ≤ b → c ≤ e → a * c ≤ b * e)
    (hzero : ∀ a : S, 0 ≤ a)
    (ρ : S → ℕ) (hρmono : Monotone ρ)
    (hρcopies : ∀ (m : ℕ) (s : S), ρ ((m : S) * s) ≤ m * ρ s)
    (M : ℕ → S)
    (hMmul : ∀ a b : ℕ, M (a * b) = M a * M b)
    (hMpow : ∀ a j : ℕ, M (a ^ j) = M a ^ j)
    (hρM : ∀ a : ℕ, ρ (M a) = exactMatrixRank a)
    (hbudget : ∀ n j g : ℕ, exactMatrixRank g ≤ n ^ j → M g ≤ (n : S) ^ j)
    (D s : S) (d k C : ℕ) (hd : 0 < d) (hs : 1 ≤ s)
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank

theorem OAI.MatrixMultiplication.AuxiliarySeparation.tensor_catalytic_obstruction line 253
Source documentation
In the semiring of actual finite complex tensors modulo mutual restriction, a fixed catalyst cannot make k copies dominate multiplication by T_d unless k ≥ d^ν. The nonzero hypothesis is exactly what supplies the scalar restriction s ≥ 1; the catalyst remains fixed throughout.
```
theorem tensor_catalytic_obstruction
    {D s : TensorSemiring.TensorClass} {d k : ℕ}
    (hd : 0 < d) (hs : s ≠ 0)
    (hcat : D + TensorSemiring.matrixClass d * s ≤ D + (k : TensorSemiring.TensorClass) * s) :
    (d : ℝ) ^ exactRankExponent ≤ k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass, OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.matrixClass, OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent
theorem OAI.MatrixMultiplication.AuxiliarySeparation.tensor_catalytic_obstruction_of_scalar_gain line 295
Source documentation
The stronger comparison produced by a finite separation certificate has the same consequence. Its positive scalar summand is only needed earlier to rule out s = 0; that nonzero fact is explicit here.
```
theorem tensor_catalytic_obstruction_of_scalar_gain
    {D s : TensorSemiring.TensorClass} {d k m : ℕ}
    (hd : 0 < d) (hs : s ≠ 0)
    (hcat : D + (m : TensorSemiring.TensorClass) + TensorSemiring.matrixClass d * s ≤
      D + (k : TensorSemiring.TensorClass) * s) :
    (d : ℝ) ^ exactRankExponent ≤ k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass, OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.matrixClass, OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent
theorem OAI.MatrixMultiplication.AuxiliarySeparation.not_tensor_add_positive_nat_le_self line 311
Source documentation
A finite tensor cannot absorb a positive scalar direct summand. Iterating such an absorption would place arbitrarily large scalar tensors below one fixed finite-rank tensor. This uses rank monotonicity, not rank additivity.
```
theorem not_tensor_add_positive_nat_le_self (D : TensorSemiring.TensorClass)
    {m : ℕ} (hm : 0 < m) : ¬ D + (m : TensorSemiring.TensorClass) ≤ D := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass
theorem OAI.MatrixMultiplication.AuxiliarySeparation.tensor_catalytic_obstruction_of_positive_scalar_gain line 342
Source documentation
The exact finite-obstruction comparison from Appendix A.1 forces k ≥ d^ν. Both tensors are fixed, m is a positive scalar gain, and the ordinary tensor rank and restriction order are the actual ones.
```
theorem tensor_catalytic_obstruction_of_positive_scalar_gain
    {D s : TensorSemiring.TensorClass} {d k m : ℕ}
    (hd : 0 < d) (hm : 0 < m)
    (hcat : D + (m : TensorSemiring.TensorClass) + TensorSemiring.matrixClass d * s ≤
      D + (k : TensorSemiring.TensorClass) * s) :
    (d : ℝ) ^ exactRankExponent ≤ k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass, OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.matrixClass, OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent
theorem OAI.MatrixMultiplication.AuxiliarySeparation.no_tensor_catalytic_gain line 357
Source documentation
Contradiction interface for the finite inconsistency certificate in the construction of an additive monotone state.
```
theorem no_tensor_catalytic_gain {d k : ℕ} (hd : 0 < d)
    (hk : (k : ℝ) < (d : ℝ) ^ exactRankExponent) :
    ¬ ∃ (D s : TensorSemiring.TensorClass) (m : ℕ), 0 < m ∧
      D + (m : TensorSemiring.TensorClass) + TensorSemiring.matrixClass d * s ≤
        D + (k : TensorSemiring.TensorClass) * s := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent, OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass, OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.matrixClass