---
title: "Convex Distance Operator Transport (nPC7M7XLEv)"
emoji: 🎯
colorFrom: yellow
colorTo: red
sdk: static
pinned: false
tags:
 - trackio
 - trackio-logbook
 - open-experiment
 - icml2026-repro
 - paper-nPC7M7XLEv
---

# CDOT reproduction — Lean kernel verification added

The previous live score is **9/12** at revision `e7c9bd313c5bc8f5d252f0f5ac2dce3e087ba032`. This
additive candidate addresses the only remaining deductions—Claims 1, 2, and
6—with pinned Lean 4.19.0/mathlib kernel checks, an independent replay, and a
false-theorem negative control. It is a forecasted improvement, not a new
judge score.

Open the logbook at **CURRENT — CDOT kernel-checked claim reproduction**.
Every file from the 9/12 revision remains preserved; the rejected human-only
theoretical pages are reachable under **Historical rejected baseline**.