MF-07: uniform polynomial product bound at joint spectral radius one

Recorded by the registry's curators from GitHub; the authors did not submit it here.

George Stepaniants

Complete original MF-07 result for arbitrary nonempty compact complex matrix families at joint spectral radius one, all positive dimensions and every switching word. All 18 exports passed actual canonical Linux default-kernel, Comparator, axiom and control checks at the immutable proof revision.

Claims

LEAN VERIFIED OP-00092 — Uniform polynomial bounds for products at joint spectral radius one

Full resolution · statement matched the canonical formalisation

Files and sources

Paper: OpenProblemsInNLA @ e375a6f, MF-07/lean/ ↗
Lean bundle: submissions/bundles/openproblemsinnla-mf-07-lean.tar.gz
Toolchain: leanprover/lean4:v4.33.1
Posted on GitHub: 17 September 2026

Verification PASSED

Attempt: 1
Toolchain: leanprover/lean4:v4.33.1
Auditor: v1 · modal
lake build: succeeded
Kernel replay: succeeded
Duration: 0:02:56.255440

Declarations audited

Declaration	Kind	Axioms	Unused hypotheses	Canonical
NLA.MF07.canonical_uniform_bound	theorem · Prop	propext, Classical.choice, Quot.sound	none	matched
RegistryProblems.Problem_OP_00092	definition	propext, Classical.choice, Quot.sound	none	no canonical statement

NLA.MF07.canonical_uniform_bound

∀ (d : Nat), instLENat.le 1 d → Exists fun Θ => And (Real.instLT.lt 0 Θ) (∀ (M : Set (NLA.MF07.Square d)), IsCompact M → M.Nonempty → Eq (NLA.MF07.jointSpectralRadius M) 1 → ∀ (n : Nat), instLENat.le 1 n → ∀ (A : Fin n → NLA.MF07.Square d), (∀ (i : Fin n), Set.instMembership.mem M (A i)) → Real.instLE.le (NLA.MF07.spectralNorm (NLA.MF07.finiteProduct A)) (instHMul.hMul Θ (instHPow.hPow (instHMul.hMul (NLA.MF07.familyNorm M) n.cast) (instHSub.hSub d 1))))

RegistryProblems.Problem_OP_00092

Prop

Build log

.MF07.matrix_product_semantics' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:20:0: NLA.MF07.diagonal_inverse {d : ℕ} (σ : Fin d → ℝ) (hσ : ∀ (i : Fin d), σ i ≠ 0) :
  NLA.MF07.diagonalWeights σ * NLA.MF07.inverseDiagonalWeights σ = 1 ∧
    NLA.MF07.inverseDiagonalWeights σ * NLA.MF07.diagonalWeights σ = 1
info: Solution.lean:21:0: 'NLA.MF07.diagonal_inverse' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:24:0: NLA.MF07.family_norm_maximum {d : ℕ} (hd : 1 ≤ d) (M : Set (NLA.MF07.Square d)) (hM : IsCompact M) (hne : M.Nonempty) :
  0 ≤ NLA.MF07.familyNorm M ∧
    (∃ A ∈ M, NLA.MF07.spectralNorm A = NLA.MF07.familyNorm M) ∧
      ∀ A ∈ M, NLA.MF07.spectralNorm A ≤ NLA.MF07.familyNorm M
info: Solution.lean:25:0: 'NLA.MF07.family_norm_maximum' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:28:0: NLA.MF07.family_growth_maximum {d : ℕ} (hd : 1 ≤ d) (M : Set (NLA.MF07.Square d)) (hM : IsCompact M) (hne : M.Nonempty)
  (n : ℕ) :
  0 ≤ NLA.MF07.familyGrowth M n ∧
    NLA.MF07.familyGrowth M n ≤ NLA.MF07.familyNorm M ^ n ∧
      (∃ w,
          w.length = n ∧
            NLA.MF07.WordIn M w ∧ NLA.MF07.spectralNorm (NLA.MF07.matrixProduct w) = NLA.MF07.familyGrowth M n) ∧
        ∀ (w : List (NLA.MF07.Square d)),
          w.length = n →
            NLA.MF07.WordIn M w → NLA.MF07.spectralNorm (NLA.MF07.matrixProduct w) ≤ NLA.MF07.familyGrowth M n
