The labelled-WQO lifting gap

Exact statement

It is not established here that WQO for finite substructures labelled by $\mathbb N$ implies the $\mathbb N\times\mathbb N$ -labelled WQO used by the core equivariant Gröbner computation, still less the all-WQO-label condition of nicely orderable actions.

StatusUnresolved under the stated weaker hypothesis set

External reviewNo documented external or specialist review of this FPRD exposition is recorded.

Context

A second label coordinate tracks support or colour information needed to turn a weak equivariant basis into a full one.

Proof or evidence

The 2025 proof explicitly uses a product-labelled WQO. The inspected papers do not prove that the weaker natural-number-labelled WQO implies it in this generality.

The remaining implication →

Verification notes

No abstract WQO assumption was silently promoted to effectiveness or to arbitrary label sets.

Limitations

Failure to find an implication is not a proof that it is false.
Additional effective structure may close the gap.

Open work

Prove the lifting for homogeneous ordered finite-signature structures or specialize the algorithm to binomial ideals.