Detecting characters for matrix multiplication over K

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 MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_detecting_character {K : Type} [Field K] {d k : ℕ} (hd : 2 ≤ d) (hk : ↑k < ↑d ^ exactRankExponent K) : ∃ (χ : Character K), ↑k ≤ χ.value (Foundation.Tensor.matMul K d d d)

Lemma 3.1: normalized, additive, multiplicative, restriction-monotone characters detect every integer strictly below the exact-rank growth value.