TheoremStatement: AI-adaptedProof: 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.

Contraction and finite-sweep error bound for synchronous waveform relaxation

Statement

Let $r, s \geq 1$ and $d = r + s$ , write $u = (x, z) \in R^{r} \times R^{s}$ , and let $F = (f, g) : D \to R^{d}$ be continuous on an open set $D \subseteq R^{d}$ . Fix $u_{0} \in D$ , $Δ > 0$ , and a closed ball ${\overline{B}}_{R} (u_{0}) \subseteq D$ with radius $R \geq 0$ . Suppose $∥ F (u) ∥_{2} \leq M$ and $∥ F (u) - F (v) ∥_{2} \leq K ∥ u - v ∥_{2}$ on that ball, where $M, K \geq 0$ , $M Δ \leq R$ , and $q : = K Δ < 1$ . Let $X_{R}$ be the set of continuous waveforms $U : [0, Δ] \to R^{d}$ with $U (0) = u_{0}$ and $\sup_{t} ∥ U (t) - u_{0} ∥_{2} \leq R$ , with the supremum metric, and define $Φ (U) (t) = u_{0} + \int_{0}^{t} F (U (s)) d s$ . Then $Φ : X_{R} \to X_{R}$ is a contraction with factor $q$ . It has a unique fixed point $U^{*}$ , which solves $U^{'} = F (U)$ with $U (0) = u_{0}$ . For any starting waveform $U^{0} \in X_{R}$ , if $U^{k + 1} = Φ (U^{k})$ and $δ_{0} : = ∥ U^{1} - U^{0} ∥_{\infty}$ , then $∥ U^{k} - U^{*} ∥_{\infty} \leq \frac{q^{k}}{1 - q} δ_{0} (k \geq 1) .$ Thus the finite-window algorithm certifies tolerance $ε$ after $k$ sweeps whenever this displayed bound is at most $ε$ ; budget exhaustion without that inequality supplies no such certificate.

Facts & Assumptions

Given: The domain, initial value, bounded/Lipschitz field, radius and window conditions, and waveform map in the Statement.

[F1]

Synchronous Picard waveform relaxation on a finite window: $X_{R}$ is the closed radius- $R$ set of continuous curves with initial value $u_{0}$ , and $Φ (U) (t) = u_{0} + \int_{0}^{t} F (U (s)) d s$ updates both component waveforms from the previous pair.

[F2]

Continuous $R^{d}$ -valued curves on a nonempty compact interval form a complete space in the supremum metric (Continuous $R^{n}$ -valued curves on a nonempty compact interval form a complete supremum-metric space).

[F3]

A closed subset of a complete metric space is complete in ZF, without a choice axiom (Closed subspaces of complete metric spaces are complete; the converse under countable choice, claim 2).

[F4]

For an integrable vector function on an increasing interval, $∥ \int_{a}^{b} V (s) d s ∥_{2} \leq \int_{a}^{b} ∥ V (s) ∥_{2} d s$ (For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable).

[F5]

The vector Riemann integral is componentwise and additive over subintervals (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral). A continuous real-valued function on a compact interval is Riemann integrable, so the continuous vector integrand is componentwise integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[F6]

A contraction of a nonempty complete metric space into itself has a unique fixed point, its iterates converge, and for $m \geq k$ the iterates satisfy $d (U^{m}, U^{k}) \leq q^{k} d (U^{1}, U^{0}) / (1 - q)$ (A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point).

[F7]

A continuous curve solves the first-order IVP exactly when it satisfies the associated Volterra equation (A first-order initial value problem is equivalent to its Volterra integral equation).

[A1]

$M Δ \leq R$ and $q = K Δ < 1$ ; the stated field bounds hold throughout the closed ball.

Proof

1.1F1F2F3givenalgebra

The constant waveform $U (t) = u_{0}$ belongs to $X_{R}$ , so $X_{R}$ is nonempty. By [F2] the ambient continuous-curve space is complete. If $U_{n} \in X_{R}$ and $U_{n} \to U$ uniformly, then $U (0) = u_{0}$ and, for every $t$ , $∥ U (t) - u_{0} ∥_{2} \leq ∥ U - U_{n} ∥_{\infty} + R$ ; letting $n \to \infty$ gives $∥ U (t) - u_{0} ∥_{2} \leq R$ . Hence $X_{R}$ is closed and complete by the choice-free direction [F3].

1.2F1F4F5A1algebra

For $U \in X_{R}$ , continuity of $U$ and the field Lipschitz bound imply $∥ F (U (t)) - F (U (t_{0})) ∥_{2} \leq K ∥ U (t) - U (t_{0}) ∥_{2} \to 0$ as $t \to t_{0}$ ; this holds with one-sided limits at endpoints. Thus $F \circ U$ is continuous and componentwise integrable by [F5]. For $0 \leq s \leq t \leq Δ$ , additivity and [F4] give $∥ Φ (U) (t) - Φ (U) (s) ∥_{2} \leq M (t - s)$ ; also $Φ (U) (0) = u_{0}$ and $∥ Φ (U) (t) - u_{0} ∥_{2} \leq M t \leq M Δ \leq R$ . Thus $Φ (U) \in X_{R}$ .

1.3F1F4A1algebra

For $U, V \in X_{R}$ and $t \in [0, Δ]$ , [F4] and the field Lipschitz bound yield $∥ Φ (U) (t) - Φ (V) (t) ∥_{2} \leq \int_{0}^{t} K ∥ U (s) - V (s) ∥_{2} d s \leq K Δ ∥ U - V ∥_{\infty} = q ∥ U - V ∥_{\infty}$ . Taking the supremum proves that $Φ$ is a contraction with $q < 1$ .

2.1F1F2F3F6step 1.1step 1.2step 1.3

By [F1], [F2]–[F3], and step 1.3, [F6] applies to the nonempty complete space $X_{R}$ and the map $Φ : X_{R} \to X_{R}$ . It gives a unique fixed point $U^{*}$ and convergence of the iterates from every $U^{0} \in X_{R}$ .

3.1F1F7step 2.1

The fixed-point identity is $U^{*} (t) = u_{0} + \int_{0}^{t} F (U^{*} (s)) d s$ . By [F7], this is equivalent to the IVP $U^{'} = F (U)$ , $U (0) = u_{0}$ .

4.1F1F6step 2.1algebra∎

Fix $k \geq 1$ . By [F6], for every $m \geq k$ , $∥ U^{m} - U^{k} ∥_{\infty} \leq q^{k} δ_{0} / (1 - q)$ . Since $U^{m} \to U^{*}$ in $X_{R}$ , the triangle inequality gives $∣ ∥ U^{*} - U^{k} ∥_{\infty} - ∥ U^{m} - U^{k} ∥_{\infty} ∣ \leq ∥ U^{*} - U^{m} ∥_{\infty} \to 0$ ; passing to the limit proves the stated bound. The algorithm reports tolerance-certified only when this bound is at most $ε$ ; when the finite budget ends first, it reports budget-exhausted without claiming the requested tolerance.

Depends on

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by Synchronous Picard waveform relaxation on a finite window.

Dependency tree · two levels

88 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.

Sources

Ekachai Lelarasmee, The Waveform Relaxation Method for Time-Domain Analysis of Large Scale Integrated Circuits: Theory and Applications, UCB/ERL M82/40 (1982) (standard reference, not scraped)
Mark Embree, Lecture Notes on Numerical Analysis, Lecture 34: Global Analysis of One-Step Integrators (2016) (standard reference, not scraped)