[proofplan] The proof is a black-box application of the standard interior regularity theory for area-minimizing integral currents. First, Almgren's big [regularity theorem](/theorems/2750) gives the general codimension estimate $\dim_{\mathcal H}(\operatorname{sing} T) \le m-2$ for an area-minimizing integral $m$-current with no interior boundary. In codimension one, Federer dimension reduction improves the estimate by reducing any large singular stratum to a non-flat area-minimizing hypersurface cone in low dimension; the classification and nonexistence of such cones below dimension $7$ gives the bound $m-7$ and emptiness for $m \le 6$. [/proofplan] [step:Apply Almgren regularity to obtain the general codimension two bound] Let $S := \operatorname{sing} T \subset \operatorname{spt} T \cap U$ denote the interior singular set of $T$, namely the set of points at which $\operatorname{spt} T$ is not locally a smooth embedded $m$-dimensional submanifold with integer multiplicity. Since $T$ is an area-minimizing integral $m$-current in $U$ and $\partial T = 0$ in $U$, the hypotheses of Almgren's interior regularity theorem for area-minimizing integral currents apply. That theorem states that the interior singular set of such a current has Hausdorff dimension at most $m-2$. Therefore \begin{align*} \dim_{\mathcal H}(S) \le m-2. \end{align*} This proves the first asserted estimate. [guided] We first isolate the set whose size must be estimated. Define $S := \operatorname{sing} T \subset \operatorname{spt} T \cap U$ to be the interior singular set: a point $x \in \operatorname{spt} T \cap U$ lies in $S$ exactly when $\operatorname{spt} T$ is not locally, near $x$, a smooth embedded $m$-dimensional submanifold carrying an integer multiplicity. The relevant black-box theorem is Almgren's interior regularity theorem for area-minimizing integral currents. Its hypotheses are precisely the following local assumptions: the current is integral, it is $m$-dimensional, it is area-minimizing against compactly supported competitors in the [open set](/page/Open%20Set), and it has no boundary in the interior. These are satisfied here because $T$ is an area-minimizing integral $m$-current in $U$ and $\partial T = 0$ in $U$. Almgren's theorem then gives the Hausdorff dimension estimate \begin{align*} \dim_{\mathcal H}(\operatorname{sing} T) \le m-2. \end{align*} Since $S$ was defined to be $\operatorname{sing} T$, this is exactly \begin{align*} \dim_{\mathcal H}(S) \le m-2. \end{align*} This proves the general codimension-two estimate. [/guided] [/step] [step:Use Federer dimension reduction in codimension one] Assume now that $n=m+1$. By the tangent-cone existence theorem for area-minimizing integral currents, every point $x \in S$ has at least one tangent cone $C_x$, obtained as a flat limit of rescalings of $T$ about $x$; moreover $C_x$ is an area-minimizing integral $m$-cone in $\mathbb R^{m+1}$. Federer's dimension-reduction theorem for area-minimizing hypersurfaces states that if $S$ had Hausdorff dimension greater than $m-7$, then one could produce a non-flat area-minimizing hypersurface cone in $\mathbb R^k$ with singularity at the origin for some $k \le 7$. The Simons-Federer classification of low-dimensional area-minimizing hypersurface cones states that no such non-flat singular area-minimizing hypersurface cone exists in dimensions $k \le 7$: every area-minimizing hypersurface cone in $\mathbb R^k$ with $k \le 7$ is a multiplicity-one hyperplane. This contradicts the cone produced by dimension reduction. Hence \begin{align*} \dim_{\mathcal H}(S) \le m-7. \end{align*} [/step] [step:Interpret the low-dimensional convention] When $m \le 6$, the inequality obtained in codimension one reads \begin{align*} \dim_{\mathcal H}(S) \le m-7 < 0. \end{align*} The Hausdorff dimension of a nonempty set is nonnegative, while the empty set is assigned Hausdorff dimension $-\infty$ by convention. Therefore the only possibility is $S = \varnothing$. Since $S = \operatorname{sing} T$, this is exactly the stated low-dimensional regularity conclusion. [/step]