MF-05: local two-family Holder continuity of the joint spectral radius
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Complete Lean verification of the original local two-family Holder assertion for arbitrary nonempty compact complex matrix families. All 14 exact contracts passed local compilation, two independent final source reviews, and actual canonical non-root Linux verification at the immutable proof revision.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, MF-05/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-mf-05-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:06:20.977471
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.MF05.canonical_local_holder | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00090 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.MF05.canonical_local_holder
∀ {d : Nat}, instLENat.le 1 d → ∀ (M0 : Set (NLA.MF07.Square d)), IsCompact M0 → M0.Nonempty → Exists fun r => And (Real.instLT.lt 0 r) (Exists fun C => And (Real.instLT.lt 0 C) (∀ (M N : Set (NLA.MF07.Square d)), IsCompact M → M.Nonempty → IsCompact N → N.Nonempty → Real.instLT.lt (NLA.MF05.canonicalHausdorff M M0) r → Real.instLT.lt (NLA.MF05.canonicalHausdorff N M0) r → Real.instLE.le (abs (instHSub.hSub (NLA.MF07.jointSpectralRadius M) (NLA.MF07.jointSpectralRadius N))) (instHMul.hMul C ((NLA.MF05.canonicalHausdorff M N).rpow (instHDiv.hDiv 1 d.cast)))))
RegistryProblems.Problem_OP_00090
Prop
Build log
ℹ [3702/3722] Built NLA.MF05.HolderScale (14s) info: NLA/MF05/HolderScale.lean:72:0: 'NLA.MF05.holder_scale_identity' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3703/3722] Built NLA.MF05.GeneralEnvelope (16s) info: NLA/MF05/GeneralEnvelope.lean:78:0: 'NLA.MF05.jointSpectralRadius_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF05/GeneralEnvelope.lean:80:0: 'NLA.MF05.general_exponential_envelope' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3704/3722] Built NLA.MF05.Hausdorff (20s) info: NLA/MF05/Hausdorff.lean:162:0: 'NLA.MF05.spectral_hausdorff_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3705/3722] Built NLA.MF07.SingularCoordinates (14s) warning: NLA/MF07/SingularCoordinates.lean:43:55: This simp argument is unused: Matrix.diagonal_apply Hint: Omit it from the simp argument list. [apply] simp [diagonalWeights, Matrix.conjTranspose_apply, hij, Ne.symm hij] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: NLA/MF07/SingularCoordinates.lean:109:29: This simp argument is unused: Matrix.diagonal_apply Hint: Omit it from the simp argument list. [apply] simp [diagonalWeights, hij] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` info: NLA/MF07/SingularCoordinates.lean:143:0: 'NLA.MF07.ordered_positive_gram_coordinates' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF07/SingularCoordinates.lean:145:0: 'NLA.MF07.exists_singular_coordinates' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3706/3722] Built NLA.MF05.RootLimit (13s) info: NLA/MF05/RootLimit.lean:87:0: 'NLA.MF05.general_root_limit_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF05/RootLimit.lean:89:0: 'NLA.MF05.exponential_bound_controls_radius' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3707/3722] Built NLA.MF07.RoundedNorm (16s) warning: NLA/MF07/RoundedNorm.lean:43:44: 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` info: NLA/MF07/RoundedNorm.lean:143:0: 'NLA.MF07.rounded_extremal_norm' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3708/3722] Built NLA.MF05.LocalBall (17s) info: NLA/MF05/LocalBall.lean:46:0: 'NLA.MF05.local_common_norm_ball' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3709/3722] Built NLA.MF05.IdentityAdjoin (16s) info: NLA/MF05/IdentityAdjoin.lean:144:0: 'NLA.MF05.identity_adjoin_word_compression' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF05/IdentityAdjoin.lean:146:0: 'NLA.MF05.scalar_identity_adjoin_radius' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3710/3722] Built NLA.MF05.Scaling (16s) info: NLA/MF05/Scaling.lean:114:0: 'NLA.MF05.positive_scaling_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3711/3722] Built NLA.MF07.BlockComparison (8.3s) warning: NLA/MF07/BlockComparison.lean:70:8: This simp argument is unused: Matrix.one_apply Hint: Omit it from the simp argument list. [apply] simp [hne] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` info: NLA/MF07/BlockComparison.lean:141:0: 'NLA.MF07.spectralNorm_le_card_mul_entry_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF07/BlockComparison.lean:143:0: 'NLA.MF07.damped_lower_product_bound' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3712/3722] Built NLA.MF07.CappedWeights (8.1s) warning: NLA/MF07/CappedWeights.lean:31:37: Try `simp at hij` instead of `simpa using hij` Note: This linter can be disabled with `set_option linter.unnecessarySimpa false` warning: NLA/MF07/CappedWeights.lean:123:90: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: NLA/MF07/CappedWeights.lean:123:90: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` info: NLA/MF07/CappedWeights.lean:158:0: 'NLA.MF07.exists_capped_weights' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3713/3722] Built NLA.MF07.Similarity (7.8s) warning: NLA/MF07/Similarity.lean:42:6: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: NLA/MF07/Similarity.lean:42:6: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` info: NLA/MF07/Similarity.lean:142:0: 'NLA.MF07.rotatedGenerator_product' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF07/Similarity.lean:144:0: 'NLA.MF07.spectralNorm_unrotate_le' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3714/3722] Built NLA.MF07.QuantitativeComparison (7.9s) info: NLA/MF07/QuantitativeComparison.lean:160:0: 'NLA.MF07.quantitative_comparison' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3715/3722] Built NLA.MF05.GeneralComparison (8.2s) info: NLA/MF05/GeneralComparison.lean:112:0: 'NLA.MF05.general_quantitative_comparison' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3716/3722] Built NLA.MF05.ComparisonNorm (7.0s) info: NLA/MF05/ComparisonNorm.lean:61:0: 'NLA.MF05.controlled_comparison_norm' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3717/3722] Built NLA.MF05.RadiusTransfer (7.4s) info: NLA/MF05/RadiusTransfer.lean:74:0: 'NLA.MF05.hausdorff_radius_transfer' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3718/3722] Built NLA.MF05.UniformHolder (7.3s) info: NLA/MF05/UniformHolder.lean:108:0: 'NLA.MF05.uniform_holder_estimate' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3719/3722] Built NLA.MF05.Final (7.5s) info: NLA/MF05/Final.lean:47:0: 'NLA.MF05.canonical_local_holder' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3720/3722] Built Solution (6.5s) info: Solution.lean:16:0: 'NLA.MF05.half_radius_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:18:0: 'NLA.MF05.spectral_hausdorff_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:20:0: 'NLA.MF05.general_exponential_envelope' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:22:0: 'NLA.MF05.general_root_limit_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:24:0: 'NLA.MF05.positive_scaling_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:26:0: 'NLA.MF05.exponential_bound_controls_radius' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:28:0: 'NLA.MF05.scalar_identity_adjoin_radius' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:30:0: 'NLA.MF05.general_quantitative_comparison' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:32:0: 'NLA.MF05.controlled_comparison_norm' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:34:0: 'NLA.MF05.hausdorff_radius_transfer' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:36:0: 'NLA.MF05.holder_scale_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:38:0: 'NLA.MF05.uniform_holder_estimate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:40:0: 'NLA.MF05.local_common_norm_ball' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:42:0: 'NLA.MF05.canonical_local_holder' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3721/3722] Built RegistryRecord (6.8s) Build completed successfully (3722 jobs).