NR-04: the nine-point distance matrix has nonnegative rank seven
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
The real nine-point squared distance matrix has nonnegative rank seven, including arbitrary real factors and zero or degenerate factor columns. Local serial Lean, two nonauthor final reviews and two published-source Linux verification runs pass.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, NR-04/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-nr-04-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:06:22.267153
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.NR04.canonical_six_factor_impossible | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00112 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.NR04.canonical_six_factor_impossible
Not (Exists fun W => Exists fun H => And (∀ (i : Fin 9) (j : Fin 6), Real.instLE.le 0 (W i j)) (And (∀ (i : Fin 6) (j : Fin 9), Real.instLE.le 0 (H i j)) (Eq (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul W H) NLA.NR04.distanceNine)))
RegistryProblems.Problem_OP_00112
Prop
Build log
or proofs because of proof irrelevance. Note: This linter can be disabled with `set_option linter.style.haveILetI false` info: NLA/NR04/FiniteSection.lean:175:0: 'NLA.NR04.extreme_eq_of_weight_support_subset' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/FiniteSection.lean:176:0: 'NLA.NR04.finite_extremePoints_affine_section' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/FiniteSection.lean:177:0: 'NLA.NR04.convexHull_extremePoints_affine_section' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2335/2345] Built NLA.NR04.PlaneOrderKey (12s) info: NLA/NR04/PlaneOrderKey.lean:91:0: 'NLA.NR04.plane_order_key_center' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/PlaneOrderKey.lean:92:0: 'NLA.NR04.plane_order_key_center_lt' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/PlaneOrderKey.lean:93:0: 'NLA.NR04.plane_order_key_lt_iff_of_ne' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/PlaneOrderKey.lean:94:0: 'NLA.NR04.plane_order_key_injective' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/PlaneOrderKey.lean:95:0: 'NLA.NR04.plane_order_key_triple_positive' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2336/2376] Built NLA.NR04.SectionContact (11s) info: NLA/NR04/SectionContact.lean:107:0: 'NLA.NR04.nonnegative_of_mem_columnHull' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/SectionContact.lean:108:0: 'NLA.NR04.finite_extremePoints_columnSection' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/SectionContact.lean:109:0: 'NLA.NR04.convexHull_extremePoints_columnSection' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/SectionContact.lean:110:0: 'NLA.NR04.section_contact_bound' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3670/3684] Built NLA.NR04.PlaneKeyNormalization (14s) info: NLA/NR04/PlaneKeyNormalization.lean:60:0: 'NLA.NR04.finite_extreme_family_key_order' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3671/3684] Built NLA.NR04.Numerical (13s) info: NLA/NR04/Numerical.lean:25:0: 'NLA.NR04.minor_eight_positive' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3672/3684] Built NLA.NR04.NineGridPlanarObstruction (10s) info: NLA/NR04/NineGridPlanarObstruction.lean:71:0: 'NLA.NR04.nine_grid_not_all_extreme' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3673/3684] Built NLA.NR04.OrdinaryRank (14s) warning: NLA/NR04/OrdinaryRank.lean:36:28: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` info: NLA/NR04/OrdinaryRank.lean:58:0: 'NLA.NR04.distance_rank_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3674/3684] Built NLA.NR04.ReflectionCertificate (13s) warning: NLA/NR04/ReflectionCertificate.lean:106:32: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` info: NLA/NR04/ReflectionCertificate.lean:134:0: 'NLA.NR04.distance_index_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/ReflectionCertificate.lean:135:0: 'NLA.NR04.centered_labels' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/ReflectionCertificate.lean:136:0: 'NLA.NR04.reflection_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/ReflectionCertificate.lean:137:0: 'NLA.NR04.seven_factor_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/ReflectionCertificate.lean:138:0: 'NLA.NR04.distance_sign_pattern' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3675/3684] Built NLA.NR04.ColumnPlaneGridObstruction (6.8s) info: NLA/NR04/ColumnPlaneGridObstruction.lean:68:0: 'NLA.NR04.nine_grid_in_column_plane_not_all_extreme' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3676/3684] Built NLA.NR04.HeightCrossingObstruction (5.4s) info: NLA/NR04/HeightCrossingObstruction.lean:71:0: 'NLA.NR04.height_crossings_not_all_extreme_in_column_plane' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3677/3684] Built NLA.NR04.ExceptionalHeightBound (6.4s) warning: NLA/NR04/ExceptionalHeightBound.lean:33:2: 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` info: NLA/NR04/ExceptionalHeightBound.lean:59:0: 'NLA.NR04.height_distinct_exception_bound_in_column_plane' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3678/3684] Built NLA.NR04.SmallSectionBound (5.7s) info: NLA/NR04/SmallSectionBound.lean:63:0: 'NLA.NR04.rank_four_section_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/SmallSectionBound.lean:64:0: 'NLA.NR04.small_section_bound' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3679/3684] Built NLA.NR04.LowRankFactorObstruction (6.2s) info: NLA/NR04/LowRankFactorObstruction.lean:64:0: 'NLA.NR04.low_rank_factor_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3680/3684] Built NLA.NR04.GeneralLowerBound (6.5s) info: NLA/NR04/GeneralLowerBound.lean:43:0: 'NLA.NR04.general_rank_seven_lower' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3681/3684] Built NLA.NR04.FinalBounds (7.3s) info: NLA/NR04/FinalBounds.lean:48:0: 'NLA.NR04.nine_point_no_small_factor' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/FinalBounds.lean:49:0: 'NLA.NR04.nine_point_nonnegative_rank_seven' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/NR04/FinalBounds.lean:50:0: 'NLA.NR04.canonical_six_factor_impossible' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3682/3684] Built Solution (7.5s) info: Solution.lean:21:0: 'NLA.NR04.minor_eight_positive' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:22:0: 'NLA.NR04.distance_index_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:23:0: 'NLA.NR04.centered_labels' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:24:0: 'NLA.NR04.reflection_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:25:0: 'NLA.NR04.seven_factor_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:26:0: 'NLA.NR04.distance_rank_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:27:0: 'NLA.NR04.distance_sign_pattern' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:28:0: 'NLA.NR04.small_section_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:29:0: 'NLA.NR04.section_contact_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:30:0: 'NLA.NR04.low_rank_factor_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:31:0: 'NLA.NR04.rank_three_small_factor' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:32:0: 'NLA.NR04.general_rank_seven_lower' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:33:0: 'NLA.NR04.nine_point_no_small_factor' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:34:0: 'NLA.NR04.nine_point_nonnegative_rank_seven' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:35:0: 'NLA.NR04.canonical_six_factor_impossible' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3683/3684] Built RegistryRecord (7.3s) Build completed successfully (3684 jobs).