VeriDiscover LabGitHub
← All writing

What a rough curve remembers about area

One boundary occupation density classifies the realizable area lifts of a rough Jordan curve, all subarcs at once.

veridiscoverLab10 min read

Draw a simple closed curve, then replace it by increasingly accurate smooth drawings. The shapes converge. Must the areas traced out by their individual arcs converge too? If they do, can two equally accurate sequences give different answers?

Our paper, Boundary occupation and realizable area lifts of Jordan curves, gives a precise answer for a critical class of rough curves. Every possible limiting area record is described by one measurable function on the original curve, taking values between zero and one. The function records how much of the curve's own planar area is included by the approximating interiors. It determines the answer on every arc simultaneously, and every such function can be realized by smooth curves that never cross themselves.

This classification also supplies the approximation needed for a rectangle theorem at the critical threshold of variation. The connection reaches a class of cases of the square peg problem, posed by Otto Toeplitz in 1911. The unrestricted problem remains open. The central contribution here is the structure behind the approximation: a description of exactly which area data the geometry permits. Problem history, current context

The question began with our reading of OpenAI's manuscript Finite time blowup for Navier–Stokes. Its construction for the smoothly forced three-dimensional equations has to realize prescribed stress data by an actual velocity field. Appendix C constructs admissible oscillations while restoring prescribed moments; Section 8.7 recomputes quadratic quantities after changing the field. A correction that disappears under one average can still matter after multiplication. We took from this a question about realizability: when an auxiliary quantity looks algebraically possible, what requires it to come from the same underlying object? Our planar theorems are independent of that PDE construction. OpenAI manuscript

For curves, the underlying object is a fixed parametrized Jordan curve. “Jordan” means continuous, closed, and without self-intersections. Write it as c(t)=(x(t),y(t))c(t)=(x(t),y(t)), with 0≤t≤10\leq t\leq1; only the initial and final points coincide. We orient it counterclockwise and keep this parameter throughout, so that a particular interval always names the same part of the original curve.

For a smooth approximation cn=(xn,yn)c_n=(x_n,y_n), its area record is the function

fn(t)=∫0tyn(u)xn′(u) du.f_n(t)=\int_0^t y_n(u)x_n'(u)\,du.

This is a running line integral. Subtracting its values at two times gives the integral along that arc. Closing the arc by the straight segment between its endpoints converts the integral into a signed area, with an explicit contribution from the segment. For a counterclockwise closed curve, our convention gives fn(1)f_n(1) equal to the negative of its enclosed area.

A realizable primitive is a uniform limit of these functions along smooth regular Jordan curves converging uniformly to cc. Regularity means the approximating velocity never vanishes. Both limits must come from the same sequence. We are asking for actual embedded approximations that carry the prescribed area record.

There is a familiar reason to be cautious. A circle of radius 1/n1/n, traversed n2n^2 times, converges uniformly to a point while retaining total signed area π\pi. This example, standard in rough-path theory, shows how repeated circulation can preserve area after visible motion disappears. Those traversals are not simple curves. Requiring every approximant to remain Jordan imposes a substantial additional restriction. Friz–Hairer, Exercise 2.10

To see the restriction, call the original curve's trace CC, its bounded interior DD, and the approximating interiors DnD_n. A point strictly inside DD eventually lies inside every DnD_n. A point outside the closure of DD eventually lies outside every DnD_n. Any persistent ambiguity in the included area must therefore live on CC itself.

For a circle or a polygon, that observation seems to leave no ambiguity: the outline has zero planar area. But continuous simple curves can have positive planar area. Osgood published an example in 1903; the history also includes Lebesgue's earlier construction and Knopp's construction of 1917. These curves have no open patch in their trace, yet the trace can occupy positive area. The relevant distinction is between being topologically one-dimensional and having zero two-dimensional measure. Osgood's paper, Nasso–Volčič on area-filling curves

At every stage, a point is either included in DnD_n or excluded. In a weak limit, increasingly fine patterns of inclusion can give an intermediate value. We call the resulting function θ:C→[0,1]\theta:C\to[0,1] a boundary occupation density. Weak convergence means that the included area converges when measured against fixed spatial test functions. A value such as 1/21/2 describes this averaged limit; it need not describe pointwise convergence of the individual inclusion decisions.

