SP-12: chromatic nullity with positive semidefiniteness and SAP

Recorded by the registry's curators from GitHub; the authors did not submit it here.

OpenAI Codex AI agents (Lean formalization, independent review, packaging)

Complete proof of the unchanged all-graph chromatic nullity target, with exact copied source closure and kernel trust. Independent full source/package reviews and actual isolated Linux Comparator/kernel verification pass.

Claims

LEAN VERIFIED OP-00253 — A chromatic lower bound for positive-semidefinite nullity with SAP

Full resolution · statement matched the canonical formalisation

Files and sources

Paper: OpenProblemsInNLA @ 099805e, SP-12/lean/ ↗
Lean bundle: submissions/bundles/openproblemsinnla-sp-12-lean.tar.gz
Toolchain: leanprover/lean4:v4.33.1
Posted on GitHub: 18 October 2026

Verification PASSED

Attempt: 1
Toolchain: leanprover/lean4:v4.33.1
Auditor: v2 · modal
lake build: succeeded
Kernel replay: succeeded
Duration: 0:03:57.205265

Warnings

These never block publication — unused hypotheses have routine false positives — but they are the best mechanical signal of a mis-transcribed statement, so they are shown rather than hidden.

author_constant_in_statement — The statement is written in terms the author defined: NLA.Statements.SP12.Target. The result is only as faithful as those definitions.
NLA.SP12.target

Declarations audited

Declaration	Kind	Axioms	Unused hypotheses	Canonical
NLA.SP12.target	theorem · Prop	propext, Classical.choice, Quot.sound	none	matched
RegistryProblems.Problem_OP_00253	definition	propext, Classical.choice, Quot.sound	none	no canonical statement

NLA.SP12.target

NLA.Statements.SP12.Target

RegistryProblems.Problem_OP_00253

Prop

Build log

