Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Cofactor completeness of nonnegative kernels

Abstract

Every finite real nonnegative kernel is generated by oriented cofactor vectors from row minors of the appropriate support size.

Definition 1.1 (Zero extension of signed cofactors).

Formalization. D5/S3/Quantum/Entanglement/AbsolutePPT/NonnegativeKernelCofactor.liftCof (✓ std3).

Source. Repository-derived.

Commentary.

Choose k rows and k+1 columns by embeddings. Take the signed cofactors of that rectangular submatrix and extend them by zero to the ambient coordinate type. Cofactor j is exactly (-1) to the natural value of j times the determinant after deleting column j with succAbove. No order on the ambient finite coordinate type is required.

Definition 1.2 (Qualifying cofactor vectors).

Formalization. D5/S3/Quantum/Entanglement/AbsolutePPT/NonnegativeKernelCofactor.cofactorCandidates (✓ std3).

Source. Repository-derived.

Commentary.

For each k at most the number of original rows, select k rows, k+1 columns and one of the two signs. Retain exactly the nonzero zero-extended vectors that are nonnegative and satisfy every original row equation. The full-kernel filter is essential when fewer rows are selected. The parameter families are finite, but this theorem does not enumerate or count their distinct rays.

Theorem 1.3 (Every circuit has a cofactor representative).

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/NonnegativeKernelCofactor.circuit_cofactor_complete (✓ std3). ∎

Source. Repository-derived.

Commentary.

The compiled declaration retains arbitrary finite J with its Fintype instance, arbitrary m, the full real matrix B and vector v, the Circuit witness, and every existential witness and conjunct in the result: row and column embeddings, orientation, positive scale, support equality, nonzero cofactor, all original row equations, nonzero zero-extended vector, and exact proportionality. A circuit with support size k+1 is a strictly positive multiple of an oriented cofactor vector with the same support. Deleting one supported column leaves independent columns. The restricted matrix has rank k: those deleted columns give the lower bound, while its strictly positive kernel vector and rank-nullity give the upper bound. A basis selected from its rows yields a nonzero k by k minor. Apply CofactorKernel.kernel_cross_identity to the strictly positive restricted vector. Its positive coordinate sum and the nonzero cofactor force a nonzero augmented determinant, determine one of the two orientations, and give positive proportionality at every coordinate. This is the classical finite-dimensional elementary-vector/cofactor argument. Zero extension reconstructs the original vector. Dividing the full original row equations by the positive factor proves full kernel membership of the cofactor representative.

No nonempty ambient coordinate type, positive row count, full row rank or sign restriction on matrix entries is assumed. A circuit itself has nonempty support. For support one, k is zero and the empty minor has determinant one. With no rows or an all-zero matrix, singleton circuits are included. Dependent and zero rows require no padding.

Theorem 1.4 (Exact cone characterization).

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/NonnegativeKernelCofactor.nonnegKernel_iff_mem_hull_cofactorCandidates (✓ std3). ∎

Source. Repository-derived.

Commentary.

A vector is a nonnegative solution of all original equations if and only if it belongs to the pointed conic hull of qualifying cofactor vectors. The forward implication consumes the existing circuit decomposition and replaces each circuit by its positive multiple of a qualifying cofactor vector. The reverse implication uses closure of the full nonnegative kernel under addition and nonnegative scaling. Zero belongs to the hull even when the coordinate type and candidate set are empty. No second support-descent argument is used.

For three equations, the theorem includes row selections of sizes zero through three and supports of sizes one through four. Using only cofactors of all three rows can miss degenerate circuits. To certify a particular finite list, every qualifying candidate must be shown positively proportional to an entry of that list, with column and row reorderings accounted for under this sign convention. No completeness or count certificate for a list of 187 rays is asserted here, and no final APPT purity claim follows without that additional consumer and the exact slack and spectrum reconstruction.

References