Corrections established by source inspection

The following distinctions were checked against the publicly accessible source files on 14 October 2026.

scope versus proof. The scope note lists a dimension-ten pair target and a dimension-twenty-one channel target, and expressly excludes the zero-key theorem LeanScope. More strongly, the inspected files end the relevant theorem bodies with by sorry:

LeanPair,LeanChannel. They specify targets; those bodies are not completed proofs. No Lean execution or independent checking of other repository files is asserted.

arithmetic roles. The dimension-ten argument uses its own algebraic and arithmetic certificate. The supplementary integer programs described in the paper concern the separate projection/combinatorial construction. Their scope does not include all geometric, operational, or nonseparability arguments, and they do not instantiate that construction's large global matrices Supplementary272.

sizes. A Choi matrix for a map $M_{10}(\mathbb{C})\to M_{10}(\mathbb{C})$ is $100\times 100$. For $M_{21}(\mathbb{C})\to M_{21}(\mathbb{C})$, it is $441\times 441$. The phrase “enormous global matrices” in the supplementary-check discussion must not be silently transferred to identify the dimension-ten Choi matrix with the separate large combinatorial objects.

entanglement breaking. Park's preprint, first submitted on 13 August 2026, states eventual entanglement breaking for every finite-dimensional PPT endomap, with a map-dependent iterate Park. We do not independently verify that preprint. Nevertheless, a proposal that a PPT channel never becomes entanglement breaking would need to confront that stated theorem; it is not a consequence of a second-iterate counterexample. Earlier results established important eventual-breaking cases HansonRouzeFranca.