Alignment Workspace

Item 52: Import the Cartesian-frames definitions and delete the mirror

Deference line · difficulty entry · project deference · open · node item-52

lean/Workspace/Deference/Contrib/CartesianFrameBridge.lean mirrors about two hundred lines of the upstream CartesianFrames/ library, because the round that needed it was dispatched while that library was on an unmerged upstream branch and the pin could not reach it. The pin is now c0d885bf, a commit on the upstream default branch that carries CartesianFrames/, so the mirror is a second definition of objects the trust chain already supplies.

The item is to import the authoritative definitions, delete the mirror, and check that every result the bridge states still holds against them — which puts inside the lean gate the cross-check that round could only run by hand, and is the concrete value of doing it.

Deliverable shape: the existing declarations, unchanged in statement, over the upstream types. Acceptance check: the Lean gate is green, the axiom audit is clean, and CartesianFrameBridge.lean defines no frame type of its own. Context: prompts/2026-08-12-cartesian-frames/ and its artifacts/, which carry the hand-run cross-check and its re-verification command.


Deliverable shape: the existing declarations, unchanged in statement, over the upstream types.

Acceptance check: the Lean gate is green, the axiom audit is clean, and CartesianFrameBridge.lean defines no frame type of its own.

Context: prompts/2026-08-12-cartesian-frames/

Registered results bearing on this item

None registered.

Where it hangs

Rounds and decisions that touch it

None recorded.