RootExteriorFlux.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Positivity of the signed boundary area for the actual exterior root map. Compact omitted sets and the ordinary area change of variables supply the sign, without a boundary regularity assumption at radius one.

lemma OAI.SLEExactGauge.root_exterior_flux_nonneg line 16