NR-03: quadratic correlation matrix nonnegative rank
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Complete Lean formalization of the negative n = 7 counterexample to the prescribed real Boolean matrix nonnegative-rank equality, with ten Comparator-boundary exports and the full source correspondence retained.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, NR-03/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-nr-03-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 13 September 2026
Verification PASSED
- Attempt
- 1
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:17:11.794030
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.NR03.not_targetStatement | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00111 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.NR03.not_targetStatement
Not NLA.NR03.targetStatement
RegistryProblems.Problem_OP_00111
Prop
Build log
lassical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block11.lean:56:0: 'NLA.NR03.RowCertificate.Four.row94' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block11.lean:62:0: 'NLA.NR03.RowCertificate.Four.row95' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3061/3070] Built NLA.NR03.RowCertificate.Four.Block12 (31s) info: NLA/NR03/RowCertificate/Four/Block12.lean:20:0: 'NLA.NR03.RowCertificate.Four.row96' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block12.lean:26:0: 'NLA.NR03.RowCertificate.Four.row97' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block12.lean:32:0: 'NLA.NR03.RowCertificate.Four.row98' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block12.lean:38:0: 'NLA.NR03.RowCertificate.Four.row99' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block12.lean:44:0: 'NLA.NR03.RowCertificate.Four.row100' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block12.lean:50:0: 'NLA.NR03.RowCertificate.Four.row101' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block12.lean:56:0: 'NLA.NR03.RowCertificate.Four.row102' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block12.lean:62:0: 'NLA.NR03.RowCertificate.Four.row103' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3062/3070] Built NLA.NR03.RowCertificate.Four.Block13 (31s) info: NLA/NR03/RowCertificate/Four/Block13.lean:20:0: 'NLA.NR03.RowCertificate.Four.row104' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block13.lean:26:0: 'NLA.NR03.RowCertificate.Four.row105' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block13.lean:32:0: 'NLA.NR03.RowCertificate.Four.row106' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block13.lean:38:0: 'NLA.NR03.RowCertificate.Four.row107' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block13.lean:44:0: 'NLA.NR03.RowCertificate.Four.row108' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block13.lean:50:0: 'NLA.NR03.RowCertificate.Four.row109' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block13.lean:56:0: 'NLA.NR03.RowCertificate.Four.row110' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block13.lean:62:0: 'NLA.NR03.RowCertificate.Four.row111' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3063/3070] Built NLA.NR03.RowCertificate.Four.Block14 (31s) info: NLA/NR03/RowCertificate/Four/Block14.lean:20:0: 'NLA.NR03.RowCertificate.Four.row112' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block14.lean:26:0: 'NLA.NR03.RowCertificate.Four.row113' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block14.lean:32:0: 'NLA.NR03.RowCertificate.Four.row114' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block14.lean:38:0: 'NLA.NR03.RowCertificate.Four.row115' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block14.lean:44:0: 'NLA.NR03.RowCertificate.Four.row116' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block14.lean:50:0: 'NLA.NR03.RowCertificate.Four.row117' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block14.lean:56:0: 'NLA.NR03.RowCertificate.Four.row118' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block14.lean:62:0: 'NLA.NR03.RowCertificate.Four.row119' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3064/3070] Built NLA.NR03.RowCertificate.Four.Block15 (35s) info: NLA/NR03/RowCertificate/Four/Block15.lean:20:0: 'NLA.NR03.RowCertificate.Four.row120' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block15.lean:26:0: 'NLA.NR03.RowCertificate.Four.row121' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block15.lean:32:0: 'NLA.NR03.RowCertificate.Four.row122' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block15.lean:38:0: 'NLA.NR03.RowCertificate.Four.row123' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block15.lean:44:0: 'NLA.NR03.RowCertificate.Four.row124' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block15.lean:50:0: 'NLA.NR03.RowCertificate.Four.row125' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block15.lean:56:0: 'NLA.NR03.RowCertificate.Four.row126' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/RowCertificate/Four/Block15.lean:62:0: 'NLA.NR03.RowCertificate.Four.row127' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3065/3070] Built NLA.NR03.FamilyIdentities (6.8s) info: NLA/NR03/FamilyIdentities.lean:160:0: 'NLA.NR03.singleton_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/FamilyIdentities.lean:295:0: 'NLA.NR03.pair_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/FamilyIdentities.lean:430:0: 'NLA.NR03.four_identity' depends on axioms: [propext, Classical.choice, Quot.sound] warning: NLA/NR03/FamilyIdentities.lean:450:19: This simp argument is unused: ha Hint: Omit it from the simp argument list. [apply] simp [natBool, hb] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` warning: NLA/NR03/FamilyIdentities.lean:450:23: This simp argument is unused: hb Hint: Omit it from the simp argument list. [apply] simp [natBool, ha] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` ℹ [3066/3070] Built NLA.NR03.Certificate (3.6s) info: NLA/NR03/Certificate.lean:28:0: 'NLA.NR03.full_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR03/Certificate.lean:36:0: 'NLA.NR03.generic_scaled_identity' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3067/3070] Built NLA.NR03.Rank (3.6s) ℹ [3068/3070] Built Solution (4.6s) info: Solution.lean:21:0: 'NLA.NR03.cMatrix_nonnegative' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:23:0: 'NLA.NR03.boolVec_seven_card' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:25:0: 'NLA.NR03.nonnegative_rank_attained_minimal' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:27:0: 'NLA.NR03.rank_le_of_factorization' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:29:0: 'NLA.NR03.scaled_certificate_gives_factorization' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:31:0: 'NLA.NR03.witness_scaled_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:33:0: 'NLA.NR03.witness_factorization' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:35:0: 'NLA.NR03.witness_rank_upper_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:37:0: 'NLA.NR03.witness_not_full_rank' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:39:0: 'NLA.NR03.not_targetStatement' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3069/3070] Built RegistryRecord (3.0s) Build completed successfully (3070 jobs).