OAI/Probability/SLE/Gauge/SerpentineMarkedRegion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The connector lies below the marked point, and every later part of the rightward serpentine lies strictly to its right. This is the geometric separation used to append the marked-point access hook.

  1. theorem OAI.SLEExactGauge.Serpentine.physicalFitChart_low_or_right line 14
  2. theorem OAI.SLEExactGauge.Serpentine.physicalFitChart_marked_distance line 27
  3. theorem OAI.SLEExactGauge.Serpentine.physicalFitChart_hook_region line 42