ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

The certified FAS contraction radius shrinks at a pitchfork

Statement

For $F_{μ} (x, y) = (μ x + x^{3}, y)$ with zero right side, use the coarse space spanned by $(0, 1)^{T}$ , iterate and residual restriction $I (x, y) = R (x, y) = y$ , coarse residual $F_{H} (v) = v$ , and one pre- and one post-sweep $S_{μ} (x, y) = (x - \frac{1}{2} (μ x + x^{3}), y / 2)$ . The exact-branch FAS cycle has root $(0, 0)$ and derivative norm $q_{μ} = (1 - μ / 2)^{2} (0 < μ \leq 1) .$ For each such $μ$ , the local theorem certifies radius $r_{μ} = \sqrt{μ / 100}$ , which tends to zero as the pitchfork parameter approaches $0$ .

Facts & Assumptions

Given: $0 < μ \leq 1$ , the two-dimensional fine residual, zero right side, the stated transfers and coarse residual, one pre/post smoother, exact coarse solve, and exact arithmetic.

[F1]

Finite-budget nonlinear FAS two-grid cycle: the coarse target is $F_{H} (I u) + R (- F_{μ} (u))$ and the correction is $u + P (v - I u)$ .

[F2]

A smooth FAS cycle converges locally under its actual derivative bounds: if the actual exact-branch cycle has root derivative norm $q$ , derivative-Lipschitz constant $L$ on a radius- $r$ ball, and $q + L r / 2 < 1$ , then its iterates converge to the root from that ball.

[F3]

On a convex open set, a uniform bound $∥ D f (z) v ∥_{2} \leq M ∥ v ∥_{2}$ implies $∥ f (y) - f (x) ∥_{2} \leq M ∥ y - x ∥_{2}$ : a uniform derivative bound on a convex open set gives a Lipschitz bound there.

[F4]

Second derivative formula for a composed cycle map: applying the second-derivative composition formula with identity middle map gives $(s_{μ} \circ s_{μ})^{''} = s_{μ}^{''} (s_{μ}) (s_{μ}^{'})^{2} + s_{μ}^{'} (s_{μ}) s_{μ}^{''}$ .

Example

Given: The scalar function $s_{μ} (x) = (1 - μ / 2) x - x^{3} / 2$ , the radius $r_{μ} = \sqrt{μ / 100}$ , and the exact coarse branch.

Verification

1.1F1givenalgebra

Let $P (v) = (0, v)^{T}$ . For any pre-smoothed $(x, y)$ , [F1] gives $g_{H} = F_{H} (y) + R (- F_{μ} (x, y)) = y - y = 0.$ The exact coarse solution is $v = 0$ , so prolonging $v - I (x, y) = - y$ sets the second fine coordinate to zero. The following post-sweep leaves it zero. Hence the actual cycle map is $E_{μ} (x, y) = (s_{μ} (s_{μ} (x)), 0) .$

1.2givenF3F4algebra

Write $a = 1 - μ / 2$ and $r = r_{μ} \leq 0.1$ . For $∣ x ∣ \leq r$ , $∣ s_{μ} (x) ∣ \leq r + \frac{1}{2} r^{3} \leq 1.005 r, ∣ s_{μ}^{'} (x) ∣ \leq 1.015, ∣ s_{μ}^{'} (s_{μ} (x)) ∣ \leq 1.02,$ and $∣ s_{μ}^{''} (x) ∣ \leq 3 r$ , $∣ s_{μ}^{''} (s_{μ} (x)) ∣ \leq 3.015 r$ . By [F4], $(s_{μ} \circ s_{μ})^{''} = s_{μ}^{''} (s_{μ}) (s_{μ}^{'})^{2} + s_{μ}^{'} (s_{μ}) s_{μ}^{''}$ , so these bounds give $∣ (s_{μ} \circ s_{μ})^{''} (x) ∣ < 7 r$ . The derivative matrix of $E_{μ}$ is $diag ((s_{μ} \circ s_{μ})^{'} (x), 0)$ , so [F3] gives $∥ D E_{μ} (z) - D E_{μ} (z^{'}) ∥_{o p} \leq 7 r ∥ z - z^{'} ∥_{2}$ on the ball.

2.1givenstep 1.1algebra

Since $F_{μ} (x, y) = 0$ implies $y = 0$ and $x (μ + x^{2}) = 0$ , for $μ > 0$ the unique fine root is $(0, 0)$ . Also $s_{μ}^{'} (0) = 1 - μ / 2$ , so differentiating the two sweeps gives $D E_{μ} (0, 0) = (\begin{array}{cc} (1 - μ / 2)^{2} & 0 \\ 0 & 0 \end{array}), q_{μ} = (1 - μ / 2)^{2} .$

3.1F2step 2.1step 1.2algebra∎

With $r^{2} = μ / 100$ , $q_{μ} + \frac{(7 r) r}{2} = (1 - μ / 2)^{2} + \frac{7 μ}{200} = 1 - \frac{193}{200} μ + \frac{1}{4} μ^{2} \leq 1 - \frac{143}{200} μ < 1.$ Thus [F2] applies on this ball. Its certified radius $r_{μ} = \sqrt{μ / 100}$ tends to zero as $μ ↓ 0$ ; at $μ = 0$ , $q_{0} = 1$ and the strict derivative hypothesis fails. For $μ < 0$ , the scalar equation $μ x + x^{3} = 0$ has the additional roots $x = \pm \sqrt{- μ}$ , which is the pitchfork bifurcation.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.