OAI/Probability/SLE/Gauge/RibbonPrefixTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A successful narrow physical prefix is preserved by the exact SLE spatial/capacity scaling. The front is transported as its actual first hit, not chosen as a separate completion certificate.

  1. lemma OAI.SLEExactGauge.scalePath_at_scaled_time line 17
  2. theorem OAI.SLEExactGauge.goodRibbonPrefix_scalePath line 22