MF-06: Pointwise Lipschitz lower bound for the joint spectral radius
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
For every fixed nonempty compact complex matrix family in every positive finite dimension, prove a one-sided linear lower perturbation bound for its joint spectral radius, uniformly over arbitrary nearby nonempty compact families. The proof includes the actual critical product-bounded exterior-power construction.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, MF-06/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-mf-06-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 18 September 2026
Verification PASSED
- Attempt
- 1
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:10:41.365584
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.MF06.canonical_pointwise_lower_lipschitz | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00091 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.MF06.canonical_pointwise_lower_lipschitz
∀ {d : Nat}, instLENat.le 1 d → ∀ (M : Set (NLA.MF07.Square d)), IsCompact M → M.Nonempty → Exists fun r => And (Real.instLT.lt 0 r) (Exists fun C => And (Real.instLT.lt 0 C) (∀ (N : Set (NLA.MF07.Square d)), IsCompact N → N.Nonempty → Real.instLT.lt (NLA.MF05.canonicalHausdorff M N) r → Real.instLE.le (instHSub.hSub (NLA.MF07.jointSpectralRadius M) (instHMul.hMul C (NLA.MF05.canonicalHausdorff M N))) (NLA.MF07.jointSpectralRadius N)))
RegistryProblems.Problem_OP_00091
Prop
Build log
not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hk0 Note: This linter can be disabled with `set_option linter.unusedVariables false` warning: NLA/MF06/CriticalAllocationGap.lean:27:27: Variable name `hkd` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hkd Note: This linter can be disabled with `set_option linter.unusedVariables false` info: NLA/MF06/CriticalAllocationGap.lean:45:0: 'NLA.MF06.critical_allocation_nonresonance' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3830/3841] Built NLA.MF06.PerturbationCone (17s) info: NLA/MF06/PerturbationCone.lean:135:0: 'NLA.MF06.matched_cone_step' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3831/3841] Built NLA.MF06.IrreducibleFlag (7.6s) info: NLA/MF06/IrreducibleFlag.lean:47:0: 'NLA.MF06.irreducible_flag' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3832/3841] Built NLA.MF06.BlockNonresonance (7.0s) info: NLA/MF06/BlockNonresonance.lean:88:0: 'NLA.MF06.block_nonresonance_product_bounded' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3833/3841] Built NLA.MF06.ProductBoundedLower (8.4s) info: NLA/MF06/ProductBoundedLower.lean:92:0: 'NLA.MF06.product_bounded_lower_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3834/3841] Built NLA.MF06.CompoundNonresonance (7.1s) warning: NLA/MF06/CompoundNonresonance.lean:23:57: Variable name `hd` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hd Note: This linter can be disabled with `set_option linter.unusedVariables false` warning: NLA/MF06/CompoundNonresonance.lean:24:25: Variable name `hb` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hb Note: This linter can be disabled with `set_option linter.unusedVariables false` info: NLA/MF06/CompoundNonresonance.lean:43:0: 'NLA.MF06.compound_nonresonance_product_bounded' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3835/3841] Built NLA.MF06.CompoundLowerTransfer (9.6s) info: NLA/MF06/CompoundLowerTransfer.lean:82:0: 'NLA.MF06.lower_lipschitz_of_critical_compound' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3836/3841] Built NLA.MF06.CriticalCompound (6.4s) info: NLA/MF06/CriticalCompound.lean:58:0: 'NLA.MF06.critical_compound_product_bounded' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3837/3841] Built NLA.MF06.NormalizedLower (4.3s) info: NLA/MF06/NormalizedLower.lean:31:0: 'NLA.MF06.normalized_pointwise_lower_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3838/3841] Built NLA.MF06.CanonicalLower (4.6s) info: NLA/MF06/CanonicalLower.lean:59:0: 'NLA.MF06.canonical_pointwise_lower_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3839/3841] Built Solution (4.3s) info: Solution.lean:14:0: 'NLA.MF05.half_radius_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:16:0: 'NLA.MF05.spectral_hausdorff_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:18:0: 'NLA.MF05.general_root_limit_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:20:0: 'NLA.MF05.positive_scaling_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:22:0: 'NLA.MF06.bounded_envelope_norm' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:24:0: 'NLA.MF06.tail_seminorm_limit' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:26:0: 'NLA.MF06.stable_gauge_max_recurrence' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:28:0: 'NLA.MF06.stable_kernel_exponential' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:30:0: 'NLA.MF06.cone_numerical_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:32:0: 'NLA.MF06.product_bounded_lower_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:34:0: 'NLA.MF06.separated_sum_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:36:0: 'NLA.MF06.block_radius_formula' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:38:0: 'NLA.MF06.block_nonresonance_product_bounded' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:40:0: 'NLA.MF06.irreducible_radius_one_product_bounded' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:42:0: 'NLA.MF06.irreducible_flag' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:44:0: 'NLA.MF06.similarity_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:46:0: 'NLA.MF06.compound_dimensions' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:48:0: 'NLA.MF06.compound_coordinate_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:50:0: 'NLA.MF06.compound_algebra' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:52:0: 'NLA.MF06.compound_norm_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:54:0: 'NLA.MF06.compound_local_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:56:0: 'NLA.MF06.tensor_algebra' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:58:0: 'NLA.MF06.tensor_norm_comparison' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:60:0: 'NLA.MF06.allocation_dimensions' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:62:0: 'NLA.MF06.allocation_algebra' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:64:0: 'NLA.MF06.allocation_product_bounded' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:66:0: 'NLA.MF06.compound_allocation_radius' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:68:0: 'NLA.MF06.distinct_allocation_degrees' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:70:0: 'NLA.MF06.allocation_tensor_norm_bridge' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:72:0: 'NLA.MF06.critical_allocation_nonresonance' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:74:0: 'NLA.MF06.compound_nonresonance_product_bounded' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:76:0: 'NLA.MF06.compound_family_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:78:0: 'NLA.MF06.critical_compound_product_bounded' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:80:0: 'NLA.MF06.compound_hausdorff_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:82:0: 'NLA.MF06.positive_hausdorff_scaling' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:84:0: 'NLA.MF06.root_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:86:0: 'NLA.MF06.normalized_pointwise_lower_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:88:0: 'NLA.MF06.canonical_pointwise_lower_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3840/3841] Built RegistryRecord (4.4s) Build completed successfully (3841 jobs).