Manuscript Oai272-A@1 · Oai272-A.tex · section · a40828a0
Deferred successors
Stage 6: the single active certificate and the exact handoff › Deferred successors · lines 2100–2136
| Candidate | Missing interface or correction |
|---|---|
| Candidate | Missing interface or correction |
| Lean proof of the zero-key theorem | A faithful formal model of instruments, complete histories, matrix-valued measures, ideal keys, and the operational quantifiers. The inspected pair/channel targets do not supply it and contain proof placeholders. |
| Dimension reduction | New maps or channels with complete positivity, range, and normalization certificates. No minimality conclusion is inherited. |
| Efficient witness production | Theorem thm:witness-algorithm supplies finite termination under an exact support promise, not an efficient complexity bound or an executed Family 272 witness. |
| One-way/two-way comparison | Both rates are already zero conditional on the same universal obstruction. A different finite-block optimum or assisted resource task must be specified to obtain a nontrivial new comparison. |
| Failure of eventual entanglement breaking | Does not follow from square failure. It would require a separate claim confronting the stated eventual-breaking theorem in Park. |