The recorded solution establishes the requested Karp reduction and recovers a source assignment from any valid target factor pair. Its mathematical correctness has a complete Lean proof; the forward map’s polynomial runtime and output size are established by a written analysis of the construction.
The construction encodes the formula as a weighted cut instance, then builds a positive rational matrix by perturbing the identity and a constant matrix with the cut weights. A satisfying assignment supplies an accepted two-component factorization. Conversely, the stability theorem forces every accepted product close to a matrix with two blocks; thresholding its first row recovers the cut and then a satisfying assignment. The output has O(s²) entries of O(log(s + 2)) bits each for source length s. This establishes hardness of exact error thresholds, without a constant-factor inapproximability claim.
Why this question matters
Nonnegative matrix factorization represents nonnegative data using a small number of nonnegative components. Fixing that number to two gives the first nontrivial approximation case. Establishing hardness here would show that even this small model can resist polynomial-time exact global optimization.
Lindy, Noferini and Van Dooren identify the hardness of rank-two nonnegative approximation as open. Exact factorization of rank-two data does not settle this question: the input here may have arbitrary rank, and the objective allows nonzero approximation error. The earlier hardness result of Gillis and Glineur permits negative input entries, so it does not establish hardness for nonnegative data.
The reduction to construct
The starting point is 3-SAT: given a Boolean formula with at most three literals per clause, decide whether a satisfying assignment exists.
The target instance consists of an m × n nonnegative rational matrix X and a nonnegative rational threshold τ, both encoded in binary. It asks whether nonnegative real matrices W of size m × 2 and H of size 2 × n satisfy the error bound below. The factors may be asymmetric and need not have rational entries.
The goal is a deterministic polynomial-time map from a 3-SAT formula to a target instance, such that the formula is satisfiable if and only if the target error bound is attainable. The requested complexity conclusion is NP-hardness for the stated target problem.
The difficult direction is excluding unintended low-error factorizations when the formula is unsatisfiable. Constructing factors from a satisfying assignment addresses only the easier direction: soundness must control every nonnegative real factor pair, including asymmetric and nonoptimal ones, while retaining a rational threshold gap.
What a complete answer must include
A complete answer must specify that map, prove both implications for every source instance, and bound its runtime and output encoding length. The research deliverable also includes an explicit algorithm that recovers a satisfying assignment from every valid target witness, with its witness encoding and correctness argument.
Literature checked 2026-09-16. This summarizes the archived bounded audit. Unindexed and unpublished work and complete citation descendants remain outside coverage; expert priority assessment is outstanding.
