Nonnegative H-eigenvalue inheritance from odd-order Hankel tensors
A real tensor $T$ of order $s$ and dimension $N$ is a Hankel tensor with generating vector $h = (h_0, h_1, \dots)$ if $T_{i_1 \cdots i_s} = h_{i_1 + \cdots + i_s - s}$ for all $i_1, \dots, i_s \in \{1, \dots, N\}$. H-eigenvalues are in Qi's sense: a real $\lambda$ is an H-eigenvalue of $T$ if some nonzero $x \in \mathbb{R}^N$ satisfies $\sum_{i_2, \dots, i_s} T_{i i_2 \cdots i_s} x_{i_2} \cdots x_{i_s} = \lambda x_i^{s-1}$ for every $i$. For odd $m \ge 3$, integers $q, n \ge 2$ and $h \in \mathbb{R}^{qm(n-1)+1}$, let $A$ be the Hankel tensor of order $m$ and dimension $q(n-1)+1$, and $B$ the Hankel tensor of order $qm$ and dimension $n$, both with generating vector $h$. Ding, Qi and Wei proved the corresponding implication for even lower order.
Problem. If $A$ has no negative H-eigenvalue, must $B$ have no negative H-eigenvalue, for every such $m$, $q$, $n$ and $h$?
Source: Ding, Qi and Wei (2017), the conjecture of Section 4 (third inheritance property); OpenProblemsInNLA states the case of odd lower order, which they leave open.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- SP
- Keywords
- Hankel tensors, H-eigenvalues, OpenProblemsInNLA
References
@article{ding2017,
author = {Ding, Weiyang and Qi, Liqun and Wei, Yimin},
title = {Inheritance properties and sum-of-squares decomposition of {H}ankel tensors: theory and algorithms},
journal = {BIT Numer. Math.},
volume = {57},
number = {1},
year = {2017},
pages = {169--190},
doi = {10.1007/s10543-016-0622-0},
eprint = {1505.02528},
archivePrefix = {arXiv},
}
@article{qi2005,
author = {Qi, Liqun},
title = {Eigenvalues of a real supersymmetric tensor},
journal = {J. Symbolic Comput.},
volume = {40},
number = {6},
year = {2005},
pages = {1302--1324},
doi = {10.1016/j.jsc.2005.05.007},
}
@misc{openproblemsinnla-tr15,
author = {Townsend, Alex},
title = {{TR-15}: Nonnegative H-eigenvalue inheritance from odd-order Hankel tensors},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/tensor-computations/TR-15/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00124.
namespace RegistryProblems.OP_00124
noncomputable section
open scoped BigOperators
/-- A real tensor with `s` slots, each of dimension `N`. -/
abbrev Tensor (s N : ℕ) := (Fin s → Fin N) → ℝ
/-- Sum of zero-based tensor indices as an actual index into the finite
generating vector. The proof establishes the bound, without a default value. -/
def generatorIndex {s N : ℕ} (indices : Fin s → Fin N) :
Fin (s * (N - 1) + 1) :=
⟨∑ j, (indices j).val, by
have hle : (∑ j : Fin s, (indices j).val) ≤ s * (N - 1) := by
calc
(∑ j : Fin s, (indices j).val) ≤ ∑ _j : Fin s, (N - 1) :=
Finset.sum_le_sum (fun j _ => Nat.le_sub_one_of_lt (indices j).isLt)
_ = s * (N - 1) := by simp
omega⟩
/-- Every entry is taken from the same finite generating vector. -/
def hankelTensor (s N : ℕ) (h : Fin (s * (N - 1) + 1) → ℝ) : Tensor s N :=
fun indices => h (generatorIndex indices)
/-- Prepend the uncontracted coordinate to the `s-1` contracted indices.
For positive order this is the usual tuple `(i, indices 0, …)`.
The total definition at order zero is never used by the conjecture. -/
def prependIndex {s N : ℕ} (i : Fin N) (indices : Fin (s - 1) → Fin N) :
Fin s → Fin N :=
fun j => if hj : j.val = 0 then i else
indices ⟨j.val - 1, by have := j.isLt; omega⟩
/-- The full H-eigenvalue contraction: sum over all ordered `(s-1)`-tuples,
with one factor of `x` for each contracted slot. There are no multinomial
weights because every ordered tuple appears separately. -/
def contraction {s N : ℕ} (T : Tensor s N) (x : Fin N → ℝ) : Fin N → ℝ :=
fun i => ∑ indices : Fin (s - 1) → Fin N,
T (prependIndex i indices) * ∏ j : Fin (s - 1), x (indices j)
/-- A genuine real H-eigenpair, including the nonzero-vector requirement. -/
def IsHEigenpair {s N : ℕ} (T : Tensor s N) (eigenvalue : ℝ)
(x : Fin N → ℝ) : Prop :=
x ≠ 0 ∧ ∀ i, contraction T x i = eigenvalue * x i ^ (s - 1)
/-- Every real H-eigenpair has a nonnegative real eigenvalue. This is exactly
the canonical absence of a negative real H-eigenvalue; existence is not assumed. -/
def HasNoNegativeHEigenvalues {s N : ℕ} (T : Tensor s N) : Prop :=
∀ (eigenvalue : ℝ) (x : Fin N → ℝ), IsHEigenpair T eigenvalue x →
0 ≤ eigenvalue
/-- The original lower tensor: order `m`, dimension `q*(n-1)+1`.
The finite cast only identifies the equal generating-vector lengths. -/
def lowerTensor (m q n : ℕ) (h : Fin (q * m * (n - 1) + 1) → ℝ) :
Tensor m (q * (n - 1) + 1) :=
hankelTensor m (q * (n - 1) + 1)
(fun i => h (Fin.cast (by simp [Nat.mul_comm, Nat.mul_assoc]) i))
/-- The original higher tensor: order `q*m`, dimension `n`, using exactly `h`. -/
def upperTensor (m q n : ℕ) (h : Fin (q * m * (n - 1) + 1) → ℝ) :
Tensor (q * m) n :=
hankelTensor (q * m) n h
/-- Every parameter restriction from the original conjecture. -/
def Admissible (m q n : ℕ) : Prop :=
Odd m ∧ 3 ≤ m ∧ 2 ≤ q ∧ 2 ≤ n
/-- OP-00124: Nonnegative H-eigenvalue inheritance from odd-order Hankel tensors -/
def _root_.RegistryProblems.Problem_OP_00124 : Prop :=
∀ (m q n : ℕ), Admissible m q n →
∀ h : Fin (q * m * (n - 1) + 1) → ℝ,
HasNoNegativeHEigenvalues (lowerTensor m q n h) →
HasNoNegativeHEigenvalues (upperTensor m q n h)
end
end RegistryProblems.OP_00124
Formalised by George Stepaniants (Apache-2.0); reviewed by clemens-admin.
Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.
Resolving this problem in Lean
Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.
In lakefile.toml:
[[require]] name = "RegistryProblems" git = "https://github.com/cthalhammer/registry-problems" rev = "753bebc58e3fee845f4fffec7d24e7c8cc2a689a"
In your proof:
import RegistryProblems.OP_00124 theorem resolution : RegistryProblems.Problem_OP_00124 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00124" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00124 := by sorry
You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.
Resolution claims
Formalizes the full negative answer to the canonical inheritance conjecture with actual ordered tensor contractions, real nonzero H-eigenpairs, universal lower positivity, an explicit upper negative pair and unconditional lower-pair existence from the intermediate value theorem.
Take $m=3$, $q=2$, $n=2$ and the common generating vector $h=(2,0,1,0,2,0,-1)$, and let $A$ be the order-three, dimension-three Hankel tensor and $B$ the order-six, dimension-two Hankel tensor it generates. The first component of $Ax^2$ equals $(x_1+x_3)^2+x_1^2+x_2^2+x_3^2$, which is positive for every nonzero real $x$, so every real H-eigenvalue of $A$ is strictly positive. For $v=(0,1)$ one has $Bv^5=(h_5,h_6)=(0,-1)$, so $-1$ is …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, TR-15/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00124, "Nonnegative H-eigenvalue inheritance from odd-order Hankel tensors", clopen.solutions.