The fact that the ambiguity is supported on the boundary is only the beginning. The main rigidity statement says that a single density governs all the arc integrals. It is fixed for the entire curve before an arc is chosen. It is also determined by the limiting primitive: two sequences producing that primitive cannot hide different boundary occupations from spatial tests.

Here is the classification in a formula. Let mm denote ordinary planar area. Under the critical variation assumption described below, there is a reference primitive f0f_0, obtained by approximation from the interior, such that all realizable primitives are exactly

fθ(t)=f0(t)−∫c((0,t])θ dm,0≤θ≤1.f_\theta(t)=f_0(t)-\int_{c((0,t])}\theta\,dm, \qquad 0\leq\theta\leq1.

Densities are identified when they differ only on a set of zero planar area. The integral measures weighted area on the trace of the initial arc. Endpoints make no difference because a point has zero planar area. Thus, once a realizable primitive has been chosen, the information omitted from the original curve has a concrete location and a precise range.

For two choices θ\theta and η\eta, the difference on any interval [s,t][s,t] is

(fθ−fη)(t)−(fθ−fη)(s)=−∫c((s,t])(θ−η) dm.(f_\theta-f_\eta)(t)-(f_\theta-f_\eta)(s) =-\int_{c((s,t])}(\theta-\eta)\,dm.

One cannot independently prescribe an area correction to each small arc and expect them to fit together. They must be restrictions of the same boundary measure. This is the useful mathematical object: the entire family of realizable lifts, organized by occupation on one fixed geometric carrier.

The formula is easy to use. If m(C)=0m(C)=0, it leaves at most one realizable primitive. Within the critical class, existence supplies exactly one. If the trace has positive area, choosing θ=1\theta=1 on a measurable portion AA and zero elsewhere changes the primitive by the cumulative area of AA. Choosing θ=1/2\theta=1/2 everywhere gives half the maximal boundary correction. In particular, total enclosed areas can range from m(D)m(D) to m(D)+m(C)m(D)+m(C), but equal total areas need not give equal primitives: the distribution of occupied area along the curve still matters.

The classification also describes the shape of the entire space of choices. It is compact in the uniform topology and convex: an average of two realizable primitives is realizable, even though averaging their curves would generally destroy embeddedness. Its extreme points are exactly the occupations that choose zero or one almost everywhere. Intermediate densities are mixtures in this precise geometric space.

Why is every allowed density attainable? A density bound alone does not construct a curve. The realization proof starts with two genuine families of smooth Jordan curves, one approaching from inside and one from outside. Their limiting boundary occupations are zero and one. We then select finitely many parameter intervals on which to follow the outer approximation, following the inner approximation elsewhere. Bridges in the intervening annulus connect the selected pieces.

The bridges must be chosen together. A connector that works for one arc can obstruct another, and smoothing a corner without further control can introduce a crossing. The construction preserves the cyclic order of all selected intervals and separates the connecting regions. At the remaining finitely many bad joins, small chord replacements provide local directions in which the curve moves strictly forward. Smoothing then preserves local injectivity, while separation of distant parameter pairs preserves global injectivity. The same construction controls the actual line integrals, so the resulting smooth curves retain the desired primitive limit.

Finer choices of intervals approximate arbitrary measurable occupations. To understand a fractional density, imagine alternating included and excluded pieces on smaller scales, choosing their proportions according to boundary area. The approximation concerns all cumulative boundary areas together. A single diagonal sequence then makes the curves and their primitives converge simultaneously. Fractional occupation is achieved by ordinary simple curves at every stage.

The critical hypothesis explains when this family of primitives exists. For a continuous scalar function xx, its strong pp-variation is

Vp(x)=(sup⁡0=t0<⋯<tN=1∑j=1N∣x(tj)−x(tj−1)∣p)1/p.V_p(x)=\left(\sup_{0=t_0<\cdots<t_N=1} \sum_{j=1}^{N}|x(t_j)-x(t_{j-1})|^p\right)^{1/p}.

