CanonicalTraceDischarge.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A capacity-two SLE presentation gives a canonical trace on its continuous-driver law through the raw inverse-flow witness.

theorem OAI.SLEExactGauge.canonical_driver_trace_generation_of_witness line 20