MI-27: coefficient one in the logarithmic commutator inequality
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Full original coefficient-one bound for every complex positive definite pair of trace sum one in every positive dimension. All twenty frozen contracts pass local Lean and actual source-matched non-root Linux Comparator/default-kernel verification; two independent nonauthor final reviews pass.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, MI-27/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-mi-27-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 19 September 2026
Verification PASSED
- Attempt
- 1
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:08:30.795693
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.MI27.logarithmic_commutator_bound | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00108 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.MI27.logarithmic_commutator_bound
∀ (n : Nat), instLENat.le 1 n → ∀ (A B : NLA.MI27.Mat n), Matrix.PosDef A → Matrix.PosDef B → Eq (Matrix.trace (instHAdd.hAdd A B)) 1 → Real.instLE.le (NLA.MI27.traceNorm (instHSub.hSub (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul B (NLA.MI27.logM (instHAdd.hAdd A B))) (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (NLA.MI27.logM (instHAdd.hAdd A B)) B))) (instHSub.hSub (instHMul.hMul (Real.instNeg.neg (NLA.MI27.trR A)) (Real.log (NLA.MI27.trR A))) (instHMul.hMul (NLA.MI27.trR B) (Real.log (NLA.MI27.trR B))))
RegistryProblems.Problem_OP_00108
Prop
Build log
_entropy_pencil_integral' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3809/3819] Built NLA.MI27.HockeyStickSubstitution (8.6s) warning: NLA/MI27/HockeyStickSubstitution.lean:42:37: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: NLA/MI27/HockeyStickSubstitution.lean:46:62: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: NLA/MI27/HockeyStickSubstitution.lean:42:37: Unused tactic linter: `rfl` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: NLA/MI27/HockeyStickSubstitution.lean:46:62: Unused tactic linter: `rfl` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: NLA/MI27/HockeyStickSubstitution.lean:92:6: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: NLA/MI27/HockeyStickSubstitution.lean:80:4: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: NLA/MI27/HockeyStickSubstitution.lean:88:4: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: NLA/MI27/HockeyStickSubstitution.lean:92:6: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` warning: NLA/MI27/HockeyStickSubstitution.lean:122:6: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: NLA/MI27/HockeyStickSubstitution.lean:109:4: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: NLA/MI27/HockeyStickSubstitution.lean:117:4: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: NLA/MI27/HockeyStickSubstitution.lean:122:6: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` info: NLA/MI27/HockeyStickSubstitution.lean:124:0: 'NLA.MI27.c11_tracePos_smul_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI27/HockeyStickSubstitution.lean:126:0: 'NLA.MI27.c11_pencil_tracePos_zero_unit_interval' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI27/HockeyStickSubstitution.lean:128:0: 'NLA.MI27.c11_pencil_integrand_positive_substitution' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI27/HockeyStickSubstitution.lean:130:0: 'NLA.MI27.c11_pencil_integrand_negative_substitution' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3810/3819] Built NLA.MI27.RelativeEntropyHockeyStick (17s) info: NLA/MI27/RelativeEntropyHockeyStick.lean:106:0: 'NLA.MI27.c11_relative_entropy_hockey_stick_Ioi' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI27/RelativeEntropyHockeyStick.lean:108:0: 'NLA.MI27.relative_entropy_finite_hockey_stick' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3811/3819] Built NLA.MI27.MixturePositivePart (18s) warning: NLA/MI27/MixturePositivePart.lean:38:4: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` info: NLA/MI27/MixturePositivePart.lean:59:0: 'NLA.MI27.c12_E_mixture_forward' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MI27/MixturePositivePart.lean:61:0: 'NLA.MI27.c12_E_mixture_reverse' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3812/3819] Built NLA.MI27.MixtureRelativeEntropy (7.7s) warning: NLA/MI27/MixtureRelativeEntropy.lean:86:8: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` warning: NLA/MI27/MixtureRelativeEntropy.lean:86:8: Unused tactic linter: `ring` does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` info: NLA/MI27/MixtureRelativeEntropy.lean:129:0: 'NLA.MI27.c12_relative_entropy_mixture_finite' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3813/3819] Built NLA.MI27.WeightedEntropy (8.8s) warning: NLA/MI27/WeightedEntropy.lean:52:4: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` info: NLA/MI27/WeightedEntropy.lean:77:0: 'NLA.MI27.weighted_entropy_finite_kernel' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3814/3819] Built NLA.MI27.EntropyTrajectory (7.5s) info: NLA/MI27/EntropyTrajectory.lean:115:0: 'NLA.MI27.entropy_trajectory_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3815/3819] Built NLA.MI27.LogarithmicCommutatorDual (8.2s) info: NLA/MI27/LogarithmicCommutatorDual.lean:81:0: 'NLA.MI27.logarithmic_commutator_dual_bound' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3816/3819] Built NLA.MI27.LogarithmicCommutator (7.6s) info: NLA/MI27/LogarithmicCommutator.lean:49:0: 'NLA.MI27.logarithmic_commutator_bound' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3817/3819] Built Solution (8.1s) info: Solution.lean:12:0: 'NLA.MI27.half_coefficient_positive' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:15:0: 'NLA.MI27.spectral_function_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:18:0: 'NLA.MI27.normalize_positive_pair' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:21:0: 'NLA.MI27.positive_trace_operator_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:24:0: 'NLA.MI27.positive_commutator_trace_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:27:0: 'NLA.MI27.positive_part_variational' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:30:0: 'NLA.MI27.positive_part_trace_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:33:0: 'NLA.MI27.unitary_flow_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:36:0: 'NLA.MI27.hockey_stick_unitary_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:39:0: 'NLA.MI27.uniform_hockey_stick_cutoff' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:42:0: 'NLA.MI27.relative_entropy_finite_hockey_stick' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:45:0: 'NLA.MI27.weighted_entropy_finite_kernel' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:48:0: 'NLA.MI27.kernel_integrals' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:51:0: 'NLA.MI27.kernel_entropy_mass_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:54:0: 'NLA.MI27.entropy_trajectory_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:57:0: 'NLA.MI27.entropy_unitary_mix_derivative' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:60:0: 'NLA.MI27.skew_commutator_trace_norm' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:63:0: 'NLA.MI27.hermitian_trace_norm_witness' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:66:0: 'NLA.MI27.logarithmic_commutator_dual_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:69:0: 'NLA.MI27.logarithmic_commutator_bound' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3818/3819] Built RegistryRecord (6.8s) Build completed successfully (3819 jobs).