PF-03: no rational nonnegative factor for a rational completely positive boundary matrix
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Complete Lean formalization of the negative answer to the original PF-03 universal question, with arbitrary positive finite factor widths and frontier in the real symmetric-matrix subtype. Local serial Lean, two independent nonauthor final reviews and two published-source Linux Comparator/kernel/sandbox runs pass.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, PF-03/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-pf-03-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:25.097619
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.PF03.canonical_negative_answer | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00114 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.PF03.canonical_negative_answer
Not NLA.PF03.RationalBoundaryFactorability
RegistryProblems.Problem_OP_00114
Prop
Build log
an:58:0: 'NLA.PF03.cross_cone_lower2' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3672/3694] Built NLA.PF03.CrossConeSigns1 (11s) info: NLA/PF03/CrossConeSigns1.lean:15:0: 'NLA.PF03.cross_cone_lower1' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3673/3694] Built NLA.PF03.CrossConeSigns0 (11s) info: NLA/PF03/CrossConeSigns0.lean:15:0: 'NLA.PF03.cross_cone_lower0' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3674/3694] Built NLA.PF03.QuadraticGeneratorBlock6 (10s) info: NLA/PF03/QuadraticGeneratorBlock6.lean:15:0: 'NLA.PF03.quadratic_generator_block6' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3675/3694] Built NLA.PF03.QuadraticGeneratorBlock5 (10s) info: NLA/PF03/QuadraticGeneratorBlock5.lean:15:0: 'NLA.PF03.quadratic_generator_block5' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3676/3694] Built NLA.PF03.QuadraticGeneratorBlock4 (10s) info: NLA/PF03/QuadraticGeneratorBlock4.lean:15:0: 'NLA.PF03.quadratic_generator_block4' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3677/3694] Built NLA.PF03.QuadraticGeneratorBlock3 (10s) info: NLA/PF03/QuadraticGeneratorBlock3.lean:15:0: 'NLA.PF03.quadratic_generator_block3' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3678/3694] Built NLA.PF03.QuadraticGeneratorBlock2 (9.0s) info: NLA/PF03/QuadraticGeneratorBlock2.lean:15:0: 'NLA.PF03.quadratic_generator_block2' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3679/3694] Built NLA.PF03.QuadraticGeneratorBlock1 (10s) info: NLA/PF03/QuadraticGeneratorBlock1.lean:15:0: 'NLA.PF03.quadratic_generator_block1' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3680/3694] Built NLA.PF03.QuadraticGeneratorBlock0 (9.9s) info: NLA/PF03/QuadraticGeneratorBlock0.lean:15:0: 'NLA.PF03.quadratic_generator_block0' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3681/3694] Built NLA.PF03.SeedLocalData (8.0s) info: NLA/PF03/SeedLocalData.lean:37:0: 'NLA.PF03.seed_local_data' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3682/3694] Built NLA.PF03.ConePointed (8.1s) info: NLA/PF03/ConePointed.lean:36:0: 'NLA.PF03.cone_pointed' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3683/3694] Built NLA.PF03.QuadraticGeneratorCertificate (8.2s) info: NLA/PF03/QuadraticGeneratorCertificate.lean:29:0: 'NLA.PF03.quadraticGeneratorCubic_cache' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3684/3694] Built NLA.PF03.ConeLocalQuadratics (8.7s) info: NLA/PF03/ConeLocalQuadratics.lean:72:0: 'NLA.PF03.cone_group_local_kernel' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF03/ConeLocalQuadratics.lean:74:0: 'NLA.PF03.seedColumn_quad_zero' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3685/3694] Built NLA.PF03.PaddedFactor (8.7s) info: NLA/PF03/PaddedFactor.lean:83:0: 'NLA.PF03.padded_real_factor' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3686/3694] Built NLA.PF03.CrossConeCertificate (7.1s) info: NLA/PF03/CrossConeCertificate.lean:65:0: 'NLA.PF03.cross_cone_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3687/3694] Built NLA.PF03.ConeCrossQuadratics (4.2s) info: NLA/PF03/ConeCrossQuadratics.lean:65:0: 'NLA.PF03.cone_group_cross_zero' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3688/3694] Built NLA.PF03.ConeQuadraticZeros (4.3s) warning: NLA/PF03/ConeQuadraticZeros.lean:46:8: `push_neg` has been deprecated. Prefer using `push Not` instead. If you'd rather continue using `push_neg` in your project, you can implement it as follows: ``` open Lean.Parser.Tactic in macro "push_neg" cfg:optConfig loc:(location)? : tactic => `(tactic| push $cfg:optConfig Not $[$loc]?) ``` info: NLA/PF03/ConeQuadraticZeros.lean:70:0: 'NLA.PF03.cone_quadratic_zeros' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3689/3694] Built NLA.PF03.ConeRationalZeros (4.3s) info: NLA/PF03/ConeRationalZeros.lean:20:0: 'NLA.PF03.cone_rational_zeros' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3690/3694] Built NLA.PF03.NoRationalFactor (4.7s) warning: NLA/PF03/NoRationalFactor.lean:23:5: Variable name `hker` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hker Note: This linter can be disabled with `set_option linter.unusedVariables false` info: NLA/PF03/NoRationalFactor.lean:57:0: 'NLA.PF03.no_rational_factor' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3691/3694] Built NLA.PF03.Counterexample (4.3s) info: NLA/PF03/Counterexample.lean:37:0: 'NLA.PF03.pf03_counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/PF03/Counterexample.lean:39:0: 'NLA.PF03.canonical_negative_answer' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3692/3694] Built Solution (4.3s) info: Solution.lean:18:0: 'NLA.PF03.alpha_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:20:0: 'NLA.PF03.cubic_eval_operations' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:22:0: 'NLA.PF03.cubic_eval_injective' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:24:0: 'NLA.PF03.seed_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:26:0: 'NLA.PF03.seed_quadratic_form' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:28:0: 'NLA.PF03.seed_local_data' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:30:0: 'NLA.PF03.local_quadratic_kernel' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:32:0: 'NLA.PF03.rational_ray_zero' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:34:0: 'NLA.PF03.triangle_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:36:0: 'NLA.PF03.cross_cone_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:38:0: 'NLA.PF03.positive_slice_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:40:0: 'NLA.PF03.cone_quadratic_zeros' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:42:0: 'NLA.PF03.cone_rational_zeros' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:44:0: 'NLA.PF03.cone_pointed' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:46:0: 'NLA.PF03.one_variable_projection' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:48:0: 'NLA.PF03.rational_projection' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:50:0: 'NLA.PF03.rational_cone_halfspaces' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:52:0: 'NLA.PF03.pointed_halfspaces_injective' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:54:0: 'NLA.PF03.gram_factor_transport' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:56:0: 'NLA.PF03.trace_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:58:0: 'NLA.PF03.no_rational_factor' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:60:0: 'NLA.PF03.padded_real_factor' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:62:0: 'NLA.PF03.cp_zero_diagonal_frontier' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:64:0: 'NLA.PF03.pf03_counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:66:0: 'NLA.PF03.canonical_negative_answer' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3693/3694] Built RegistryRecord (4.3s) Build completed successfully (3694 jobs).