Add Lean kernel verification for Claims 1 2 and 6

Activate current evaluator-visible claim package

Update logbook: Convex Distance Operator Transport (nPC7M7XLEv)

initial commit