NM-04: the complete Rowland–Wu polynomial identity for rectangular Sinkhorn scaling
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Complete Lean verification of the original Rowland-Wu coefficient identity for every strictly positive real rectangular matrix, including positive scaling existence and uniqueness, empty and singular minors, and all transition signs.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, NM-04/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-nm-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:27.269498
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.NM04.rowland_wu_identity | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00110 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.NM04.rowland_wu_identity
∀ {m n : Nat} (hm : instLENat.le 1 m) (hn : instLENat.le 1 n) (A : NLA.NM04.Rect m n), NLA.NM04.Positive A → Eq (Finset.univ.sum fun E => instHMul.hMul (instHMul.hMul (instHMul.hMul (instHSMul.hSMul (Real.instInv.inv m.cast) ((NLA.NM04.HReal m n).submatrix Subtype.val Subtype.val)).det (E.prod fun I => NLA.NM04.delta A hm hn I)) ((Finset.instSDiff.sdiff Finset.univ E).prod fun I => NLA.NM04.gamma A hm hn I)) (instHPow.hPow (NLA.NM04.sinkhorn A (NLA.NM04.firstIndex hm) (NLA.NM04.firstIndex hn)) E.card)) 0
RegistryProblems.Problem_OP_00110
Prop
Build log
' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3660/3671] Built NLA.NM04.ScalingExistence (7.0s) info: NLA/NM04/ScalingExistence.lean:54:0: 'NLA.NM04.positive_balanced_scaling_exists' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3661/3671] Built NLA.NM04.PencilConsequences (7.7s) info: NLA/NM04/PencilConsequences.lean:114:0: 'NLA.NM04.weight_empty' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NM04/PencilConsequences.lean:115:0: 'NLA.NM04.weight_nonzero' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NM04/PencilConsequences.lean:116:0: 'NLA.NM04.pencil_kernel_of_minor_relation' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NM04/PencilConsequences.lean:117:0: 'NLA.NM04.transport_scaled_pencil_kernel' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NM04/PencilConsequences.lean:118:0: 'NLA.NM04.coefficient_sum_of_pencil_kernel' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3662/3671] Built NLA.NM04.BorderedMinors (7.2s) info: NLA/NM04/BorderedMinors.lean:115:0: 'NLA.NM04.borderedMinor_eq_matrix' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NM04/BorderedMinors.lean:117:0: 'NLA.NM04.borderedMinor_det_of_row_mem' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NM04/BorderedMinors.lean:119:0: 'NLA.NM04.borderedMinor_det_of_column_mem' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NM04/BorderedMinors.lean:121:0: 'NLA.NM04.borderedMinor_det_of_not_mem' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NM04/BorderedMinors.lean:123:0: 'NLA.NM04.cofactorForm_border_entry' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3663/3671] Built NLA.NM04.MinorColumnExchange (7.3s) info: NLA/NM04/MinorColumnExchange.lean:150:0: 'NLA.NM04.minorColumnForm_exchange' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NM04/MinorColumnExchange.lean:152:0: 'NLA.NM04.cofactorForm_column_sum' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NM04/MinorColumnExchange.lean:154:0: 'NLA.NM04.minor_column_exchange_identity' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3664/3671] Built NLA.NM04.SinkhornSemantics (6.0s) info: NLA/NM04/SinkhornSemantics.lean:32:0: 'NLA.NM04.sinkhorn_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3665/3671] Built NLA.NM04.MinorRaising (7.0s) info: NLA/NM04/MinorRaising.lean:107:0: 'NLA.NM04.cofactorForm_row_column_sum' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NM04/MinorRaising.lean:109:0: 'NLA.NM04.borderedMinor_sum' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NM04/MinorRaising.lean:111:0: 'NLA.NM04.minor_raising_identity' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3666/3671] Built NLA.NM04.MinorRowExchange (6.2s) info: NLA/NM04/MinorRowExchange.lean:44:0: 'NLA.NM04.minor_row_exchange_identity' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3667/3671] Built NLA.NM04.BalancedMinor (3.9s) info: NLA/NM04/BalancedMinor.lean:88:0: 'NLA.NM04.balanced_minor_relation' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3668/3671] Built NLA.NM04.Canonical (3.8s) info: NLA/NM04/Canonical.lean:27:0: 'NLA.NM04.balanced_null_vector' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NM04/Canonical.lean:40:0: 'NLA.NM04.sinkhorn_pencil_singular' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NM04/Canonical.lean:54:0: 'NLA.NM04.rowland_wu_identity' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3669/3671] Built Solution (3.8s) info: Solution.lean:14:0: 'NLA.NM04.coercivity_half_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:16:0: 'NLA.NM04.row_partition_positive' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:18:0: 'NLA.NM04.potential_continuous' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:20:0: 'NLA.NM04.potential_line_derivative' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:22:0: 'NLA.NM04.zero_mean_coercivity' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:24:0: 'NLA.NM04.potential_attains_minimum' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:26:0: 'NLA.NM04.potential_minimum_has_margins' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:28:0: 'NLA.NM04.positive_balanced_scaling_exists' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:30:0: 'NLA.NM04.positive_balanced_scaling_unique' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:32:0: 'NLA.NM04.sinkhorn_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:34:0: 'NLA.NM04.position_sorted_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:36:0: 'NLA.NM04.empty_minor_values' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:38:0: 'NLA.NM04.H_diagonal' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:40:0: 'NLA.NM04.H_raising' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:42:0: 'NLA.NM04.H_lowering' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:44:0: 'NLA.NM04.H_column_exchange' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:46:0: 'NLA.NM04.H_row_exchange' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:48:0: 'NLA.NM04.H_other' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:50:0: 'NLA.NM04.weighted_principal_minor_expansion' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:52:0: 'NLA.NM04.cofactor_signed_minor_formula' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:54:0: 'NLA.NM04.universal_rank_one_update' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:56:0: 'NLA.NM04.universal_bordered_determinant' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:58:0: 'NLA.NM04.minor_lowering_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:60:0: 'NLA.NM04.minor_column_exchange_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:62:0: 'NLA.NM04.minor_row_exchange_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:64:0: 'NLA.NM04.minor_raising_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:66:0: 'NLA.NM04.schur_margin_identities' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:68:0: 'NLA.NM04.schur_bordered_minor' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:70:0: 'NLA.NM04.balanced_minor_relation' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:72:0: 'NLA.NM04.weighted_transition_action' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:74:0: 'NLA.NM04.balanced_null_vector' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:76:0: 'NLA.NM04.diagonal_minor_covariance' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:78:0: 'NLA.NM04.diagonal_pencil_covariance' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:80:0: 'NLA.NM04.sinkhorn_pencil_singular' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:82:0: 'NLA.NM04.rowland_wu_identity' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3670/3671] Built RegistryRecord (3.6s) Build completed successfully (3671 jobs).