cal.choice, Quot.sound]
info: NLA/Proofs/SP11/LSSLabelBounds.lean:215:0: 'NLA.Proofs.SP11.lssGarden_child_occurrenceLabel_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/SP11/LSSLabelBounds.lean:216:0: 'NLA.Proofs.SP11.lssGarden_childOccurrence_label_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3048/3057] Built NLA.Proofs.SP11.DoubleHistogramWeights (5.0s)
warning: NLA/Proofs/SP11/DoubleHistogramWeights.lean:81:29: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: NLA/Proofs/SP11/DoubleHistogramWeights.lean:87:29: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
info: NLA/Proofs/SP11/DoubleHistogramWeights.lean:146:0: 'NLA.Proofs.SP11.GardenTree.vertexClassWeight_doubleColoringExponent' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
info: NLA/Proofs/SP11/DoubleHistogramWeights.lean:147:0: 'NLA.Proofs.SP11.GardenTree.doubleIncidentSum_eq_of_exponent_eq' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [3049/3057] Built NLA.Proofs.SP11.OccurrenceParent (6.2s)
info: NLA/Proofs/SP11/OccurrenceParent.lean:57:0: 'NLA.Proofs.SP11.GardenTree.exists_parent_of_not_root' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3050/3060] Built NLA.Proofs.SP11.CanonicalPair (6.4s)
info: NLA/Proofs/SP11/CanonicalPair.lean:176:0: 'NLA.Proofs.SP11.canonicalPair_sign_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3051/3060] Built NLA.Proofs.SP11.ColoringExt (4.9s)
info: NLA/Proofs/SP11/ColoringExt.lean:54:0: 'NLA.Proofs.SP11.GardenTree.doubleColoring_ext_of_occurrence_outputs' depends on axioms: [propext, Quot.sound]
ℹ [3052/3060] Built NLA.Proofs.SP11.PriorInsertion (6.0s)
info: NLA/Proofs/SP11/PriorInsertion.lean:131:0: 'NLA.Proofs.SP11.augmentedPriorVertex_at_insertion' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/SP11/PriorInsertion.lean:132:0: 'NLA.Proofs.SP11.augmentedPriorVertex_succAbove' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3053/3060] Built NLA.Proofs.SP11.OrdinaryBlockers (5.8s)
info: NLA/Proofs/SP11/OrdinaryBlockers.lean:83:0: 'NLA.Proofs.SP11.GardenTree.child_occurrence_blockers' depends on axioms: [propext, Quot.sound]
ℹ [3054/3060] Built NLA.Proofs.SP11.CanonicalOutputs (5.6s)
info: NLA/Proofs/SP11/CanonicalOutputs.lean:75:0: 'NLA.Proofs.SP11.GardenTree.normalColoring_child_output_val' depends on axioms: [propext]
info: NLA/Proofs/SP11/CanonicalOutputs.lean:76:0: 'NLA.Proofs.SP11.GardenTree.insertedColoring_input_val_of_not_root' depends on axioms: [propext]
✔ [3055/3082] Built NLA.Proofs.SP11.AugmentedColors (3.2s)
ℹ [3067/3087] Built NLA.Proofs.SP11.DoubleOccurrenceShape (6.0s)
info: NLA/Proofs/SP11/DoubleOccurrenceShape.lean:147:0: 'NLA.Proofs.SP11.doubleLSS_coloring_eq_of_exponent_eq_and_blockers' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [3074/3087] Built NLA.Statements.SP12 (4.7s)
info: NLA/Statements/SP12.lean:47:0: 'NLA.Statements.SP12.Target' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3080/3090] Built NLA.Proofs.SP11.MonomialProducts (6.1s)
info: NLA/Proofs/SP11/MonomialProducts.lean:105:0: 'NLA.Proofs.SP11.occurrenceExponent_eq_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/SP11/MonomialProducts.lean:106:0: 'NLA.Proofs.SP11.sum_monomial_ne_zero_of_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3081/3090] Built NLA.Proofs.SP11.TopOccurrences (7.4s)
info: NLA/Proofs/SP11/TopOccurrences.lean:238:0: 'NLA.Proofs.SP11.augmentedTopOccurrence_blockers' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3083/3090] Built NLA.Proofs.SP11.GramCoefficient (4.7s)
info: NLA/Proofs/SP11/GramCoefficient.lean:46:0: 'NLA.Proofs.SP11.polynomialGram_ne_zero_of_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3084/3101] Built NLA.Proofs.SP11.DiagonalUniqueness (6.1s)
info: NLA/Proofs/SP11/DiagonalUniqueness.lean:155:0: 'NLA.Proofs.SP11.canonicalPair_diagonal_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3154/3160] Built NLA.Proofs.SP11.EdgeUniqueness (6.9s)
info: NLA/Proofs/SP11/EdgeUniqueness.lean:103:0: 'NLA.Proofs.SP11.canonicalPair_edge_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3155/3185] Built NLA.Proofs.SP12.SAPTestSpace (7.9s)
info: NLA/Proofs/SP12/SAPTestSpace.lean:119:0: 'NLA.Proofs.SP12.isOpen_injective_testMultiplication' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/SP12/SAPTestSpace.lean:120:0: 'NLA.Proofs.SP12.strongArnold_iff_injective_testMultiplication' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [3198/3206] Built NLA.Proofs.SP11.Final (5.0s)
info: NLA/Proofs/SP11/Final.lean:61:0: 'NLA.Proofs.SP11.target' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3201/3206] Built NLA.Proofs.SP12.ExtendedRows (6.9s)
info: NLA/Proofs/SP12/ExtendedRows.lean:117:0: 'NLA.Proofs.SP12.injective_testMultiplication_extendedRows_zero' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [3202/3210] Built NLA.Proofs.SP12.RealLSS (5.0s)
info: NLA/Proofs/SP12/RealLSS.lean:114:0: 'NLA.Proofs.SP12.evaluated_polynomialLSS_prior_linearIndependent' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [3204/3210] Built NLA.Proofs.SP12.GramDifferential (7.0s)
info: NLA/Proofs/SP12/GramDifferential.lean:246:0: 'NLA.Proofs.SP12.map_nonedgeGram_nhds' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3206/3210] Built NLA.Proofs.SP12.GramSAP (6.1s)
info: NLA/Proofs/SP12/GramSAP.lean:138:0: 'NLA.Proofs.SP12.strongArnold_submatrix_equiv' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/SP12/GramSAP.lean:139:0: 'NLA.Proofs.SP12.gram_nonnegativeQuadraticForm' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/SP12/GramSAP.lean:140:0: 'NLA.Proofs.SP12.gram_strongArnold_of_prior_linearIndependent' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [3207/3210] Built NLA.Proofs.SP12.NeighborhoodLifting (5.9s)
info: NLA/Proofs/SP12/NeighborhoodLifting.lean:43:0: 'NLA.Proofs.SP12.exists_nonzero_lift_in_nhds' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3208/3234] Built NLA.Proofs.SP12.StrongDelta (5.4s)
info: NLA/Proofs/SP12/StrongDelta.lean:66:0: 'NLA.Proofs.SP12.exists_strongDelta_gram' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3229/3237] Built NLA.Proofs.SP12.Chromatic (5.4s)
info: NLA/Proofs/SP12/Chromatic.lean:118:0: 'NLA.Proofs.SP12.chromatic_delete_zero_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3230/3237] Built NLA.Proofs.SP12.VertexExtension (8.3s)
info: NLA/Proofs/SP12/VertexExtension.lean:168:0: 'NLA.Proofs.SP12.exists_vertexExtension' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3232/3237] Built NLA.Proofs.SP12.Critical (3.3s)
info: NLA/Proofs/SP12/Critical.lean:143:0: 'NLA.Proofs.SP12.critical_minDegree' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/SP12/Critical.lean:144:0: 'NLA.Proofs.SP12.exists_induced_degree_core' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3233/3237] Built NLA.Proofs.SP12.ChromaticInduction (3.3s)
info: NLA/Proofs/SP12/ChromaticInduction.lean:83:0: 'NLA.Proofs.SP12.target_of_strongDelta_and_extension' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3234/3237] Built NLA.Proofs.SP12.Final (3.3s)
info: NLA/Proofs/SP12/Final.lean:21:0: 'NLA.Proofs.SP12.target' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3235/3237] Built Solution (3.1s)
info: Solution.lean:13:0: 'NLA.SP12.target' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3236/3237] Built RegistryRecord (3.2s)
Build completed successfully (3237 jobs).