The supremum runs over every finite partition. It measures the total budget of oscillation at exponent pp, including choices of sampling times adapted to the path. Our assumption is that Vp(x)V_p(x) and Vq(y)V_q(y) are finite for exponents p,q>1p,q>1 satisfying

1p+1q=1.\frac1p+\frac1q=1.

Young's integration theorem, dating to 1936, handles the strict inequality 1/p+1/q>11/p+1/q>1. Its usual conclusion does not automatically extend to equality. Sauzedde's anisotropic winding and Green theorem also works in that strict range. We reach equality for the present realization problem by using the geometry of simple arcs. Young's original paper, Sauzedde, Theorem 0.2

The key estimate has a direct geometric explanation. Draw the line through the endpoints of a simple arc. Break the arc into its excursions away from that line. Each excursion, together with its closing segment, bounds a Jordan domain. If its horizontal and vertical oscillations are aja_j and bjb_j, its area is at most ajbja_jb_j, the area of its coordinate bounding rectangle.

The intervals belonging to distinct excursions are disjoint. Their horizontal oscillations therefore draw on one pp-variation budget, and their vertical oscillations draw on one qq-variation budget. Hölder's inequality gives

∑jajbj≤(∑jajp)1/p(∑jbjq)1/q.\sum_j a_jb_j \leq\left(\sum_j a_j^p\right)^{1/p} \left(\sum_j b_j^q\right)^{1/q}.

This is an area estimate that still closes at equality. A long, narrow excursion may have a large diameter while enclosing little area, so keeping the two coordinate budgets separate is essential. Combined with conformal approximation and control of the original parameter, the estimate produces a uniformly convergent primitive. The occupation construction then gives the full classification throughout this conjugate-exponent class.

The symmetric choice is p=q=2p=q=2. It includes every Jordan parametrization that is 1/21/2-Hölder: its displacement over a time interval is bounded by a constant times the square root of the interval's length. Squaring and summing shows that its strong quadratic variation is finite. Here “strong” matters: the bound concerns every partition, rather than a quadratic-variation limit along one prescribed sequence. Unequal conjugate exponents allow different amounts of roughness in the two coordinates.

The rectangle consequence uses a separate result of Asano and Ike. Their criterion turns a smooth Jordan approximation with convergent area primitives into inscribed rectangles of every prescribed similarity class. Applying it to the critical construction gives that conclusion for the curves above, including finite strong quadratic variation. This is an application of their theorem; its microlocal sheaf argument is not part of our Lean proof. Asano–Ike, Theorem 1.1

This places the result within a problem with more than a century of history. Toeplitz's 1911 question asks for a square on every continuous Jordan curve. We establish a critical-class consequence in that problem's larger rectangle setting. The closest recent comparison is Li and Pan's September 2026 result for finite rr-variation with r<2r<2; the endpoint r=2r=2 is outside that theorem. Positive-area traces already have all prescribed rectangles by an earlier density argument, so classifying their area lifts is a different contribution. Li–Pan, Asano–Ike, Remark 5.5

We have also formalized the scalar classification, its topological structure, and the geometric constructions it needs in Lean. The release records contain the exact theorem statements, source hashes, and results of compilation and kernel replay on a server. It retains two explicit classical inputs: conformal uniformization of a Jordan domain with its boundary correspondence, and Green's area formula. The internal approximation, comparison, gluing, and smoothing arguments are proved within the project. The verification scope does not include every theorem in the manuscript or the external rectangle criterion. Formal statement and verification scope

The resulting mechanism separates three questions that can otherwise become entangled. Geometry locates the possible defect on the boundary. Rigidity forces all observations of it to arise from one density. Realization determines whether every admissible density can actually occur. Together they turn an ambiguity in rough integration into a classified geometric freedom, with explicit constraints and a constructive converse. That is the mathematical understanding we hope will be useful beyond this particular family of curves.

The paper, source code, and verification records are available in the boundary-occupation repository.

The accompanying manuscript

Boundary occupation and realizable area lifts of Jordan curves

Preprint · September 10, 2026

The v0.1.0 verification records report 159 Lean modules and 1,380 declarations passing server compilation, axiom audit, and project kernel replay. The scalar classification retains two classical theorem inputs; the external rectangle criterion is not included in this formalization.