PF-02: disconnected minimal PSD factorization orbits
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Complete exact counterexample to the original universal connectedness question: a positive integer matrix of actual rank six and attained PSD rank three has a disconnected full real congruence quotient with its Euclidean quotient topology.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, PF-02/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-pf-02-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 15 September 2026
Verification PASSED
- Attempt
- 1
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:02:11.842211
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.PF02.canonical_counterexample | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00113 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.PF02.canonical_counterexample
Not NLA.PF02.AllMinimalOrbitsConnected
RegistryProblems.Problem_OP_00113
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [3642/3653] Built NLA.PF02.Definitions (6.4s) ✔ [3643/3653] Built NLA.PF02.Orbits (9.5s) ✔ [3644/3653] Built NLA.PF02.Rank (6.0s) ℹ [3645/3653] Built NLA.PF02.Action (10s) info: NLA/PF02/Action.lean:74:0: 'NLA.PF02.changeBasis_preserves_factorization' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/Action.lean:75:0: 'NLA.PF02.changeBasis_congruent' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/Action.lean:76:0: 'NLA.PF02.congruent_iff_changeBasis' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3646/3653] Built NLA.PF02.Data (27s) info: NLA/PF02/Data.lean:95:0: 'NLA.PF02.thirty_two_pos' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/Data.lean:96:0: 'NLA.PF02.explicit_factorizations' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/Data.lean:97:0: 'NLA.PF02.witness_numeric_data' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3647/3653] Built NLA.PF02.Coordinates (5.7s) info: NLA/PF02/Coordinates.lean:74:0: 'NLA.PF02.trace_coordinate_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/Coordinates.lean:75:0: 'NLA.PF02.factorization_coordinate_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/Coordinates.lean:76:0: 'NLA.PF02.congruence_covariance' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/Coordinates.lean:77:0: 'NLA.PF02.rowCoordinates_congruence' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3648/3653] Built NLA.PF02.CongruencePolynomial (11s) info: NLA/PF02/CongruencePolynomial.lean:38:0: 'NLA.PF02.congruenceCoordinates_det' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/CongruencePolynomial.lean:39:0: 'NLA.PF02.orientation_congruent' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3649/3653] Built NLA.PF02.Topology (4.1s) info: NLA/PF02/Topology.lean:81:0: 'NLA.PF02.orbit_quotient_disconnected' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3650/3653] Built NLA.PF02.Proof (4.1s) info: NLA/PF02/Proof.lean:80:0: 'NLA.PF02.witness_data' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/Proof.lean:81:0: 'NLA.PF02.witness_factorizations' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/Proof.lean:82:0: 'NLA.PF02.witness_minimal_rank' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/Proof.lean:83:0: 'NLA.PF02.orbit_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/Proof.lean:84:0: 'NLA.PF02.orientation_nonvanishing' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/Proof.lean:85:0: 'NLA.PF02.orientation_preserved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/Proof.lean:86:0: 'NLA.PF02.quotient_separation' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/Proof.lean:87:0: 'NLA.PF02.witness_disconnected' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF02/Proof.lean:88:0: 'NLA.PF02.canonical_counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3651/3653] Built Solution (3.7s) ✔ [3652/3653] Built RegistryRecord (3.8s) Build completed successfully (3653 jobs).