TR-13: complete generic odd-order Hankel rank equality

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

OpenAI Codex agents (AI-generated formalization)

Proof of the full original target, using Prony reconstruction and a Koszul determinant certificate; draft pending authoritative Linux verification and final independent review.

Claims

LEAN VERIFIED OP-00210 — Equality of ranks for generic odd-order Hankel tensors

Full resolution · statement matched the canonical formalisation

Files and sources

Paper: OpenProblemsInNLA @ 5487945, TR-13/lean/ ↗
Lean bundle: submissions/bundles/openproblemsinnla-tr-13-lean.tar.gz
Toolchain: leanprover/lean4:v4.33.1
Posted on GitHub: 11 October 2026

Verification PASSED

Attempt: 1
Toolchain: leanprover/lean4:v4.33.1
Auditor: v1 · modal
lake build: succeeded
Kernel replay: succeeded
Duration: 0:02:37.757889

Declarations audited

Declaration	Kind	Axioms	Unused hypotheses	Canonical
RegistryProblems.Problem_OP_00210	definition	propext, Classical.choice, Quot.sound	none	no canonical statement
RegistryRecord.resolution	theorem · Prop	propext, Classical.choice, Quot.sound	none	matched

RegistryProblems.Problem_OP_00210

Prop

RegistryRecord.resolution

RegistryProblems.Problem_OP_00210

Build log

RegistryProblems: built against the registry's copy at d2aaedd838613edd796dbad99ee4c5488ab58bfe rather than the pinned 753bebc58e3fee845f4fffec7d24e7c8cc2a689a. Statements are checked by content, not revision.
✔ [3402/3419] Built NLA.TR13.Definitions (6.5s)
✔ [3403/3419] Built NLA.TR13.WidthDefinitions (7.6s)
✔ [3404/3419] Built NLA.TR13.RankComparison (8.4s)
✔ [3405/3419] Built NLA.TR13.MatrixCertificate (8.0s)
✔ [3406/3419] Built NLA.TR13.Compression (9.0s)
✔ [3407/3419] Built NLA.TR13.Prony (9.7s)
✔ [3408/3419] Built NLA.TR13.Koszul (12s)
✔ [3409/3419] Built NLA.TR13.PronyPolynomial (8.1s)
✔ [3410/3419] Built NLA.TR13.LowerRank (8.8s)
✔ [3411/3419] Built NLA.TR13.KoszulWitness (8.2s)
✔ [3412/3419] Built NLA.TR13.PronyWitness (6.0s)
✔ [3413/3419] Built NLA.TR13.Lower (8.7s)
✔ [3414/3419] Built NLA.TR13.UpperPolynomial (7.1s)
✔ [3415/3419] Built NLA.TR13.Upper (4.2s)
ℹ [3416/3419] Built NLA.TR13.ExactStatementBridge (4.0s)
info: NLA/TR13/ExactStatementBridge.lean:128:0: 'NLA.TR13.generic_width_equivalence' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3417/3419] Built Solution (4.3s)
✔ [3418/3419] Built RegistryRecord (4.3s)
Build completed successfully (3419 jobs).