clopen.solutions
Submission v1

MI-04: universal positive-block norm implies essentially Hermitian

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

George Stepaniants

Complete Lean verification of the full original MI-04 necessity implication. All21 exports passed actual canonical Linux default-kernel, Comparator, axiom and control checks at the immutable proof revision.

Claims

LEAN VERIFIED OP-00099 — A universal block-norm characterization of essentially Hermitian matrices
Full resolution · statement matched the canonical formalisation

Files and sources

Paper
OpenProblemsInNLA @ e375a6f, MI-04/lean/ ↗
Lean bundle
submissions/bundles/openproblemsinnla-mi-04-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:03:38.531306

Declarations audited

DeclarationKindAxiomsUnused hypothesesCanonical
NLA.MI04.universal_positive_block_essentially_hermitian theorem · Prop propext, Classical.choice, Quot.sound none matched
RegistryProblems.Problem_OP_00099 definition propext, Classical.choice, Quot.sound none no canonical statement

NLA.MI04.universal_positive_block_essentially_hermitian

∀ {n : Nat}, instLENat.le 1 n → ∀ (X : NLA.MI04.Square n), (∀ (A B : NLA.MI04.Square n), Matrix.IsHermitian A → Matrix.IsHermitian B → (Matrix.fromBlocks A X (Matrix.conjTranspose X) B).PosSemidef → Real.instLE.le (NLA.MI04.spectralNorm (Matrix.fromBlocks A X (Matrix.conjTranspose X) B)) (NLA.MI04.spectralNorm (instHAdd.hAdd A B))) → Exists fun K => And (Matrix.IsHermitian K) (Exists fun α => Exists fun β => Eq X (instHAdd.hAdd (instHSMul.hSMul α K) (instHSMul.hSMul β 1)))

RegistryProblems.Problem_OP_00099

Prop

Build log

this warning:
  [apply] _hn

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: NLA/MI04/Geometry.lean:78:10: This simp argument is unused:
  Complex.star_def

Hint: Omit it from the simp argument list.
  [apply] simp [Complex.mul_im]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/MI04/Geometry.lean:100:44: This simp argument is unused:
  map_smul

Hint: Omit it from the simp argument list.
  [apply] simp [matrixCoefficient, u, v, map_add, diagonal_coordinateUnit, inner_add_left, inner_add_right,
    inner_sub_left, inner_smul_left, inner_smul_right, inner_coordinateUnit_left, coordinateUnit_apply,
    Complex.star_def, hij, Ne.symm hij, hik, Ne.symm hik, hjk, Ne.symm hjk]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/MI04/Geometry.lean:102:55: This simp argument is unused:
  Complex.star_def

Hint: Omit it from the simp argument list.
  [apply] simp [matrixCoefficient, u, v, map_add, map_smul, diagonal_coordinateUnit, inner_add_left, inner_add_right,
    inner_sub_left, inner_smul_left, inner_smul_right, inner_coordinateUnit_left, coordinateUnit_apply, hij,
    Ne.symm hij, hik, Ne.symm hik, hjk, Ne.symm hjk]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/MI04/Geometry.lean:91:64: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: NLA/MI04/Geometry.lean:78:44: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: NLA/MI04/Geometry.lean:97:60: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: NLA/MI04/Geometry.lean:103:60: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: NLA/MI04/Geometry.lean:91:64: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
info: NLA/MI04/Geometry.lean:108:0: 'NLA.MI04.diagonal_pair_collinearity' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3756/3760] Built NLA.MI04.Diagonalization (12s)
warning: NLA/MI04/Diagonalization.lean:38:4: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
warning: NLA/MI04/Diagonalization.lean:47:4: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
warning: NLA/MI04/Diagonalization.lean:84:17: `ContinuousLinearMap.add_apply` has been deprecated: Use `add_apply` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.add_apply` to `add_apply x`).
warning: NLA/MI04/Diagonalization.lean:84:48: `ContinuousLinearMap.smul_apply` has been deprecated: Use `smul_apply` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.smul_apply` to `smul_apply x`).
warning: NLA/MI04/Diagonalization.lean:101:4: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
warning: NLA/MI04/Diagonalization.lean:95:48: Variable name `hn` 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] _hn

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: NLA/MI04/Diagonalization.lean:126:0: 'NLA.MI04.normal_unitary_diagonalization' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3757/3760] Built NLA.MI04.Conclusion (4.8s)
warning: NLA/MI04/Conclusion.lean:51:26: This simp argument is unused:
  Matrix.diagonal_apply

Hint: Omit it from the simp argument list.
  [apply] simp [realDiagonal, Matrix.one_apply, hij]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/MI04/Conclusion.lean:51:49: This simp argument is unused:
  Matrix.one_apply

Hint: Omit it from the simp argument list.
  [apply] simp [realDiagonal, Matrix.diagonal_apply, hij]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: NLA/MI04/Conclusion.lean:72:0: 'NLA.MI04.pair_symmetry_essentially_hermitian' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MI04/Conclusion.lean:74:0: 'NLA.MI04.universal_positive_block_essentially_hermitian' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3758/3760] Built Solution (4.3s)
info: Solution.lean:17:0: 'NLA.MI04.topValue_maximum' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:19:0: 'NLA.MI04.positive_quadratic_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:21:0: 'NLA.MI04.positive_norm_eq_top' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:23:0: 'NLA.MI04.shifted_topValue' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:25:0: 'NLA.MI04.scalar_order_iff_top' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:27:0: 'NLA.MI04.unitary_topValue' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:29:0: 'NLA.MI04.simple_peak_sandwich' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:31:0: 'NLA.MI04.simple_peak_second_order' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:33:0: 'NLA.MI04.pencil_isHermitian' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:35:0: 'NLA.MI04.universal_to_extreme_symmetry' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:37:0: 'NLA.MI04.extreme_symmetry_scaled_unitary' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:39:0: 'NLA.MI04.weighted_magnitude_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:41:0: 'NLA.MI04.offDiagonal_magnitude_symmetry' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:43:0: 'NLA.MI04.orthonormal_pair_symmetry' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:45:0: 'NLA.MI04.pair_symmetry_normal' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:47:0: 'NLA.MI04.normal_unitary_diagonalization' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:49:0: 'NLA.MI04.pair_symmetry_unitary' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:51:0: 'NLA.MI04.diagonal_pair_collinearity' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:53:0: 'NLA.MI04.collinear_values_affine' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:55:0: 'NLA.MI04.pair_symmetry_essentially_hermitian' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:57:0: 'NLA.MI04.universal_positive_block_essentially_hermitian' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3759/3760] Built RegistryRecord (4.6s)
Build completed successfully (3760 jobs).