On the minimal dimension of range-criterion counterexamples to the PPT² conjecture

The PPT² conjecture asserts that the composition of two completely positive and completely copositive (PPT) maps is entanglement breaking. A recently announced counterexample is a range-criterion pair: PPT maps M₁₀ → M₆ → M₁₀ whose composite Choi matrix has no nonzero product vector in its range, so the range criterion certifies its entanglement. We ask how small such a pair can be. For PPT maps Φ: Mₘ → Mₖ and Ψ: Mₖ → Mₙ with Ψ ∘ Φ ≠ 0 and max(m, k, n) ≤ 6, we prove, by rank bounds, Chern class and excess intersection computations, and computer-assisted steps, that the range of the Choi matrix of Ψ ∘ Φ contains a nonzero product vector whenever k ≤ 5 or min(m, n) ≤ 5. Hence no counterexample on M₄ or M₅ can be certified in this way, and among the types (m, k, n) with all dimensions at most six, only (6, 6, 6) with restricted Choi ranks remains open. For m = n = 4 the range contains a nonzero product vector for every k, and no range-criterion pair has type (4, 6, d), (6, 4, d), (d, 6, 4) or (d, 4, 6) with d ≤ 9. The computed facts are checked in Lean 4, modulo classical, quoted or hand-proved inputs. Lean also derives the main theorem from nine algebro-geometric steps proved in the paper, taken as hypotheses. The announced counterexample lifts a map on M₄ through exterior powers. If a map loses rank transversally at finitely many points, its Schur-functor lifts (with nonzero composite) put product vectors into the kernel of the composite Choi matrix that form an unextendible product set only for exterior powers, and then one of the three dimensions is at least ten. Another lift is a range-criterion pair of type (6, 10, 10). Finally, symmetry under a compact connected group acting irreducibly on both outer spaces puts a product vector into the composite range; the conjecture holds in several covariant classes. Version 5 has a new abstract and corrects the introduction. The introduction now says that the types of Proposition 4.24 are excluded for every certificate, not only for those with an unextendible product set, and that no range-criterion pair has type (4,6,n), (6,4,n), (n,6,4) or (n,4,6) with n ≤ 9. Its paraphrase of Lemma 4.19 restores the hypothesis that the product vector is in the kernel, and several terms are defined at first use. Section 4 defines more of the symbols it takes from the supplement; the wording of open problems (2), (3) and (5) is corrected. Lettered subsections and statements are marked as new in version 4, and the code pointers cite version 4 of the software. No statement, proof or numbering has changed. Mathematics Subject Classification (2020): 81P40; 15A69, 14M15, 14C17, 47L07.