TR-14: exact ordinary and symmetric ranks of all complex Hankel tensors

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-width Target, retaining arbitrary mode-dependent ordinary factors, zero and exceptional data. Independent fresh shared/canonical audits and strict actual Linux proof-commit verification pass.

Claims

LEAN VERIFIED OP-00211 — Comon's exact-rank conjecture for Hankel tensors

Full resolution · statement matched the canonical formalisation

Files and sources

Paper: OpenProblemsInNLA @ 099805e, TR-14/lean/ ↗
Lean bundle: submissions/bundles/openproblemsinnla-tr-14-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:07:56.150917

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.TR14.Target. The result is only as faithful as those definitions.
NLA.TR14.target

Declarations audited

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

NLA.TR14.target

NLA.Statements.TR14.Target

RegistryProblems.Problem_OP_00211

Prop

Build log

assical.choice, Quot.sound]
ℹ [3461/3479] Built NLA.Proofs.TR14.TR14BinaryUpper (7.8s)
info: NLA/Proofs/TR14/TR14BinaryUpper.lean:30:0: 'NLA.Proofs.TR14.binary_symmetricWidth_of_minimal_monic' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3462/3479] Built NLA.Proofs.TR14.UnitTransformation (5.4s)
info: NLA/Proofs/TR14/UnitTransformation.lean:32:0: 'NLA.Proofs.TR14.linearTransformation_unit' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3463/3479] Built NLA.Proofs.TR14.ContextualReduced (6.1s)
info: NLA/Proofs/TR14/ContextualReduced.lean:85:0: 'NLA.Proofs.TR14.nilpotent_eq_zero_of_context' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/TR14/ContextualReduced.lean:86:0: 'NLA.Proofs.TR14.auxiliarySubalgebra_isReduced_of_context' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3464/3482] Built NLA.Proofs.TR14.LocalCRTRootData (7.9s)
info: NLA/Proofs/TR14/LocalCRTRootData.lean:103:0: 'NLA.Proofs.TR14.localRoot_factorization' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3465/3483] Built NLA.Proofs.TR14.ReducedSubalgebras (8.9s)
info: NLA/Proofs/TR14/ReducedSubalgebras.lean:141:0: 'NLA.Proofs.TR14.finite_reducedSubalgebras_of_finiteDimensional' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [3466/3483] Built NLA.Proofs.TR14.ContextualProductStep (8.8s)
info: NLA/Proofs/TR14/ContextualProductStep.lean:90:0: 'NLA.Proofs.TR14.contextual_product_step_of_finite_reduced' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3467/3483] Built NLA.Proofs.TR14.LocalCRTShift (8.2s)
info: NLA/Proofs/TR14/LocalCRTShift.lean:96:0: 'NLA.Proofs.TR14.localShiftEquiv_root' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3468/3483] Built NLA.Proofs.TR14.CyclicSpanDimension (8.0s)
info: NLA/Proofs/TR14/CyclicSpanDimension.lean:118:0: 'NLA.Proofs.TR14.cyclicPrefix_finrank' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3469/3483] Built NLA.Proofs.TR14.ScalarGraphSeparation (7.8s)
info: NLA/Proofs/TR14/ScalarGraphSeparation.lean:54:0: 'NLA.Proofs.TR14.stabilizer_fst_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3470/3483] Built NLA.Proofs.TR14.ContextualProduct (7.9s)
info: NLA/Proofs/TR14/ContextualProduct.lean:30:0: 'NLA.Proofs.TR14.contextual_product_step' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3471/3483] Built NLA.Proofs.TR14.LocalCRTAlgebra (8.1s)
info: NLA/Proofs/TR14/LocalCRTAlgebra.lean:123:0: 'NLA.Proofs.TR14.localCRTEquiv_root' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3472/3486] Built NLA.Proofs.TR14.BlockPolynomialImage (8.4s)
info: NLA/Proofs/TR14/BlockPolynomialImage.lean:120:0: 'NLA.Proofs.TR14.blockModeLinear_finrank_range' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3473/3487] Built NLA.Proofs.TR14.ContextualIteration (10s)
info: NLA/Proofs/TR14/ContextualIteration.lean:122:0: 'NLA.Proofs.TR14.contextual_product_list_dimension_bound_of_stabilizer_finrank_le_one' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
ℹ [3474/3487] Built NLA.Proofs.TR14.LocalCRTFunctional (8.8s)
info: NLA/Proofs/TR14/LocalCRTFunctional.lean:102:0: 'NLA.Proofs.TR14.localCRTComponent_frobenius' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3475/3488] Built NLA.Proofs.TR14.ReducedPrimitiveBlocks (9.0s)
info: NLA/Proofs/TR14/ReducedPrimitiveBlocks.lean:119:0: 'NLA.Proofs.TR14.reduced_complex_exists_equiv_fin' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/TR14/ReducedPrimitiveBlocks.lean:120:0: 'NLA.Proofs.TR14.reducedBlockIdempotent_scalar_action' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3476/3490] Built NLA.Proofs.TR14.CornerContext (10s)
info: NLA/Proofs/TR14/CornerContext.lean:185:0: 'NLA.Proofs.TR14.cornerBlockFunctional_frobenius' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3477/3490] Built NLA.Proofs.TR14.LocalCRTMoments (8.6s)
info: NLA/Proofs/TR14/LocalCRTMoments.lean:83:0: 'NLA.Proofs.TR14.localCRT_hankel_of_apolar' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3478/3494] Built NLA.Proofs.TR14.OrthogonalBlockDimensions (8.2s)
info: NLA/Proofs/TR14/OrthogonalBlockDimensions.lean:95:0: 'NLA.Proofs.TR14.orthogonalBlockEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/TR14/OrthogonalBlockDimensions.lean:96:0: 'NLA.Proofs.TR14.sum_finrank_mapped_reducedBlocks' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3479/3494] Built NLA.Proofs.TR14.LocalBlockSupport (8.3s)
info: NLA/Proofs/TR14/LocalBlockSupport.lean:124:0: 'NLA.Proofs.TR14.orthogonal_idempotent_card_le_rootSupport' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/TR14/LocalBlockSupport.lean:125:0: 'NLA.Proofs.TR14.blockIdeal_finrank_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3480/3494] Built NLA.Proofs.TR14.NumericalBlockLower (7.2s)
info: NLA/Proofs/TR14/NumericalBlockLower.lean:61:0: 'NLA.Proofs.TR14.numerical_block_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3481/3494] Built NLA.Proofs.TR14.CornerStabilizer (10s)
info: NLA/Proofs/TR14/CornerStabilizer.lean:95:0: 'NLA.Proofs.TR14.primitive_corner_stabilizer_finrank_le_one' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3482/3494] Built NLA.Proofs.TR14.GraphBlockModeDimension (10s)
info: NLA/Proofs/TR14/GraphBlockModeDimension.lean:104:0: 'NLA.Proofs.TR14.normalizedGraph_corner_mode_finrank_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3483/3494] Built NLA.Proofs.TR14.LocalCRTFourierSigma (8.0s)
info: NLA/Proofs/TR14/LocalCRTFourierSigma.lean:149:0: 'NLA.Proofs.TR14.localCRT_fourier_sigma_of_minimal' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3486/3497] Built NLA.Proofs.TR14.WidthPadding (7.3s)
info: NLA/Proofs/TR14/WidthPadding.lean:56:0: 'NLA.Proofs.TR14.symmetricWidth_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3487/3497] Built NLA.Proofs.TR14.LocalCRTFourierCount (9.0s)
info: NLA/Proofs/TR14/LocalCRTFourierCount.lean:72:0: 'NLA.Proofs.TR14.localCRTFourierNode_card_formula' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3489/3497] Built NLA.Proofs.TR14.CornerInheritance (11s)
info: NLA/Proofs/TR14/CornerInheritance.lean:163:0: 'NLA.Proofs.TR14.primitive_corner_block_dimension_inequality' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3490/3497] Built NLA.Proofs.TR14.LocalCRTFourierWidth (10s)
info: NLA/Proofs/TR14/LocalCRTFourierWidth.lean:69:0: 'NLA.Proofs.TR14.localCRTFourier_symmetricWidth_of_minimal' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3491/3497] Built NLA.Proofs.TR14.NormalizedOrdinaryLower (13s)
info: NLA/Proofs/TR14/NormalizedOrdinaryLower.lean:167:0: 'NLA.Proofs.TR14.ordinary_lower_of_minimal_monic_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/Proofs/TR14/NormalizedOrdinaryLower.lean:168:0: 'NLA.Proofs.TR14.ordinary_lower_of_minimal_monic' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3492/3497] Built NLA.Proofs.TR14.ChartLocalFourierWidth (5.5s)
info: NLA/Proofs/TR14/ChartLocalFourierWidth.lean:44:0: 'NLA.Proofs.TR14.chart_localCRTFourier_symmetricWidth' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3493/3497] Built NLA.Proofs.TR14.ChartUpperConstruction (4.6s)
info: NLA/Proofs/TR14/ChartUpperConstruction.lean:70:0: 'NLA.Proofs.TR14.exists_chart_two_symmetricWidths' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3494/3497] Built NLA.Proofs.TR14.Final (4.3s)
info: NLA/Proofs/TR14/Final.lean:55:0: 'NLA.Proofs.TR14.target' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3495/3497] Built Solution (4.5s)
info: Solution.lean:13:0: 'NLA.TR14.target' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3496/3497] Built RegistryRecord (4.2s)
Build completed successfully (3497 jobs).