SP-11: unrestricted real symmetric delta conjecture
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 real symmetric delta target, with exact copied source closure and kernel trust. Independent full source/package reviews and actual isolated Linux Comparator/kernel verification are complete.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ 5487945, SP-11/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-sp-11-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
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:03:27.425366
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.SP11.target | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00252 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.SP11.target
NLA.Statements.SP11.Target
RegistryProblems.Problem_OP_00252
Prop
Build log
lLSS_coordinateExpansion' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/SP11/GardenExpansion.lean:111:0: 'NLA.Proofs.SP11.alternatingForm_basis_perm' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3038/3051] Built NLA.Proofs.SP11.PriorListStructure (7.1s) info: NLA/Proofs/SP11/PriorListStructure.lean:158:0: 'NLA.Proofs.SP11.OrderedGreedy.priorVertex_arity_le_slot' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/SP11/PriorListStructure.lean:159:0: 'NLA.Proofs.SP11.OrderedGreedy.augmentedPriorVertex_arity_le_slot' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3039/3053] Built NLA.Proofs.SP11.GardenColors (5.8s) info: NLA/Proofs/SP11/GardenColors.lean:122:0: 'NLA.Proofs.SP11.exists_sorted_coordinate_tuple' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/SP11/GardenColors.lean:123:0: 'NLA.Proofs.SP11.polynomialAlternatingForm_basis_eq_monomial' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3040/3056] Built NLA.Proofs.SP11.GardenTree (6.1s) info: NLA/Proofs/SP11/GardenTree.lean:98:0: 'NLA.Proofs.SP11.GardenTree.value_eq_sum_weight' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3041/3056] Built NLA.Proofs.SP11.ColorWeights (5.1s) info: NLA/Proofs/SP11/ColorWeights.lean:57:0: 'NLA.Proofs.SP11.vertexClassWeight_colorExponent' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3042/3056] Built NLA.Proofs.SP11.ColorBounds (4.0s) info: NLA/Proofs/SP11/ColorBounds.lean:55:0: 'NLA.Proofs.SP11.color_ge_slot_of_earlier_fixed' depends on axioms: [propext] info: NLA/Proofs/SP11/ColorBounds.lean:56:0: 'NLA.Proofs.SP11.outputColor_ge_arity' depends on axioms: [propext] ℹ [3043/3060] Built NLA.Proofs.SP11.LSSGarden (5.1s) info: NLA/Proofs/SP11/LSSGarden.lean:57:0: 'NLA.Proofs.SP11.polynomialLSS_eq_sum_garden' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3044/3060] Built NLA.Proofs.SP11.ColorRigidity (6.8s) info: NLA/Proofs/SP11/ColorRigidity.lean:99:0: 'NLA.Proofs.SP11.color_eq_of_class_incident_sums_and_blockers' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3045/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] ℹ [3046/3060] Built NLA.Proofs.SP11.DoubleRootGarden (8.2s) info: NLA/Proofs/SP11/DoubleRootGarden.lean:220:0: 'NLA.Proofs.SP11.GardenTree.dotProduct_eq_sum_doubleWeight' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/SP11/DoubleRootGarden.lean:242:0: 'NLA.Proofs.SP11.polynomialGram_eq_sum_signedGardenMonomial' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3047/3060] Built NLA.Proofs.SP11.CanonicalColoring (7.0s) info: NLA/Proofs/SP11/CanonicalColoring.lean:123:0: 'NLA.Proofs.SP11.GardenTree.normalColoring_admissible' depends on axioms: [propext, Quot.sound] info: NLA/Proofs/SP11/CanonicalColoring.lean:124:0: 'NLA.Proofs.SP11.GardenTree.insertedColoring_admissible' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/SP11/CanonicalColoring.lean:158:0: 'NLA.Proofs.SP11.lssGarden_normalStructure' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3048/3060] Built NLA.Proofs.SP11.AugmentedColors (4.9s) ℹ [3049/3060] Built NLA.Proofs.SP11.LSSLabelBounds (7.8s) info: NLA/Proofs/SP11/LSSLabelBounds.lean:214:0: 'NLA.Proofs.SP11.lssGarden_occurrenceLabel_eq_iff_root' depends on axioms: [propext, Classical.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] ⚠ [3050/3060] Built NLA.Proofs.SP11.DoubleHistogramWeights (6.8s) 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] ℹ [3051/3060] Built NLA.Proofs.SP11.OccurrenceParent (6.8s) 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] ℹ [3052/3060] Built NLA.Proofs.SP11.CanonicalPair (6.9s) info: NLA/Proofs/SP11/CanonicalPair.lean:176:0: 'NLA.Proofs.SP11.canonicalPair_sign_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3053/3060] Built NLA.Proofs.SP11.ColoringExt (5.1s) info: NLA/Proofs/SP11/ColoringExt.lean:54:0: 'NLA.Proofs.SP11.GardenTree.doubleColoring_ext_of_occurrence_outputs' depends on axioms: [propext, Quot.sound] ℹ [3054/3064] Built NLA.Proofs.SP11.OrdinaryBlockers (6.2s) info: NLA/Proofs/SP11/OrdinaryBlockers.lean:83:0: 'NLA.Proofs.SP11.GardenTree.child_occurrence_blockers' depends on axioms: [propext, Quot.sound] ℹ [3056/3085] Built NLA.Proofs.SP11.CanonicalOutputs (6.3s) 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] ℹ [3076/3085] 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] ℹ [3077/3085] Built NLA.Proofs.SP11.MonomialProducts (5.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] ℹ [3078/3085] Built NLA.Proofs.SP11.DiagonalUniqueness (7.9s) info: NLA/Proofs/SP11/DiagonalUniqueness.lean:155:0: 'NLA.Proofs.SP11.canonicalPair_diagonal_unique' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3079/3085] Built NLA.Proofs.SP11.TopOccurrences (8.1s) info: NLA/Proofs/SP11/TopOccurrences.lean:238:0: 'NLA.Proofs.SP11.augmentedTopOccurrence_blockers' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3080/3085] Built NLA.Proofs.SP11.GramCoefficient (5.0s) info: NLA/Proofs/SP11/GramCoefficient.lean:46:0: 'NLA.Proofs.SP11.polynomialGram_ne_zero_of_unique' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3081/3085] Built NLA.Proofs.SP11.EdgeUniqueness (5.0s) info: NLA/Proofs/SP11/EdgeUniqueness.lean:103:0: 'NLA.Proofs.SP11.canonicalPair_edge_unique' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3082/3085] Built NLA.Proofs.SP11.Final (3.8s) info: NLA/Proofs/SP11/Final.lean:61:0: 'NLA.Proofs.SP11.target' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3083/3085] Built Solution (3.7s) info: Solution.lean:13:0: 'NLA.SP11.target' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3084/3085] Built RegistryRecord (3.6s) Build completed successfully (3085 jobs).