info: Solution.lean:29:0: 'NLA.MF07.family_growth_maximum' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:32:0: NLA.MF07.family_growth_submultiplicative {d : ℕ} (hd : 1 ≤ d) (M : Set (NLA.MF07.Square d)) (hM : IsCompact M)
  (hne : M.Nonempty) (m n : ℕ) : NLA.MF07.familyGrowth M (m + n) ≤ NLA.MF07.familyGrowth M m * NLA.MF07.familyGrowth M n
info: Solution.lean:33:0: 'NLA.MF07.family_growth_submultiplicative' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:36:0: NLA.MF07.radius_one_semantics {d : ℕ} (hd : 1 ≤ d) (M : Set (NLA.MF07.Square d)) (hM : IsCompact M) (hne : M.Nonempty) :
  (NLA.MF07.jointSpectralRadius M = 1 ↔ Filter.Tendsto (NLA.MF07.rootGrowth M) Filter.atTop (nhds 1)) ∧
    (NLA.MF07.jointSpectralRadius M = 1 → 1 ≤ NLA.MF07.familyNorm M)
info: Solution.lean:37:0: 'NLA.MF07.radius_one_semantics' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:40:0: NLA.MF07.identity_family_semantics {d : ℕ} (hd : 1 ≤ d) :
  NLA.MF07.familyNorm {1} = 1 ∧ (∀ (n : ℕ), NLA.MF07.familyGrowth {1} n = 1) ∧ NLA.MF07.jointSpectralRadius {1} = 1
info: Solution.lean:41:0: 'NLA.MF07.identity_family_semantics' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:44:0: NLA.MF07.approximate_extremal_norm {d : ℕ} (hd : 1 ≤ d) (M : Set (NLA.MF07.Square d)) (hM : IsCompact M)
  (hne : M.Nonempty) (hr : NLA.MF07.jointSpectralRadius M = 1) (a : ℝ) (ha : 1 < a) :
  ∃ v c,
    1 ≤ c ∧
      NLA.MF07.IsComplexNorm v ∧
        (∀ (x : NLA.MF07.EuclideanVector d), ‖x‖ ≤ v x ∧ v x ≤ c * ‖x‖) ∧
          ∀ A ∈ M, ∀ (x : NLA.MF07.EuclideanVector d), v (NLA.MF07.applyMatrix A x) ≤ a * v x
info: Solution.lean:45:0: 'NLA.MF07.approximate_extremal_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:48:0: NLA.MF07.rounded_extremal_norm {d : ℕ} (hd : 1 ≤ d) (M : Set (NLA.MF07.Square d)) (hM : IsCompact M) (hne : M.Nonempty)
  (hr : NLA.MF07.jointSpectralRadius M = 1) (a : ℝ) (ha : 1 < a) :
  ∃ Q σ w,
    NLA.MF07.IsUnitary Q ∧
      Antitone σ ∧
        (∀ (i : Fin d), 0 < σ i) ∧
          NLA.MF07.IsComplexNorm w ∧
            (∀ (x : NLA.MF07.EuclideanVector d), ‖x‖ ≤ w x ∧ w x ≤ ↑d * ‖x‖) ∧
              (∀ A ∈ M,
                  ∀ (x : NLA.MF07.EuclideanVector d),
                    w (NLA.MF07.applyMatrix (NLA.MF07.rotatedGenerator Q σ A) x) ≤ a * w x) ∧
                ∀ A ∈ M, ∀ (i j : Fin d), ‖NLA.MF07.rotatedGenerator Q σ A i j‖ ≤ NLA.MF07.familyNorm M * σ j / σ i
info: Solution.lean:49:0: 'NLA.MF07.rounded_extremal_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:52:0: NLA.MF07.triangular_damping {d : ℕ} (h : Fin d → ℝ) (hh : Antitone h) (hpos : ∀ (i : Fin d), 0 < h i)
  (X : NLA.MF07.Square d) (hX : NLA.MF07.LowerForWeights h X) :
  NLA.MF07.spectralNorm (NLA.MF07.diagonalDamping h X) ≤ NLA.MF07.spectralNorm X
