# Exact Hausdorff gauges for SLE

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [An exact Hausdorff gauge for SLE: A moment-integral and finite-batch construction](../../preprints/An-exact-Hausdorff-gauge-for-SLE-September-25-2026/An-exact-Hausdorff-gauge-for-SLE-September-25-2026.pdf)
- [An explicit exact Hausdorff gauge for SLE: A regular formula from quantitative tails and dense visits](../../preprints/An-explicit-exact-Hausdorff-gauge-for-SLE-September-26-2026/An-explicit-exact-Hausdorff-gauge-for-SLE-September-26-2026.pdf)

## Scope

For $0<\kappa<8$, put $d=1+\kappa/8$. The formalization proves that every continuous nondecreasing Hausdorff gauge agreeing with $h(r)=r^d(\log\log(1/r))^{(2-d)/2}$ at sufficiently small positive radii almost surely assigns positive measure to every nontrivial compact positive-time segment of ordinary chordal $\mathrm{SLE}_\kappa$.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Positivity of the explicit gauge on every positive-time segment | [SLELowerPositivity.lean](../ComparatorChallenges/SLELowerPositivity.lean) |