MF-14: degree44 closure coverage refutes the original seven-product degree42 equality
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Seven chronological products cover every complex polynomial through degree 44 in the full 129-coefficient closure model, refuting the original equality 42. The later exact maximum 47 is outside this formalization. Local serial Lean, two nonauthor final reviews and two published-source Linux verification runs pass.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, MF-14/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-mf-14-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:16:05.934461
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.MF14Degree44.original_equality_false | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00094 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.MF14Degree44.original_equality_false
Not (IsGreatest NLA.MF14.coveredDegrees 42)
RegistryProblems.Problem_OP_00094
Prop
Build log
] info: NLA/MF14Degree44/Mod3Rows6.lean:34:0: 'NLA.MF14Degree44.Mod3Certificate.natural_inverse_row_32' depends on axioms: [propext] info: NLA/MF14Degree44/Mod3Rows6.lean:43:0: 'NLA.MF14Degree44.Mod3Certificate.natural_inverse_row_33' depends on axioms: [propext] info: NLA/MF14Degree44/Mod3Rows6.lean:52:0: 'NLA.MF14Degree44.Mod3Certificate.natural_inverse_row_34' depends on axioms: [propext] ℹ [3715/3724] Built NLA.MF14Degree44.Mod3Rows7 (35s) info: NLA/MF14Degree44/Mod3Rows7.lean:16:0: 'NLA.MF14Degree44.Mod3Certificate.natural_inverse_row_35' depends on axioms: [propext] info: NLA/MF14Degree44/Mod3Rows7.lean:25:0: 'NLA.MF14Degree44.Mod3Certificate.natural_inverse_row_36' depends on axioms: [propext] info: NLA/MF14Degree44/Mod3Rows7.lean:34:0: 'NLA.MF14Degree44.Mod3Certificate.natural_inverse_row_37' depends on axioms: [propext] info: NLA/MF14Degree44/Mod3Rows7.lean:43:0: 'NLA.MF14Degree44.Mod3Certificate.natural_inverse_row_38' depends on axioms: [propext] info: NLA/MF14Degree44/Mod3Rows7.lean:52:0: 'NLA.MF14Degree44.Mod3Certificate.natural_inverse_row_39' depends on axioms: [propext] ℹ [3717/3727] Built NLA.MF14Degree44.Mod3CastBridge (8.8s) info: NLA/MF14Degree44/Mod3CastBridge.lean:26:0: 'NLA.MF14Degree44.Mod3Certificate.product_entry_cast' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF14Degree44/Mod3CastBridge.lean:28:0: 'NLA.MF14Degree44.Mod3Certificate.matrix_entry_of_natural_residue' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3720/3727] Built NLA.MF14Degree44.Mod3Rows8 (24s) info: NLA/MF14Degree44/Mod3Rows8.lean:16:0: 'NLA.MF14Degree44.Mod3Certificate.natural_inverse_row_40' depends on axioms: [propext] info: NLA/MF14Degree44/Mod3Rows8.lean:25:0: 'NLA.MF14Degree44.Mod3Certificate.natural_inverse_row_41' depends on axioms: [propext] info: NLA/MF14Degree44/Mod3Rows8.lean:34:0: 'NLA.MF14Degree44.Mod3Certificate.natural_inverse_row_42' depends on axioms: [propext] info: NLA/MF14Degree44/Mod3Rows8.lean:43:0: 'NLA.MF14Degree44.Mod3Certificate.natural_inverse_row_43' depends on axioms: [propext] info: NLA/MF14Degree44/Mod3Rows8.lean:52:0: 'NLA.MF14Degree44.Mod3Certificate.natural_inverse_row_44' depends on axioms: [propext] ℹ [3721/3727] Built NLA.MF14Degree44.Mod3Certificate (7.2s) info: NLA/MF14Degree44/Mod3Certificate.lean:149:0: 'NLA.MF14Degree44.integerJacobian_eq_checked_table' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF14Degree44/Mod3Certificate.lean:151:0: 'NLA.MF14Degree44.mod3_checked_table_inverse' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF14Degree44/Mod3Certificate.lean:153:0: 'NLA.MF14Degree44.integerJacobianMod3_eq_checked_table' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF14Degree44/Mod3Certificate.lean:155:0: 'NLA.MF14Degree44.integer_jacobian_mod3_inverse' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3722/3727] Built NLA.MF14Degree44.JacobianNonzero (7.4s) info: NLA/MF14Degree44/JacobianNonzero.lean:39:0: 'NLA.MF14Degree44.integer_jacobian_det_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF14Degree44/JacobianNonzero.lean:41:0: 'NLA.MF14Degree44.complex_integer_jacobian_det_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3723/3727] Built NLA.MF14Degree44.JacobianIdentity (6.7s) info: NLA/MF14Degree44/JacobianIdentity.lean:36:0: 'NLA.MF14Degree44.coefficient_jacobian_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF14Degree44/JacobianIdentity.lean:38:0: 'NLA.MF14Degree44.coefficient_derivative_bijective' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3724/3727] Built NLA.MF14Degree44.FinalClosure (7.6s) info: NLA/MF14Degree44/FinalClosure.lean:70:0: 'NLA.MF14Degree44.quad_reconstruction_of_degree' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF14Degree44/FinalClosure.lean:72:0: 'NLA.MF14Degree44.border_quad_natDegree' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF14Degree44/FinalClosure.lean:74:0: 'NLA.MF14Degree44.monic_border_joint_closure' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF14Degree44/FinalClosure.lean:76:0: 'NLA.MF14Degree44.family_image_mem_closure' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF14Degree44/FinalClosure.lean:78:0: 'NLA.MF14Degree44.degree44_coverage' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/MF14Degree44/FinalClosure.lean:80:0: 'NLA.MF14Degree44.original_equality_false' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3725/3727] Built Solution (6.2s) info: Solution.lean:12:0: 'NLA.MF14Degree44.canonical_gate_padding' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:15:0: 'NLA.MF14Degree44.four_prefix_full_coefficients' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:18:0: 'NLA.MF14Degree44.three_product_tuple' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:21:0: 'NLA.MF14Degree44.good_border_parameters_eventually' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:24:0: 'NLA.MF14Degree44.fourth_span_coordinates' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:27:0: 'NLA.MF14Degree44.fourth_map_smooth' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:30:0: 'NLA.MF14Degree44.fourth_jacobian_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:33:0: 'NLA.MF14Degree44.fourth_minor_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:36:0: 'NLA.MF14Degree44.fourth_product_joint_closure' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:39:0: 'NLA.MF14Degree44.polynomial_density_of_strict_derivative' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:42:0: 'NLA.MF14Degree44.degeneration_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:45:0: 'NLA.MF14Degree44.degeneration_at_zero' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:48:0: 'NLA.MF14Degree44.degeneration_in_span' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:51:0: 'NLA.MF14Degree44.monic_border_joint_closure' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:54:0: 'NLA.MF14Degree44.continuation_actual_output' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:57:0: 'NLA.MF14Degree44.continuation_degree_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:60:0: 'NLA.MF14Degree44.continuation_closure_transfer' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:63:0: 'NLA.MF14Degree44.family_image_mem_closure' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:66:0: 'NLA.MF14Degree44.family_degree_and_full_vector' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:69:0: 'NLA.MF14Degree44.coefficient_map_smooth' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:72:0: 'NLA.MF14Degree44.coefficient_jacobian_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:75:0: 'NLA.MF14Degree44.integer_jacobian_mod3_inverse' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:78:0: 'NLA.MF14Degree44.coefficient_derivative_bijective' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:81:0: 'NLA.MF14Degree44.degree44_coverage' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:84:0: 'NLA.MF14Degree44.original_equality_false' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3726/3727] Built RegistryRecord (7.0s) Build completed successfully (3727 jobs).