Section 15.4 optimality proof
This module is the reader-facing entry point for the legal-trace coupling proof of farthest-in-future optimality. The trace submodule packages the six proof layers from policy semantics through finite exchange iteration.
Implementation details: