RA-20: critical-point counts for symmetric rank-two approximation with diagonal zeros
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Complete negative resolution of the original joint generic critical-count conjecture: the actual count at n=s=3 is three, whereas its formula predicts four.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, RA-20/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-ra-20-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 13 September 2026
Verification PASSED
- Attempt
- 1
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:02:20.962802
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.RA20.not_criticalCountConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00118 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.RA20.not_criticalCountConjecture
Not NLA.RA20.criticalCountConjecture
RegistryProblems.Problem_OP_00118
Prop
Build log
nd] info: NLA/RA20/Generic.lean:103:0: 'NLA.RA20.generic_data_intersection_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [3489/3498] Built NLA.RA20.Differential (14s) warning: NLA/RA20/Differential.lean:103: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` warning: NLA/RA20/Differential.lean:105: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/RA20/Differential.lean:160:0: 'NLA.RA20.full_frobenius_differential_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Differential.lean:161:0: 'NLA.RA20.hollow_distance_semantics_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Differential.lean:162:0: 'NLA.RA20.component_hessians_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3490/3498] Built NLA.RA20.Algebra (9.1s) info: NLA/RA20/Algebra.lean:111:0: 'NLA.RA20.hollow_variety_semantics_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Algebra.lean:226:0: 'NLA.RA20.reduced_coordinate_ring_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3491/3498] Built NLA.RA20.Tangent (15s) info: NLA/RA20/Tangent.lean:141:0: 'NLA.RA20.polyDirectional_hollowPullback' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Tangent.lean:142:0: 'NLA.RA20.algebraic_tangent_space_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3492/3498] Built NLA.RA20.Smooth (19s) info: NLA/RA20/Smooth.lean:81:0: 'NLA.RA20.triple_product_not_formallySmooth' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Smooth.lean:152:0: 'NLA.RA20.formallySmooth_of_retraction' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Smooth.lean:217:0: 'NLA.RA20.abc_local_not_smooth' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Smooth.lean:358:0: 'NLA.RA20.abc_local_smooth' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Smooth.lean:409:0: 'NLA.RA20.abc_smooth_locus_iff' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Smooth.lean:411:0: 'NLA.RA20.abcPoint_comap' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Smooth.lean:472:0: 'NLA.RA20.reducedPoint_comap' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Smooth.lean:474:0: 'NLA.RA20.algebraic_smooth_locus_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3493/3498] Built NLA.RA20.Critical (5.0s) info: NLA/RA20/Critical.lean:50:0: 'NLA.RA20.hollow_frobenius_differential' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Critical.lean:52:0: 'NLA.RA20.generic_candidate_injective' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Critical.lean:144:0: 'NLA.RA20.smoothCritical_hollow_iff' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Critical.lean:146:0: 'NLA.RA20.critical_first_plane' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Critical.lean:148:0: 'NLA.RA20.critical_second_plane' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Critical.lean:150:0: 'NLA.RA20.critical_third_plane' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Critical.lean:198:0: 'NLA.RA20.generic_candidate_critical' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Critical.lean:200:0: 'NLA.RA20.generic_critical_exhaustion' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Critical.lean:202:0: 'NLA.RA20.generic_critical_locus_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3494/3498] Built NLA.RA20.Count (4.5s) info: NLA/RA20/Count.lean:57:0: 'NLA.RA20.critical_count_three' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Count.lean:58:0: 'NLA.RA20.generic_count_three_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Count.lean:59:0: 'NLA.RA20.generic_count_not_four_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Count.lean:60:0: 'NLA.RA20.not_criticalCountConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3495/3498] Built NLA.RA20.Proof (4.3s) info: NLA/RA20/Proof.lean:24:0: 'NLA.RA20.hollow_variety_semantics_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Proof.lean:26:0: 'NLA.RA20.reduced_coordinate_ring_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Proof.lean:28:0: 'NLA.RA20.algebraic_smooth_locus_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Proof.lean:30:0: 'NLA.RA20.algebraic_tangent_space_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Proof.lean:32:0: 'NLA.RA20.full_frobenius_differential_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Proof.lean:34:0: 'NLA.RA20.hollow_distance_semantics_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Proof.lean:36:0: 'NLA.RA20.generic_critical_locus_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Proof.lean:38:0: 'NLA.RA20.component_hessians_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Proof.lean:40:0: 'NLA.RA20.generic_data_intersection_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Proof.lean:42:0: 'NLA.RA20.generic_count_three_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Proof.lean:44:0: 'NLA.RA20.generic_count_not_four_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA20/Proof.lean:46:0: 'NLA.RA20.not_criticalCountConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3496/3498] Built Solution (4.4s) info: Solution.lean:94:0: 'NLA.RA20.hollow_variety_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:96:0: 'NLA.RA20.reduced_coordinate_ring' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:98:0: 'NLA.RA20.algebraic_smooth_locus' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:100:0: 'NLA.RA20.algebraic_tangent_space' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:102:0: 'NLA.RA20.full_frobenius_differential' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:104:0: 'NLA.RA20.hollow_distance_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:106:0: 'NLA.RA20.generic_critical_locus' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:108:0: 'NLA.RA20.component_hessians' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:110:0: 'NLA.RA20.generic_data_intersection' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:112:0: 'NLA.RA20.generic_count_three' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:114:0: 'NLA.RA20.generic_count_not_four' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:116:0: 'NLA.RA20.not_criticalCountConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3497/3498] Built RegistryRecord (4.2s) Build completed successfully (3498 jobs).