Multiplicative states obtained by normalizing translates of additive states.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate {S : Type u_1} [CommSemiring S] (z : S) (f : S → ℝ) : S → ℝ

Translate a state by multiplication, then normalize at the unit.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate z f x = f (z * x) / f z

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate_continuousOn {S : Type u_1} [CommSemiring S] {K : Set (S → ℝ)} (z : S) (hz : ∀ f ∈ K, f z ≠ 0) : Continuous fun (f : ↑K) => normalizedTranslate z ↑f

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.frozenConstraint {S : Type u_1} [CommSemiring S] (z : S) (c : ℝ) : Set (S → ℝ)

Functions satisfying a fixed multiplicative scaling relation at one semiring element.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.frozenConstraint z c = {f : S → ℝ | ∀ (x : S), f (z * x) = c * f x}

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.frozenSlice {S : Type u_1} [CommSemiring S] (C : Set (S → ℝ)) (z : S) (c : ℝ) : Set (S → ℝ)

Intersect a family of candidate states with one multiplicative scaling constraint.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.frozenSlice C z c = C ∩ MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.frozenConstraint z c

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.frozenConstraint_isClosed {S : Type u_1} [CommSemiring S] (z : S) (c : ℝ) : IsClosed (frozenConstraint z c)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.frozenSlice_isClosed {S : Type u_1} [CommSemiring S] {C : Set (S → ℝ)} (hC : IsClosed C) (z : S) (c : ℝ) : IsClosed (frozenSlice C z c)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.frozenSlice_isCompact {S : Type u_1} [CommSemiring S] {C : Set (S → ℝ)} (hC : IsCompact C) (z : S) (c : ℝ) : IsCompact (frozenSlice C z c)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.frozenConstraint_convex {S : Type u_1} [CommSemiring S] (z : S) (c : ℝ) : Convex ℝ (frozenConstraint z c)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.frozenSlice_convex {S : Type u_1} [CommSemiring S] {C : Set (S → ℝ)} (hC : Convex ℝ C) (z : S) (c : ℝ) : Convex ℝ (frozenSlice C z c)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate_mem_frozenConstraint {S : Type u_1} [CommSemiring S] {z w : S} {c : ℝ} {f : S → ℝ} (hf : f ∈ frozenConstraint z c) : normalizedTranslate w f ∈ frozenConstraint z c

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.frozenSlice_mapsTo_normalizedTranslate {S : Type u_1} [CommSemiring S] {C : Set (S → ℝ)} {z w : S} {c : ℝ} (hC : Set.MapsTo (normalizedTranslate w) C C) : Set.MapsTo (normalizedTranslate w) (frozenSlice C z c) (frozenSlice C z c)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.frozenConstraint_value {S : Type u_1} [CommSemiring S] {z : S} {c : ℝ} {f : S → ℝ} (hf : f ∈ frozenConstraint z c) (hf1 : f 1 = 1) : f z = c

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.frozenConstraint_normalizedTranslate_eq {S : Type u_1} [CommSemiring S] {z : S} {c : ℝ} {f : S → ℝ} (hf : f ∈ frozenConstraint z c) (hf1 : f 1 = 1) (hfz : f z ≠ 0) : normalizedTranslate z f = f

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate_eq_mem_frozenConstraint {S : Type u_1} [CommSemiring S] {z : S} {f : S → ℝ} (hfz : f z ≠ 0) (hf : normalizedTranslate z f = f) : f ∈ frozenConstraint z (f z)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate_eq_nonzero {S : Type u_1} [CommSemiring S] {z : S} {f : S → ℝ} (hf1 : f 1 = 1) (hf : normalizedTranslate z f = f) : f z ≠ 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate_eq_mem_frozenConstraint_of_normalized {S : Type u_1} [CommSemiring S] {z : S} {f : S → ℝ} (hf1 : f 1 = 1) (hf : normalizedTranslate z f = f) : f ∈ frozenConstraint z (f z)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalizedTranslate_eq_mem_frozenSlice {S : Type u_1} [CommSemiring S] {C : Set (S → ℝ)} {z : S} {f : S → ℝ} (hfC : f ∈ C) (hf1 : f 1 = 1) (hf : normalizedTranslate z f = f) : f ∈ frozenSlice C z (f z)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_finite_multiplicative_slice {S : Type u_1} [CommSemiring S] {K : Set (S → ℝ)} (hKcompact : IsCompact K) (hKconvex : Convex ℝ K) (hKne : K.Nonempty) (hKnorm : ∀ f ∈ K, f 1 = 1) (hKnonzero : ∀ f ∈ K, ∀ (z : S), z ≠ 0 → f z ≠ 0) (hKmap : ∀ (z : S), z ≠ 0 → Set.MapsTo (normalizedTranslate z) K K) (t : Finset { z : S // z ≠ 0 }) : ∃ C ⊆ K, C.Nonempty ∧ IsCompact C ∧ Convex ℝ C ∧ (∀ (z : S), z ≠ 0 → Set.MapsTo (normalizedTranslate z) C C) ∧ ∀ f ∈ C, ∀ z ∈ t, ∀ (x : S), f (↑z * x) = f ↑z * f x

Every finite collection of multiplication identities holds throughout a nonempty compact convex subset that remains invariant under all translates.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_multiplicative_of_invariant_states {S : Type u_1} [CommSemiring S] {K : Set (S → ℝ)} (hKcompact : IsCompact K) (hKconvex : Convex ℝ K) (hKne : K.Nonempty) (hKnorm : ∀ f ∈ K, f 1 = 1) (hKzero : ∀ f ∈ K, f 0 = 0) (hKnonzero : ∀ f ∈ K, ∀ (z : S), z ≠ 0 → f z ≠ 0) (hKmap : ∀ (z : S), z ≠ 0 → Set.MapsTo (normalizedTranslate z) K K) : ∃ f ∈ K, ∀ (x y : S), f (x * y) = f x * f y

A compact convex normalized state space invariant under multiplication translates contains a multiplicative state. Frozen eigenvalue slices preserve convexity at each finite fixed-point step.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalizedStates_exists_multiplicative {S : Type u_1} [CommSemiring S] [Preorder S] (R : S → ℕ) (d : S) (k : ℝ) (hunit : ∀ (z : S), z ≠ 0 → 1 ≤ z) (hmulmono : ∀ (z x y : S), x ≤ y → z * x ≤ z * y) (hdom : ∀ (z x : S), z * x ≤ ↑(R x) * z) (hne : (normalizedStates (fun (x : S) => ↑(R x)) d k).Nonempty) : ∃ f ∈ normalizedStates (fun (x : S) => ↑(R x)) d k, ∀ (x y : S), f (x * y) = f x * f y

Appendix A.2 for a ranked restriction semiring: once the preliminary normalized state set is nonempty, it contains a multiplicative state.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_monotone_semiringHom_of_normalizedStates {S : Type u_1} [CommSemiring S] [Preorder S] (R : S → ℕ) (d : S) (k : ℝ) (hunit : ∀ (z : S), z ≠ 0 → 1 ≤ z) (hmulmono : ∀ (z x y : S), x ≤ y → z * x ≤ z * y) (hdom : ∀ (z x : S), z * x ≤ ↑(R x) * z) (hne : (normalizedStates (fun (x : S) => ↑(R x)) d k).Nonempty) : ∃ (χ : S →+* ℝ), Monotone ⇑χ ∧ (∀ (x : S), 0 ≤ χ x ∧ χ x ≤ ↑(R x)) ∧ k ≤ χ d

The multiplicative state as a normalized monotone semiring homomorphism, with the original rank bounds and detector inequality preserved.