ExampleConstruction: AI-adaptedVerification: AI-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Positive-measure attraction to a degenerate saddle

PDF p. 3: Footnote 3

Example

Let $U : R^{2} \to R$ be $U (x, y) = x^{3} + y^{3}$ . Its negative-gradient flow is the system $\dot{x} = - \partial_{x} U$ , $\dot{y} = - \partial_{y} U$ ; a trajectory means a differentiable solution on an open interval containing $0$ that admits no extension as a solution to a larger such interval. The origin is a degenerate saddle: it is a critical point, its Hessian is the zero matrix, and every neighborhood of it contains points where $U$ is greater than $U (0, 0)$ and points where $U$ is less. Every trajectory starting in the positive quadrant $(0, \infty)^{2}$ exists for all forward time and converges to $(0, 0)$ . Assuming countable choice, the set of such initial points contains a Lebesgue-measurable box of positive measure.

Example references

First-order systems, initial value problems, and solutions on intervals

The Hessian matrix and critical points of a scalar field

Explicit scalar quadratic descent and its forward domain

The Axiom of Countable Choice (AC_ω)

A box in ℝⁿ with parameters aᵢ≤ bᵢ is Lebesgue measurable of measure ∏_i<n(bᵢ-aᵢ), whichever of its faces are included

Facts & Assumptions

Given: The function $U$ and its negative-gradient system in the example. Countable choice is assumed for the measure assertion.

Goal: Verify the saddle properties, forward convergence, and the positive-measure assertion.

[F1]

A critical point has zero gradient, and the Hessian is the matrix of second partial derivatives (The Hessian matrix and critical points of a scalar field).

[F2]

The power, sum, and product rules give the indicated derivatives of polynomials (Sum, product, quotient, and chain rules from difference quotients).

[F3]

For $\dot{u} = - a u^{2}$ with $a > 0$ and $u (0) = u_{0} > 0$ , the unique maximal solution is $u (t) = u_{0} / (1 + a u_{0} t)$ on $(- 1 / (a u_{0}), \infty)$ . Finitely many independent such coordinates give forward solutions converging to zero. Assuming countable choice, their attraction region contains the positive-measure box $(0, 1)^{n}$ (Explicit scalar quadratic descent and its forward domain, The Axiom of Countable Choice (AC_ω)).

[F4]

Assuming countable choice, for $n \geq 1$ and real endpoints $a_{i} \leq b_{i}$ , an open box $\prod_{i < n} (a_{i}, b_{i})$ is Lebesgue measurable with measure $\prod_{i < n} (b_{i} - a_{i})$ (A box in ℝⁿ with parameters aᵢ≤ bᵢ is Lebesgue measurable of measure ∏_i<n(bᵢ-aᵢ), whichever of its faces are included, The Axiom of Countable Choice (AC_ω)).

[F5]

For an open set $D \subseteq R \times R^{n}$ and a map $F : D \to R^{n}$ , a solution with initial data $(0, z_{0}) \in D$ is a differentiable map $z : I \to R^{n}$ on an interval containing $0$ , satisfying $(t, z (t)) \in D$ , $z (0) = z_{0}$ , and $z^{'} (t) = F (t, z (t))$ for every $t \in I$ . Here take $n = 2$ , $D = R \times R^{2}$ , $z = (x, y)$ , and $F (t, z) = (- \partial_{x} U (x, y), - \partial_{y} U (x, y))$ ; this system equation means that both coordinate equations hold (First-order systems, initial value problems, and solutions on intervals).

Verification

technique · direct

1.1F1F2algebra

By the polynomial derivative rules, $\nabla U (x, y) = (3 x^{2}, 3 y^{2})$ and $\nabla^{2} U (x, y) = (\begin{array}{cc} 6 x & 0 \\ 0 & 6 y \end{array})$ . Thus the origin is critical and its Hessian is zero. For every $ε > 0$ , the points $(t, 0)$ and $(- t, 0)$ with $0 < t < ε$ are within $ε$ of the origin, while their respective values are $t^{3} > 0$ and $- t^{3} < 0$ . This proves the stated saddle property.

2.1givenF3F5step 1.1

The negative-gradient equations are $\dot{x} = - 3 x^{2}$ and $\dot{y} = - 3 y^{2}$ . For initial data $(x_{0}, y_{0}) \in (0, \infty)^{2}$ , [F3] gives $x (t) = x_{0} / (1 + 3 x_{0} t)$ and $y (t) = y_{0} / (1 + 3 y_{0} t)$ . The intersection of their maximal intervals is $I = (\max {- 1 / (3 x_{0}), - 1 / (3 y_{0})}, \infty)$ . The pair of formulas is a solution on $I$ by [F5]; scalar uniqueness makes any solution with these initial data agree with the formulas wherever both are defined. The coordinate whose pole is the left endpoint of $I$ cannot extend across that endpoint, by scalar maximality. Hence the pair is the unique maximal trajectory. Its domain contains every $t \geq 0$ , and each coordinate tends to zero as $t \to \infty$ .

3.1givenF4step 2.1algebra∎

By step 2.1 every initial point of $(0, 1)^{2}$ has a trajectory converging to the origin. Under countable choice, [F4] with $n = 2$ and endpoints $a_{0} = a_{1} = 0$ , $b_{0} = b_{1} = 1$ makes this box Lebesgue measurable with measure $(1 - 0) (1 - 0) = 1 > 0$ . This proves the positive-measure assertion.

Source notes

The example is attributed to the article's footnote 3. Its verification above uses the stated mathematical suppliers and direct calculation.

Depends on

Dependency tree · 2 levels

Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.

Sources

Expander graphs are globally synchronizing · PDF p. 3, footnote 3