info: Solution.lean:53:0: 'NLA.MF07.triangular_damping' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:56:0: NLA.MF07.interspersed_product_bound {d : ℕ} (M : Set (NLA.MF07.Square d)) (C E : NLA.MF07.Square d → NLA.MF07.Square d)
  (K u v : ℝ) (hK : 1 ≤ K) (hu : 0 ≤ u) (hv : 0 ≤ v)
  (hC :
    ∀ (z : List (NLA.MF07.Square d)),
      NLA.MF07.WordIn M z → NLA.MF07.spectralNorm (NLA.MF07.matrixProduct (List.map C z)) ≤ K * u ^ z.length)
  (hE : ∀ A ∈ M, NLA.MF07.spectralNorm (E A) ≤ v) (z : List (NLA.MF07.Square d)) (hz : NLA.MF07.WordIn M z) :
  NLA.MF07.spectralNorm (NLA.MF07.matrixProduct (List.map (fun A => C A + E A) z)) ≤ K * (u + K * v) ^ z.length
info: Solution.lean:57:0: 'NLA.MF07.interspersed_product_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:60:0: NLA.MF07.quantitative_comparison {d : ℕ} (hd : 1 ≤ d) (M : Set (NLA.MF07.Square d)) (hM : IsCompact M)
  (hne : M.Nonempty) (hr : NLA.MF07.jointSpectralRadius M = 1) (s : ℝ) (hs : 1 ≤ s) (n : ℕ) :
  NLA.MF07.familyGrowth M n ≤ ↑d * s ^ (d - 1) * (1 + 2 * ↑d ^ 2 * NLA.MF07.familyNorm M / s) ^ n
info: Solution.lean:61:0: 'NLA.MF07.quantitative_comparison' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:64:0: NLA.MF07.scalar_family_growth (M : Set (NLA.MF07.Square 1)) (hM : IsCompact M) (hne : M.Nonempty) :
  (∀ (n : ℕ), NLA.MF07.familyGrowth M n = NLA.MF07.familyNorm M ^ n) ∧
    NLA.MF07.jointSpectralRadius M = NLA.MF07.familyNorm M
info: Solution.lean:65:0: 'NLA.MF07.scalar_family_growth' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:68:0: NLA.MF07.exp_one_bound : Real.exp 1 ≤ 3
info: Solution.lean:69:0: 'NLA.MF07.exp_one_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:72:0: NLA.MF07.comparison_threshold_bound (d n : ℕ) (hd : 2 ≤ d) (hn : 1 ≤ n) (L : ℝ) (hL : 1 ≤ L) :
  1 ≤ NLA.MF07.comparisonThreshold d n L ∧
    ↑d * NLA.MF07.comparisonThreshold d n L ^ (d - 1) * (1 + 2 * ↑d ^ 2 * L / NLA.MF07.comparisonThreshold d n L) ^ n ≤
      NLA.MF07.growthConstant d * (L * ↑n) ^ (d - 1)
info: Solution.lean:73:0: 'NLA.MF07.comparison_threshold_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:76:0: NLA.MF07.growth_constant_positive (d : ℕ) (hd : 1 ≤ d) : 0 < NLA.MF07.growthConstant d
info: Solution.lean:77:0: 'NLA.MF07.growth_constant_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:80:0: NLA.MF07.radius_one_growth {d : ℕ} (hd : 1 ≤ d) (M : Set (NLA.MF07.Square d)) (hM : IsCompact M) (hne : M.Nonempty)
  (hr : NLA.MF07.jointSpectralRadius M = 1) (n : ℕ) (hn : 1 ≤ n) :
  NLA.MF07.familyGrowth M n ≤ NLA.MF07.growthConstant d * (NLA.MF07.familyNorm M * ↑n) ^ (d - 1)
info: Solution.lean:81:0: 'NLA.MF07.radius_one_growth' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:84:0: NLA.MF07.canonical_uniform_bound (d : ℕ) (hd : 1 ≤ d) :
  ∃ Θ,
    0 < Θ ∧
      ∀ (M : Set (NLA.MF07.Square d)),
        IsCompact M →
          M.Nonempty →
            NLA.MF07.jointSpectralRadius M = 1 →
              ∀ (n : ℕ),
                1 ≤ n →
                  ∀ (A : Fin n → NLA.MF07.Square d),
                    (∀ (i : Fin n), A i ∈ M) →
                      NLA.MF07.spectralNorm (NLA.MF07.finiteProduct A) ≤ Θ * (NLA.MF07.familyNorm M * ↑n) ^ (d - 1)
info: Solution.lean:85:0: 'NLA.MF07.canonical_uniform_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3710/3711] Built RegistryRecord (4.3s)
Build completed successfully (3711 jobs).