The definable Lebesgue measure conjecture for the unit interval

Let $\mathbb{K}$ be a definably complete expansion of an ordered field, and let $\mu$ be the outer measure defined by infima of sums of lengths of definable open-interval covers indexed by definable closed discrete sets. Then the definable Lebesgue measure conjecture.

$$\mu((0,1))=1.$$

This asserts that the definable outer measure of the unit interval agrees with its expected Lebesgue measure; it is automatic in expansions of the real field with the natural numbers and is proved later in the paper when $\mathbb{K}$ is unrestrained.