Existence.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Detecting characters for complex matrix multiplication

This proves Lemma 3.1, including Appendix A. Finite inconsistency would produce a positive scalar-gain catalyst, ruled out by the exact-rank exponent. A compact normalized state space then yields a multiplicative state, which transfers to the concrete coefficient-level character interface.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_detecting_character line 25
Source documentation
Lemma 3.1: normalized, additive, multiplicative, restriction-monotone characters detect every integer strictly below the exact-rank growth value.
```
theorem exists_detecting_character {d k : ℕ} (hd : 2 ≤ d)
    (hk : (k : ℝ) < (d : ℝ) ^ exactRankExponent) :
    ∃ χ : Character, (k : ℝ) ≤ χ.value (Tensor.matrixMultiplication d d d) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent, OAI.MatrixMultiplication.AuxiliarySeparation.Character