Alphabeta Math
Pipeline-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.

✓ 10 results · all verified · 3 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 7 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Nonsmooth contact time stepping and projections

1 · Prerequisites

2 · Summary

This page treats two distinct finite-dimensional contact models. For a fixed nonempty compact convex set, it defines the outward normal-cone evolution and explicit projection Euler, proves the normal-cone and projection facts used by the method, and proves uniqueness under the choice assumptions inherited through its absolutely-continuous FTC supplier. Countable Choice is used for almost-everywhere differentiability, Lebesgue differentiation, and null-set unions; Dependent Choice is inherited through the integrated FTC identities. The exact Euler interpolants converge uniformly; with certified per-step projection residuals, the error is bounded by a constant times h plus the accumulated projection tolerances. The computation reports an unresolved status when a projection certificate cannot be produced within its budget.

For one-dimensional unilateral impact, the first-impact algorithm accepts constant acceleration and a prescribed restitution coefficient. It returns free flight when the complete incoming-root list is empty and the gap is certified nonnegative on the whole step, including a grazing zero that does not cause penetration; it returns unresolved when root completeness or nonpenetration cannot be certified. Its proof establishes momentum balance, complementarity, and the kinetic-energy change at the instantaneous impact; it does not continue through sustained contact or repeated impacts. A separate frictionless binary-sphere law is proved by direct impulse algebra. The event-driven sphere algorithm accepts explicitly valid finite dense/event providers and consumes the event page's general time-error, reset-error and mode-flow interfaces. Its certificates enforce nonpenetrating reference states and account for every guard zero; any unlisted or nontransverse zero returns unresolved. A local geometry lemma supplies the full-state guard/normal and reset Lipschitz bounds. Event-bracket width, guard residual, prior reset error and outgoing flow during a reporting lag are kept separate; only matched smooth prefixes and aligned reset states are compared. This retains arbitrary C1 force fields without claiming a generic provider construction from a rational-expression checker. Frictional multi-contact, simultaneous impacts, grazing event times, Zeno behavior, and a penalty-to-rigid limit are outside the proved event guarantees.

3 · Logical flowchart

4 · Definitions, theorems and proofs

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Compactness of equi-Lipschitz curves with values in a compact Euclidean set

Statement

Let d≥1, T>0, and let C⊆Rd be nonempty, compact, and closed. Let M≥0. If uj:[0,T]→C satisfies ∥uj(t)−uj(s)∥2≤M∣t−s∣(j≥1, s,t∈[0,T]), then some subsequence converges uniformly to a map u:[0,T]→C with the same Lipschitz bound.

Facts & Assumptions

Given: The set C, interval [0,T], constant M, and sequence of maps in the Statement. Compactness has its open-cover meaning; the Lipschitz inequality is displayed in the Statement.

[F1]

Heine-Borel in Rn: with the Euclidean metric a subset of Rn is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line: every compact subset of Rd is bounded; Every complete ordered field is Archimedean: the natural numbers are cofinal in R, so a bounded set is contained in a box [−R,R]d for some integer R≥1.

[F3]

Convergence of a sequence in a metric space: xk→x iff d(xk,x)→0 in R: if a sequence converges to x, then it is eventually in every open ball centered at x.

[F4]

The reals are complete: every Cauchy sequence of real numbers converges in R.

[F5]

The well-ordering principle and The recursion theorem: every nonempty subset of N has a least element, and a uniquely specified recursive sequence on N exists.

[F6]

Integer part: for every real x there is exactly one integer m with m≤x<m+1: for each real a there is an integer m with m≤a<m+1.

[F8]

Cauchy-Schwarz ∣⟨x,y⟩∣≤∥x∥2∥y∥2 with its equality case, the triangle inequality for ∥⋅∥2, the parallelogram law and polarisation: ∥x∥22=∑k<dxk2, each coordinate satisfies ∣xk∣≤∥x∥2, and the Euclidean norm satisfies the triangle inequality.

[F9]

The principle of mathematical induction: every finite initial segment {0,…,N} of N is finite.

Proof

1.1F1F6F8F9givenchoose

By [F1], choose an integer R≥1 with C⊆[−R,R]d. For each natural r≥1, let Γr={kT/2r:0≤k≤2r} and put Kr=(R+1)2r. Let Gr consist of the lattice points whose coordinates are mk2−r with integers −Kr≤mk≤Kr. Each coordinate index set is finite: its nonnegative and negative parts are copies of finite natural initial segments, which are finite by [F9]; induction on the finite number d of coordinates shows their Cartesian product Gr is finite. To verify its covering radius, fix x∈[−R,R]d. For each k<d, [F6] applied to 2rxk gives an integer mk with mk≤2rxk<mk+1. Thus mk≤R2r≤Kr and mk>−R2r−1≥−(R+1)2r=−Kr, using 1≤2r for r≥1 (from the power recursion and induction). The corresponding lattice point g has ∣xk−gk∣<2−r in every coordinate, so [F8] gives ∥x−g∥22=∑k<d∣xk−gk∣2<d2−2r and hence ∥x−g∥2<δr:=d 2−r. Assign each value uj(t) at each t∈Γr to the first lattice point within δr in a fixed ordering of Gr. This gives one of finitely many patterns.

2.1step 1.1F5givenchoose

Starting from the positive index set I0={j∈N:j≥1}, partition each infinite index set Ir−1 by the finitely many patterns at resolution r. At least one class is infinite; choose the first such pattern in the fixed finite ordering and let Ir be its infinite class. Then Ir⊆Ir−1.

3.1step 2.1F5F9choose

Set n0=1∈I0. For r≥1, recursively choose nr to be the least member of Ir greater than nr−1. The infinite set Ir is unbounded: if it were contained in some finite initial segment {0,…,N}, that segment would be finite by [F9], contradicting that Ir is infinite. Hence {n∈Ir:n>nr−1} is nonempty, and [F5] supplies its least member. For every fixed r, all nk with k≥r belong to Ir, so the maps with those indices have the same resolution-r pattern.

4.1step 3.1F7F8givenchoosealgebra

For k,l≥r and t∈[0,T], choose s∈Γr with ∣t−s∣≤T/2r. At each lattice time, the common pattern assigns both values to the same lattice point, so the triangle inequality [F8] gives ∥unk(s)−unl(s)∥2≤2δr. Using the Lipschitz bounds and the triangle inequality again, ∥unk(t)−unl(t)∥2≤∥unk(t)−unk(s)∥2+∥unk(s)−unl(s)∥2+∥unl(s)−unl(t)∥2≤2MT/2r+2δr. By [F7], the right side tends to zero as r→∞, uniformly in t, so (unk) is uniformly Cauchy.

5.1F2F3F4F7F8step 4.1given∎

At each t, step 4.1 and [F8] make every coordinate sequence unk(t)j Cauchy; [F4] therefore gives a pointwise limit u(t)∈Rd. Given ε>0, choose r so ρr:=2MT/2r+2δr<ε, using [F7]. For every k≥r, step 4.1 gives ∑j<d∣unk(t)j−unl(t)j∣2≤ρr2 for all l≥r and all t. Passing to the coordinatewise limit in this finite sum yields ∑j<d∣unk(t)j−u(t)j∣2≤ρr2, hence ∥unk(t)−u(t)∥2≤ρr<ε, uniformly in t. Thus the subsequence converges uniformly. If u(t)∉C, openness of the complement [F2] gives a ball about u(t) disjoint from C, while convergence [F3] puts unk(t) in that ball eventually, a contradiction. Thus u(t)∈C. For fixed s,t, coordinatewise convergence at those two points gives ∑j<d∣u(t)j−u(s)j∣2=lim⁡k∑j<d∣unk(t)j−unk(s)j∣2≤M2∣t−s∣2; taking nonnegative square roots yields ∥u(t)−u(s)∥2≤M∣t−s∣.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Projection onto a closed convex set is nonexpansive

Statement

Let d∈N, including d=0. Let C⊆Rd be nonempty, closed, and convex, and let PC(y) denote the unique nearest point in C to y. Then ∥PC(u)−PC(v)∥2≤∥u−v∥2(u,v∈Rd).

Facts & Assumptions

Given: The set C and points u,v in the Statement.

[F1]

For d≥1, Metric projection onto a closed convex set satisfies the variational inequality: if p=PC(y), then ⟨y−p,z−p⟩≤0 for every z∈C.

[F3]

The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn: R0 consists of its single zero vector, whose norm is 0.

Proof

1.1F3given

If d=0, then the nonempty set C⊆R0={0} is {0}, so PC is the constant zero map and the claimed inequality is 0≤0.

1.2F1givenalgebra

Now assume d≥1. Put p=PC(u) and q=PC(v). Applying [F1] first with (y,z)=(u,q) and then with (y,z)=(v,p) gives ⟨u−p,p−q⟩≥0 and ⟨q−v,p−q⟩≥0. Therefore ⟨u−v,p−q⟩=⟨u−p,p−q⟩+∥p−q∥22+⟨q−v,p−q⟩≥∥p−q∥22.

2.1F2step 1.2givenalgebra∎

By [F2], ∥p−q∥22≤∥u−v∥2∥p−q∥2. If p=q the result is immediate; otherwise divide by the positive number ∥p−q∥2.

AlgorithmAlgorithm: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

First-impact step for a one-dimensional unilateral contact

Definition

Input a gap q≥0, velocity v∈R, constant acceleration a∈R, step horizon h>0, mass m>0, restitution e∈[0,1], and a candidate-root budget B∈N. Use exact real arithmetic and comparisons. Define g(s)=q+sv+12as2 and w(s)=v+as on [0,h]. Return impact, free-flight, or unresolved by these instructions.

  • If q=0 and v<0, return impact at s=0 with contact gap 0, v−=v, J=−m(1+e)v−, and v+=−ev−.
  • Otherwise form the complete candidate set R of real roots of g. If q=v=a=0, set R=∅. If a=0 and v≠0, set R={−q/v}. If a=0, v=0, and q>0, set R=∅. If a≠0, put D=v2−2aq: for D<0 set R=∅; for D=0 set R={−v/a}; and for D>0 set R={(−v−D)/a,(−v+D)/a}, with duplicate values removed. If ∣R∣>B, return unresolved. From R, retain exactly the values s satisfying 0<s≤h and w(s)<0, and order them increasingly.
  • If the retained list is nonempty, take its least value s, set v−=w(s), J=−m(1+e)v−, and v+=−ev−, and return impact with time s, contact gap 0, impulse J, and post-impact velocity v+.
  • If the retained list is empty, compute the minimum of g on [0,h] by evaluating its two endpoints and, when a>0 and −v/a∈(0,h), its vertex −v/a. If this minimum is negative, return unresolved; otherwise return free-flight with endpoint (g(h),w(h)) and impulse 0.

The candidate set contains every root of the nonzero polynomial g, so the retained list is complete. The vertex check certifies nonpenetration over the whole step, including a grazing zero. The procedure stops after this first event and returns at the event time; it does not integrate the post-impact mode, sustained contact, or repeated impacts. A numerical implementation that cannot certify an exact comparison returns unresolved.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Impulse, momentum, and kinetic-energy laws for an isolated frictionless sphere impact

Statement

Let two spheres of radii r1,r2>0 and masses m1,m2>0 have centers q1,q2∈Rd at contact, so ∥q1−q2∥2=r1+r2. Let n=(q1−q2)/(r1+r2) be the unit normal pointing from center 2 to center 1. Suppose the pre-impact relative normal velocity is vn=⟨v1−−v2−,n⟩<0. For prescribed restitution e∈[0,1], put α=1m1+1m2,J=−(1+e)vnα,v1+=v1−+Jm1n,v2+=v2−−Jm2n. Then J>0, total linear momentum is conserved, the post-impact relative normal velocity is −evn, each tangential velocity is unchanged, and K+−K−=−(1−e2)vn22(1/m1+1/m2)≤0, where K±=12m1∥v1±∥22+12m2∥v2±∥22. This is a single frictionless binary impulse law; it asserts no existence or uniqueness for simultaneous or frictional multi-contact.

Facts & Assumptions

Given: The two masses, contact normal, pre-impact velocities, and restitution coefficient in the Statement.

[F1]

The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn: the Euclidean inner product is bilinear and symmetric, and ∥x∥22=⟨x,x⟩.

Proof

1.1F1givenalgebra

Since m1,m2>0, α>0. Since 1+e>0 and vn<0, J>0. The impulse changes total momentum by m1(v1+−v1−)+m2(v2+−v2−)=Jn−Jn=0.

2.1F1step 1.1givenalgebra

Taking the relative normal component gives ⟨v1+−v2+,n⟩=vn+J(1m1+1m2)=vn−(1+e)vn=−evn. For either velocity, projection onto any vector orthogonal to n is unchanged because the impulse term is parallel to n.

3.1F1step 1.1givenalgebra∎

Expanding the two squared norms with [F1] yields K+−K−=J⟨v1−−v2−,n⟩+J22(1m1+1m2)=Jvn+J2α2. Substitute J=−(1+e)vn/α to obtain K+−K−=−(1−e2)vn2/(2α). Since 0≤e≤1, this is nonpositive; at e=0 it is the maximal loss in this law and at e=1 it is zero.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

A certified projection variational residual bounds the projection error

Statement

Let d∈N, including d=0. Let C⊆Rd be nonempty, closed, and convex. If y∈Rd, ε≥0, and p∈C satisfy sup⁡z∈C⟨y−p,z−p⟩≤ε2, then ∥p−PC(y)∥2≤ε.

Facts & Assumptions

Given: The set C, input y, tolerance ε, and feasible candidate p in the Statement.

[F1]

For d≥1, Every point has a unique nearest point in a nonempty closed Euclidean convex set supplies the unique nearest point q=PC(y)∈C; Metric projection onto a closed convex set satisfies the variational inequality gives ⟨y−q,z−q⟩≤0 for every z∈C.

[F2]

The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn: R0={0} and its Euclidean norm and inner product are zero.

Proof

1.1F2given

If d=0, then C={0}, y=p=PC(y)=0, and the residual supremum is 0≤ε2; the asserted distance is 0≤ε.

1.2F1givenalgebra

Now assume d≥1. Put q=PC(y) and d0=p−q. The residual bound at z=q gives ⟨y−p,d0⟩≥−ε2. By [F1] with z=p, ⟨y−q,d0⟩≤0. Since y−q=(y−p)+d0, this also gives ⟨y−p,d0⟩+∥d0∥22≤0.

2.1step 1.2givenalgebra∎

Combining the two bounds yields ∥d0∥22≤ε2. Both sides are nonnegative, so ∥p−PC(y)∥2=∥d0∥2≤ε. This also covers ε=0.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Complementarity, momentum balance, and energy loss at a scalar impact

Statement

For any resolved output of First-impact step for a one-dimensional unilateral contact, let q∗ be the reported gap (zero at an impact, the free-flight endpoint gap otherwise), let J be the reported impulse, and let v∗ be the reported endpoint velocity. Then q∗≥0, J≥0, and q∗J=0. On a free-flight branch, J=0 and mv∗=mv+mah. On an impact branch at time s, with incoming velocity v−=v+as, the post-impact velocity satisfies mv+=mv−+J and 12m(v+)2−12m(v−)2=−12m(1−e2)(v−)2≤0. When a=0, the full resolved step has nonincreasing kinetic energy. For a≠0, the displayed energy statement concerns only the instantaneous impact jump; work during free flight is not covered by it.

Facts & Assumptions

Given: The inputs and resolved output of the algorithm in the Statement.

[F1]

First-impact step for a one-dimensional unilateral contact: an impact output has q∗=0, v−<0, J=−m(1+e)v−, and v+=−ev−; a free-flight output has J=0, q∗=q+hv+12ah2≥0, and v∗=v+ah.

Proof

1.1F1givenalgebra

On an impact branch, [F1] gives q∗=0, J=−m(1+e)v−>0, and v+=−ev−≥0, since m>0, e∈[0,1], and v−<0. Hence q∗J=0. On a free-flight branch, [F1] gives q∗≥0 and J=0, so complementarity also holds.

1.2F1givenalgebra

On a free-flight branch, mv∗=m(v+ah)=mv+mah. On an impact branch, [F1] gives mv−=m(v+as) and J=−m(1+e)v−. Therefore mv−+J=mv−−m(1+e)v−=−mev−=mv+, using v+=−ev−.

2.1F1step 1.1givenalgebra∎

On an impact branch, [F1] gives (v+)2=e2(v−)2, so the kinetic-energy difference is 12m(e2−1)(v−)2=−12m(1−e2)(v−)2≤0. If a=0 and the branch is free flight, v∗=v and kinetic energy is unchanged; impact branches have the nonincrease just established. For nonzero a, no claim is made about total free-flight work.

LemmaStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

Sphere-contact guards, normals and binary resets have explicit tube bounds

Statement

Use the Euclidean norm on the full state z=(q1,…,qP,v1,…,vP) of P≥2 spheres in Rd. Fix a pair i<j, positive masses mi,mj, positive radii ri,rj, and a fixed restitution coefficient e∈[0,1]. Put dij=qi−qj,n(z)=dij∥dij∥2,γ(z)=∥dij∥2−ri−rj, α=mi−1+mj−1,κ=1+eα,β=mi−2+mj−2. Extend the binary reset formula of Impulse, momentum, and kinetic-energy laws for an isolated frictionless sphere impact to every state with dij≠0 by setting J(z)=−κ⟨vi−vj,n(z)⟩, replacing vi by vi+J(z)n(z)/mi and vj by vj−J(z)n(z)/mj, and leaving all other coordinates unchanged. Denote this time-independent reset extension by R(z).

The functions γ,n,R are C1 on the open set dij≠0. For two states z,z′ with both pair distances at least σ>0 and both relative velocity norms at most V≥0, ∣γ(z)−γ(z′)∣≤2∥z−z′∥2,∥n(z)−n(z′)∥2≤22σ∥z−z′∥2, ∥R(z)−R(z′)∥2≤LR∥z−z′∥2,LR:=1+2 βκ(1+4Vσ). These pairwise bounds do not require a convex collision-free state set. Along a differentiable smooth segment with qk′=vk, ddtγ(z(t))=⟨n(z(t)),vi(t)−vj(t)⟩. The normal bound 2/σ applies to differences of the relative vectors dij; its full-state version includes the factor 2. This extension does not assert that an approximate state is exactly at contact or that an event exists.

Facts & Assumptions

Given: The stated pair, fixed masses/radii/restitution, two states with separated pair centers and bounded relative velocities, and the Euclidean full-state norm.

[F1]

The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn fixes the bilinear inner product and squared Euclidean norm.

[F3]

Impulse, momentum, and kinetic-energy laws for an isolated frictionless sphere impact supplies the impulse and equal/opposite binary velocity updates at an exact incoming contact.

[F5]

If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative: continuous first partial derivatives on an open set give total differentiability, with its derivative given by those partials.

Proof

1.1givenF1F2algebra

Write a=∥dij∥2 and a′=∥dij′∥2. By [F2], ∣a−a′∣≤∥dij−dij′∥2. Also ∥dij−dij′∥2≤∥qi−qi′∥2+∥qj−qj′∥2≤2∥q−q′∥2≤2∥z−z′∥2. Subtracting the fixed radii gives the guard bound.

2.1givenF2step 1.1algebra

The identity n−n′=(dij−dij′)/a+dij′(1/a−1/a′) and step 1.1 give ∥n−n′∥2≤∥dij−dij′∥2/a+∣a−a′∣/a≤2∥dij−dij′∥2/σ. Applying the full-state estimate from step 1.1 gives the asserted normal bound.

3.1givenF2F3step 1.1step 2.1algebra

Put w=vi−vj and w′=vi′−vj′. The impulse formula in [F3], used as the stated extension, gives ∣J−J′∣≤κ(∥w−w′∥2+∥w′∥2∥n−n′∥2)≤κ(2∥v−v′∥2+22Vσ∥q−q′∥2), and ∣J′∣≤κV. The two changed velocity increments have joint norm difference β∥Jn−J′n′∥2, which is at most β(∣J−J′∣+∣J′∣∥n−n′∥2).

4.1givenF2step 2.1step 3.1algebra

Combining steps 2.1–3.1 bounds the reset-increment difference by 2βκ(∥v−v′∥2+4V∥q−q′∥2/σ). Each coordinate-block norm is at most ∥z−z′∥2. The identity part of the reset contributes at most ∥z−z′∥2 by [F2], giving exactly the stated LR. This argument compares the two endpoints directly and uses no connecting line segment.

5.1givenF1F2F4F5algebra∎

For a nonzero vector d and increment h, rationalization gives ∥d+h∥2−∥d∥2=2⟨d,h⟩+∥h∥22∥d+h∥2+∥d∥2. The denominator tends to 2∥d∥2>0, so the total derivative is h↦⟨d/∥d∥2,h⟩, continuously dependent on d≠0. The coordinate rules in [F4] give continuous partial derivatives for the quotient defining n and the products defining R on this open set; [F5] makes them C1. Applying [F4] along dij′=vi−vj proves the guard derivative formula.

AlgorithmAlgorithm: AI-adaptedProof: Not applicableOpen item page →

Event-driven integration for isolated frictionless spherical impacts

Definition

Inputs. A dimension d≥1; P≥2 spheres with centers qi, velocities vi, masses mi>0, radii ri>0 and fixed restitution coefficients eij∈[0,1]; an initial state and horizon T>0; a positive time-bracket tolerance ϵtime, a separate positive guard-residual tolerance ϵguard, an event-separation bound δ>0, a certified finite event-count bound Nevt∈N, an event budget B∈N, an endpoint policy πT∈{include,pre-impact}, and a finite-budget certificate provider. The exact smooth-mode reference dynamics are qi′=vi,vi′=Fi(t,q,v), where F=(F1,…,FP) is a specified C1 force field on an open neighborhood of an admitted compact tube. The exact reference initial state is nonpenetrating: γij(0):=∥qi(0)−qj(0)∥2−ri−rj≥0 for every pair. A completed provider must certify that the exact reference states remain nonpenetrating on each smooth segment and after every exact reset; a failed or undecidable nonpenetration check returns unresolved. Throughout each certified incoming/outgoing tube every pair distance is at least a stated σ>0. The provider supplies finite relative-velocity bounds V and state/field bounds wherever they are used below.

The provider is an explicit admissible input, not an automatically constructed oracle for arbitrary C1 fields. It must supply the following valid data, with any failed or undecidable certificate test returning unresolved.

  1. From the last reported reset time t∗, supply a continuous accumulated dense reconstruction U. For a selected event with bracket [a,b], let X− be the exact incoming smooth-mode continuation launched from the aligned reference state at t∗, and let X~− be the exact solution of the same smooth field launched from the reported state there. Certify both continuations through b, including the part after the true event τ. Supply E≥∥X~−(t∗)−X−(t∗)∥2 (initially E=0) and a uniform bound ∥U(t)−X~−(t)∥2≤ηloc for every t∈[t∗,b]. With H=b−t∗, supply a state-Lipschitz constant L and the common solution/tube hypotheses of A Lipschitz ODE mode flow is stable to its initial state on a tube on this whole interval, and use ηref=ηloc+eLHE as the uniform bound relative to X− through b. In a certified no-event branch replace b by T. A finite cover of certified convex mode tubes may be used with its propagated bounds. A Jacobian bound on a nonconvex compact set alone is not a substitute. The continuation X− agrees with the incoming reference path up to τ; after τ it is an auxiliary smooth trajectory, not the reset hybrid path. It need not be nonpenetrating after τ, but must satisfy the stated separation and field/tube bounds.

  2. For every pair i<j, exact-reference guard enclosures for γij(t)=∥qi(t)−qj(t)∥2−ri−rj, and a certificate covering the whole physical smooth prefix from t∗ through the next reference event, or through T if there is no next event, that proves γij≥0 throughout and accounts for every possible zero. Every zero is either the just-processed segment-start root for that pair (which may be ignored once) or a candidate root bracket satisfying item 3; any other possible zero, including a grazing or zero-speed zero, or any possible negative guard value returns unresolved. At the initial simulation time, a zero must be processed as an enabled incoming root or the result is unresolved. Thus a no-event result requires certified nonpenetration and exclusion of every unlisted zero over the whole interval, not merely exclusion of incoming roots. A sufficient explicit sampling assumption may replace a range cover only when its stated variation/domain assumptions justify the same exclusion. Endpoint signs or an unsuccessful sign scan alone do not certify absence. Dense-guard enclosures must include the state-error inflation 2ηref as well as guard-evaluation and rounding error; the bound follows from Sphere-contact guards, normals and binary resets have explicit tube bounds. For candidate localization these dense enclosures refer to X− from item 1. The nonpenetration requirement concerns the physical reference hybrid path; it does not prohibit a negative incoming-continuation guard after its first event. Require the selected continuation root to match the earliest unprocessed physical reference event.

  3. For each candidate event, a bracket t∗≤a≤b≤T containing exactly one root τ of the selected incoming-continuation guard γij−(t)=∥qi−(t)−qj−(t)∥2−ri−rj, with b−a≤ϵtime and b−a<δ/3. On the entire bracket, certify the incoming inequality γ˙ij−(t)≤−ν<0, not just a derivative value at its root. Supply disjoint ordering certificates identifying the unique earliest event among all pairs. If b=T, certify whether the exact root is τ=T; an undecided endpoint equality returns unresolved. A grazing/uncertain derivative, ambiguous overlap or simultaneous multi-contact is unresolved; lexicographic inspection does not settle physical simultaneous impacts.

  4. At τ^=b, a certified bound ϵobs≥∣γij(τ^,U(τ^))∣ with ϵobs≤ϵguard. The provider includes all evaluation errors in this bound. If a=b, the root certificate gives τ=a=b; set the lag bound Δ=0. If a<b, set Δ:=min⁡{b−a,2ηref+ϵobsν}, the nonnegative lag bound supplied by A transverse hybrid event time is stable under dense-output and root error using the continuation bound from item 1 on the whole bracket. Require certified bounds M−,M+ for the incoming/outgoing fields through this lag, and all remaining reset-domain and common outgoing solution/tube hypotheses of Reset and smooth-mode flow propagate a transverse event-time error. Include the incoming continuation through b in these checks. For the selected pair use the state-reset bound LR from Sphere-contact guards, normals and binary resets have explicit tube bounds, with a velocity bound valid for both compared reset inputs. This reset has no explicit time dependence. If the reset formula is evaluated inexactly, the computed full-state output R^(U(b)) must come with a separate ϵR≥0 satisfying ∥R^(U(b))−R(U(b))∥2≤ϵR, where the norm is on the full state (q,v); for an exact reset set ϵR=0.

  5. A certificate that the matched isolated exact events have separation at least δ and count at most Nevt under the input endpoint policy. For an exact event at T, policy include processes the reset and counts it; policy pre-impact reports the endpoint before reset and excludes that endpoint event from the processed-event count. Process an initial enabled root at most once. Missing endpoint/count/separation bookkeeping is unresolved. In particular e=0 does not establish another isolated transverse event after the reset.

Procedure. Initialize the current reported time t∗=0, current state to the input initial state, aligned-start error E=0, accepted-event count j=0, and an empty output ledger. While t∗<T, request the provider certificates for every unordered pair on the entire remaining horizon [t∗,T], inspecting the pair list in increasing lexicographic order. If the provider certifies no further zero except the permitted just-processed segment-start root, with nonpenetration and no unlisted zero through T, append the segment, its error bound and certificates, and return complete. Otherwise select the certified unique earliest pair and its bracket [a,b], with upper endpoint τ^=b. If the provider certifies τ=T and πT=pre-impact, append the incoming segment through T and return complete with the pre-impact endpoint; do not apply a reset or increment j. If j≥B or j≥Nevt, return unresolved with the certified partial trajectory. Otherwise evaluate the binary impulse formula of Impulse, momentum, and kinetic-energy laws for an isolated frictionless sphere impact as the smooth reset extension at U(b); keep positions fixed and update only the selected two velocities. The impulse theorem's exact contact/momentum/restitution/energy laws concern the reference exact incoming contact. A reported approximate state is not asserted to be exactly at contact; its reset error is recorded.

By Reset and smooth-mode flow propagate a transverse event-time error, set the next aligned reset-state error bound to E←LRηref+(LRM−+M+)Δ+ϵR. The outgoing M+Δ term accounts for the reference trajectory's flow from its earlier true reset to the reported time. Append the reported reset, set t∗←b, update the current reported state and set j←j+1. Restart the smooth integrator at b, discard the previous local reconstruction, and start the next accumulated dense-error ledger. If t∗=T, return complete with the endpoint reset included. Otherwise repeat the loop. These recurrences compare only matched smooth-mode prefixes and post-reset states at aligned times; they make no same-clock state-error assertion between an exact jump and its later reported jump.

Output complete with the certified trajectory, event brackets, error ledger and certificates, or unresolved with the certified prefix. If an endpoint root is included, it is counted under Nevt and must fit within B. Any missing continuation/error, enclosure, margin, ordering, separation/count or restart certificate, failed reset domain, or depleted provider budget returns unresolved without an event-absence claim. To allocate a slot for every certified event under the selected endpoint policy, choose B≥Nevt.

Enumerate every unordered pair once per smooth segment. Root-solve guard evaluations, dense reintegration and restart-error calculation are charged separately from one inspection per pair. No neighbor-search acceleration, frictional solver, or simultaneous-contact solver is specified.

Remarks

The general mode/guard/reset terminology is Smooth hybrid ODE modes, guards, resets, and deterministic event priority. For each pair transition declare crossing orientation σij=−1, so the incoming bracket condition γ˙ij≤−ν is exactly σijγ˙ij≥ν. If one full mode graph is required, use an initial label m0 and one label mij for each unordered contact pair, all carrying the identical smooth field. From every label, include a transition to each mij carrying that pair's guard and reset; this includes a self-transition at mij. Start in m0. Simultaneous or ambiguous roots remain unresolved, so the graph imposes no physical priority rule. This avoids assigning many distinct guards to one self-transition. The four general interfaces used here apply to explicitly supplied valid dense/error and interval certificates. The event page's rational residual-checker construction is one sufficient provider branch; this procedure does not import that construction as an evaluator for every C1 force or an irrational reported reset state.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Projected contact dynamics and explicit projection Euler step

Definition

Let d≥1, let C⊆Rd be nonempty, closed, and convex, and let PC(y) be the unique nearest point in C to y, whose existence and uniqueness are Every point has a unique nearest point in a nonempty closed Euclidean convex set. For x∈C, set NC(x)={n∈Rd:⟨n,z−x⟩≤0 for every z∈C}; for x∉C, set NC(x)=∅. On C this is the outward normal cone of Scaled KKT residual and convex normal cone. The projection variational inequality of Metric projection onto a closed convex set satisfies the variational inequality says PC(y)=p exactly when p∈C and y−p∈NC(p).

For T>0, a solution of the projected contact dynamics with forcing f:[0,T]×C→Rd and initial state x0∈C is an absolutely continuous map x:[0,T]→C satisfying f(t,x(t))−x˙(t)∈NC(x(t))for almost every t∈[0,T]. Equivalently, x˙(t)+NC(x(t))∋f(t,x(t)). For an integer N≥1, put h=T/N, tk=kh, and define the exact explicit projection Euler nodes by xk+1=PC(xk+hf(tk,xk)),k=0,…,N−1, starting from x0. Its affine interpolant joins consecutive nodes linearly on each interval [tk,tk+1].

For a map x:[0,T]→Rd, absolutely continuous means that each coordinate is absolutely continuous in the scalar sense of Absolute continuity on a compact interval, and x˙(t) is the vector of coordinate derivatives, from The derivative f′(c)=lim⁡x→cf(x)−f(c)x−c of f:A→R at a point c∈A that is a limit point of A, and differentiability on a set, wherever they all exist. The solution condition requires a Lebesgue-null set N⊆[0,T] such that for every t∉N all coordinate derivatives exist and the displayed inclusion holds. Here almost every t is relative to Lebesgue measure λ from Lebesgue measurable sets, the family L(Rn), and the restricted set function λn, with the convention of Measure-null sets and almost-everywhere statements relative to a measure.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Naive all-pairs sphere-contact search has quadratic work

Statement

For P≥2 spheres, the naive search that evaluates every unordered pair guard exactly once per smooth segment performs P(P−1)/2 pair-guard evaluations. Thus it uses O(P2) pair checks; this count excludes the cost of each certified event solve, dense reintegration, and restart-error certificate. With zero or one sphere the pair list is empty, but the event-driven algorithm is defined for P≥2.

Facts & Assumptions

Given: The pair-enumeration loop of Event-driven integration for isolated frictionless spherical impacts and the particle count P∈N.

[F1]

Event-driven integration for isolated frictionless spherical impacts: on each smooth segment, the naive search inspects each unordered pair i<j once; event-certificate solves and reintegration are charged separately.

[F2]

Laws of finite sums and finite products: finite sums split and telescope, and The principle of mathematical induction supplies induction on P.

Proof

1.1F1given

For each lower index i=1,…,P−1, the loop tests exactly P−i higher indices. Every unordered pair has a unique smaller index, so these sets of tests are disjoint and include every pair once. The count is therefore ∑i=1P−1(P−i).

2.1F2step 1.1givenalgebrainduction∎

Reindexing by r=P−i gives ∑r=1P−1r. This sum is P(P−1)/2: it is 0 for P=0 and P=1, and increasing P to P+1 adds exactly P, which changes P(P−1)/2 to P(P+1)/2; induction gives the formula. For every P≥2, it is at most P2/2, proving the stated O(P2) bound.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

The convex normal-cone operator is maximal monotone and its resolvent is projection

Statement

Let C⊆Rd be nonempty, closed, and convex, and let NC have the convention of Projected contact dynamics and explicit projection Euler step. In dimension d=0, interpret this convention directly as C=R0={0}, NC(0)={0}, and PC(0)=0. An operator A:Rd⇉Rd is monotone if ⟨u−v,x−y⟩≥0 for all u∈A(x) and v∈A(y); it is maximal monotone if its graph has no proper monotone graph extension. Then NC is maximal monotone. For every τ>0 and y∈Rd, there is a unique p with y−p∈τNC(p), and that point is PC(y). Equivalently, (I+τNC)−1=PC.

Facts & Assumptions

Given: The set C and normal-cone convention in the Statement, and a scalar τ>0.

[F1]

Scaled KKT residual and convex normal cone and Projected contact dynamics and explicit projection Euler step: for x∈C, NC(x)={n:⟨n,z−x⟩≤0 for every z∈C}; outside C, the operator is empty.

[F2]

Extended-real indicator of a set: ιC is 0 on C and +∞ outside C.

[F3]

Subdifferentials of proper extended-real convex functions: for proper convex g and x∈dom⁡g, p∈∂g(x) means g(z)≥g(x)+⟨p,z−x⟩ for every z; if x∉dom⁡g, then ∂g(x)=∅.

[F4]

Existence, resolvent characterization, and firm nonexpansiveness of the proximal map: for proper closed convex g and τ>0, u=prox⁡τg(y) iff (y−u)/τ∈∂g(u).

[F5]

The proximal map of an indicator is Euclidean projection: the indicator of this nonempty closed convex set is proper, closed, and convex, and prox⁡τιC(y)=PC(y), the unique nearest point.

Proof

1.1F1givenalgebra

Let n∈NC(x) and m∈NC(y). Testing the definition in [F1] with z=y and z=x gives ⟨n,y−x⟩≤0 and ⟨m,x−y⟩≤0. Adding and changing signs yields ⟨n−m,x−y⟩≥0. Thus NC is monotone.

1.2F1F2F3F5given

The indicator is proper, closed, and convex by [F5], and its domain is C by [F2]. At x∈C, [F2]–[F3] show p∈∂ιC(x) exactly when ⟨p,z−x⟩≤0 for every z∈C; inequalities for z∉C are automatic because ιC(z)=+∞. At x∉C, both ∂ιC(x) and NC(x) are empty. Hence ∂ιC=NC.

2.1F4F5step 1.1step 1.2givenalgebra

Given any y∈Rd, put p=PC(y)=prox⁡τιC(y) by [F5]. By [F4] and step 1.2, (y−p)/τ∈NC(p), so y−p∈τNC(p). If also y−q∈τNC(q), monotonicity [step 1.1] gives 0≤⟨(y−p−y+q)/τ,p−q⟩=−∥p−q∥22/τ, hence p=q. Therefore the resolvent exists uniquely at every y and equals PC.

3.1step 2.1givenalgebra∎

Suppose (x,v) is monotonically related to the graph of NC, so ⟨v−n,x−y⟩≥0 for every n∈NC(y). Apply step 2.1 to x+τv to obtain p and n=(x+τv−p)/τ∈NC(p). Then x−p=τ(n−v), and the relation gives 0≤⟨v−n,x−p⟩=−τ∥v−n∥22. Thus v=n and x=p, so (x,v) already lies in the graph. Every monotone extension adds no point; NC is maximal monotone.

AlgorithmAlgorithm: AI-adaptedProof: Not applicableOpen item page →

Projected Euler with certified inexact projection solves

Definition

Input a nonempty compact, closed, and convex set C⊆Rd, d≥1, an exact force evaluator f:[0,T]×C→Rd, T>0, integer step count N≥1, initial state x0∈C, tolerances εk≥0, finite budgets Bk∈N for k=0,…,N−1, and a projection-certificate provider S. The explicit closedness condition matches Projected contact dynamics and explicit projection Euler step. An admissible provider, queried with (C,y,ε,B), must return after at most B candidate checks, in either case: unresolved or certified(p,\Pi) with a finite exact certificate Π proving p∈C and

sup⁡z∈C⟨y−p,z−p⟩≤ε2.

Set h=T/N, tk=kh, and start with the given x0. For k=0,…,N−1, form yk=xk+hf(tk,xk) and call S(C,yk,εk,Bk). If the response is unresolved or is not a sound certified(p,\Pi) response of the stated form, stop and return unresolved with the valid prefix x0,…,xk. Otherwise set xk+1=p and continue. After all N calls succeed, return complete, the nodes, their affine interpolant, and the per-step tolerances. The procedure assumes exact force evaluations and sound exact certificates; arithmetic and force-evaluation errors are not included. For exact projection-Euler requests, set every εk=0 and require the same residual certificate of A certified projection variational residual bounds the projection error.

Allow at most N provider calls, and enforce each call's stated finite candidate-check budget. Failure to certify a projection is reported; no convergence or accuracy is inferred from an unverified stopping tolerance. The provider is an explicit input: this definition does not construct a solver for arbitrary compact convex sets.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Solutions of projected contact dynamics are unique under the inherited choice assumptions

Statement

Assume Countable Choice and Dependent Choice. Let d∈N and T>0, let C⊆Rd be nonempty, closed, and convex, and let f:[0,T]×C→Rd satisfy ∥f(t,x)−f(t,y)∥2≤L∥x−y∥2 for all t,x,y, with L≥0. Any two absolutely continuous solutions of the projected dynamics of Projected contact dynamics and explicit projection Euler step with the same initial state agree on [0,T]. For d=0, extend the solution convention directly: C=R0={0}, NC(0)={0}, and a solution is the sole map x(t)=0.

Facts & Assumptions

Given: Countable Choice, Dependent Choice, the set and forcing, and two absolutely continuous solution maps in the Statement.

[A1]

The Axiom of Countable Choice (ACω) is inherited through [F4]'s absolutely-continuous FTC.

[F1]

For d≥1, Projected contact dynamics and explicit projection Euler step: a solution satisfies f(t,x(t))−x˙(t)∈NC(x(t)) for almost every t.

[F2]

The convex normal-cone operator is maximal monotone and its resolvent is projection: if nx∈NC(x) and ny∈NC(y), then ⟨nx−ny,x−y⟩≥0.

[F3]

Gronwall's integral inequality with variable and constant coefficients: if continuous u≥0 satisfies u(t)≤u(0)+∫0t2Lu(s) ds, then u(t)≤u(0)e2Lt.

[F4]

The product of two absolutely continuous functions is absolutely continuous and Fundamental theorem of calculus for absolutely continuous functions: products of absolutely continuous real functions are absolutely continuous with the ordinary product derivative almost everywhere, and the integral of that derivative is the endpoint difference.

[F6]

The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn: R0 is the singleton zero vector space, with zero inner product and norm.

Proof

1.1F6given

If d=0, then C={0} and both solution maps are identically zero. Coordinatewise absolute continuity and differentiation are vacuous, and the inclusion is 0∈NC(0)={0}, so this agrees with the extended convention and uniqueness holds.

1.2F1F2given

Assume d≥1 and let x,y be the two solutions and define nx=f(t,x)−x˙ and ny=f(t,y)−y˙ at almost every time where both inclusions hold. By [F1] these belong to NC(x) and NC(y); [F2] gives ⟨nx−ny,x−y⟩≥0.

2.1A1A2F1F2F3F4F5step 1.2givenalgebra∎

The function u(t)=∥x(t)−y(t)∥22 is absolutely continuous by [F4]. At almost every t, [F1] and step 1.2 give u′(t)=2⟨x˙−y˙,x−y⟩=2⟨f(t,x)−f(t,y),x−y⟩−2⟨nx−ny,x−y⟩≤2Lu(t), using the Lipschitz hypothesis and [F5]. Since u(0)=0, [F4] integrates this differential inequality to u(t)≤∫0t2Lu(s) ds. Applying [F3] gives u(t)=0 for every t, so x=y. This argument uses no choices beyond the two axioms already required by [F4].

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Existence and uniqueness for projected dynamics and convergence of projection Euler under countable and dependent choice

Statement

Let d≥1, let C⊆Rd be nonempty, compact, and convex, let T>0, and let x0∈C. Suppose f:[0,T]×C→Rd is Lipschitz in the explicit sense ∥f(t,x)−f(s,y)∥2≤L(∣t−s∣+∥x−y∥2) for some L≥0 and all s,t,x,y. Assume the Axioms of Countable Choice and Dependent Choice. Then the projected inclusion x(0)=x0,f(t,x(t))−x˙(t)∈NC(x(t))for almost every t∈[0,T] has a unique absolutely continuous solution x:[0,T]→C. For each integer N≥1, define h=T/N, tk=kh, and the exact projection Euler nodes by xk+1=PC(xk+hf(tk,xk)),k=0,…,N−1. Their affine interpolants converge uniformly to x as N→∞. Countable Choice is used for the almost-everywhere statements and null-set unions; Dependent Choice enters through the absolutely-continuous FTC supplier used in the integrated proof. The monotonicity estimate for uniqueness makes no additional choices.

Facts & Assumptions

Given: Countable Choice, Dependent Choice, the set, forcing, and initial state in the Statement.

[A1]

The Axiom of Countable Choice (ACω): every countable family of nonempty sets has a choice function. It is used by the differentiability, Lebesgue-differentiation, and null-union suppliers below.

[A2]

The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain: every serial relation on a nonempty set admits an infinite dependent sequence. It is inherited through [F7]'s absolutely-continuous FTC.

[F1]

Projected contact dynamics and explicit projection Euler step: PC is the unique nearest-point projection, NC has the outward convention, and the exact projection Euler recurrence and affine interpolation are as in the Statement.

[F3]

Compactness of equi-Lipschitz curves with values in a compact Euclidean set: a sequence of uniformly Lipschitz curves into compact closed C has a uniformly convergent subsequence with limit in C.

[F4]

Solutions of projected contact dynamics are unique under the inherited choice assumptions: under Countable Choice and Dependent Choice, for a forcing Lipschitz in x, any two absolutely continuous solutions with the same initial state agree.

[F7]

The product of two absolutely continuous functions is absolutely continuous and Fundamental theorem of calculus for absolutely continuous functions: under Countable Choice and Dependent Choice, for an absolutely continuous vector curve, Φz(x)=⟨x,z⟩−12∥x∥22 is absolutely continuous, has derivative ⟨x˙,z−x⟩ almost everywhere, and its derivative integrates to its endpoint difference.

[F8]

A locally integrable function on Rn and Lebesgue differentiation theorem on Rn: for a locally Lebesgue-integrable function on R, at almost every t the averages (2r)−1∫t−rt+rg(s) ds tend to g(t) as r↓0; the theorem assumes Countable Choice.

[F9]

Q is countably infinite gives a bijection N→Q, and N×N≈N gives a bijection J:N2→N.

[F10]

The recursion theorem and The principle of mathematical induction allow the finite iterated pairing construction on Nd; The rationals embed densely in the reals gives rational approximants to each real coordinate; and Cauchy-Schwarz ∣⟨x,y⟩∣≤∥x∥2∥y∥2 with its equality case, the triangle inequality for ∥⋅∥2, the parallelogram law and polarisation gives the finite-sum Euclidean norm formula used to bound a vector from its coordinate errors.

[F11]

A property holding outside a set of elementary measure zero is exactly a property holding λ-almost everywhere identifies covering nullity with Lebesgue nullity under Countable Choice; A countable union of measure-zero sets has measure zero, by countable choice then shows that a countable union of Lebesgue-null subsets of R is null.

Proof

1.1F1F2F5givenalgebra

Since d≥1, [F5] shows that compact C is closed and bounded. Along with the stated nonemptiness and convexity, this verifies the set hypotheses in [F1] and the projection suppliers before they are used. Boundedness gives a finite diameter bound D for C. Put M=∥f(0,x0)∥2+L(T+D); the Lipschitz hypothesis gives ∥f(t,x)∥2≤M on [0,T]×C. For each exact Euler step, PC(xk)=xk, so [F2] gives ∥xk+1−xk∥2≤h∥f(tk,xk)∥2≤hM. Convexity keeps the affine interpolant in C, and its slope on each step has norm at most M.

1.2F1givenalgebra

On each open mesh cell [tk,tk+1), write Xh for the affine interpolant, Xˉh=xk+1, Fh=f(tk,xk), and nh=Fh−X˙h=(xk+hFh−xk+1)/h. By the projection variational inequality in [F1], nh∈NC(Xˉh). Consequently, for every fixed z∈C, ⟨X˙h−Fh,z−Xˉh⟩≥0.

2.1A1F3F6step 1.1given

Apply [F3] to the sequence of interpolants for N=1,2,…. Along a subsequence Nj→∞, they converge uniformly to a map x:[0,T]→C with x(0)=x0 and Lipschitz constant M. By [F6], x is absolutely continuous and differentiable almost everywhere; at each differentiability point, the Lipschitz inequality implies ∥x˙(t)∥2≤M.

3.1A1A2F1F6F7step 2.1step 1.2givenalgebra

Fix 0≤a<b≤T and a fixed z∈C. We have ∥Xˉh−Xh∥2≤Mh and ∥X˙h−Fh∥2≤2M, so replacing Xˉh by Xh in the integral of step 1.2 changes it by at most 2M2h(b−a). The term with X˙h is the endpoint difference of Φz(Xh), where Φz(w)=⟨w,z⟩−12∥w∥22. Uniform convergence gives its limit as the endpoint difference of Φz(x); [F7] identifies that difference with ∫ab⟨x˙,z−x⟩. Also ∥Fh(t)−f(t,x(t))∥2≤L(h+Mh+∥Xh−x∥∞) on each mesh cell, so Fh→f(t,x(t)) uniformly along the selected subsequence. Passing to the limit in the integrated inequality yields ∫abgz(t) dt≥0,gz(t):=⟨x˙(t)−f(t,x(t)),z−x(t)⟩.

4.1A1F7F8step 3.1givenalgebra

The function gz is Lebesgue-integrable: [F7] gives a measurable L1 version of x˙; define it to be 0 where the derivative is undefined. Boundedness of f,x,z makes the other factors integrable. Extend this representative of gz by zero outside [0,T] to obtain a locally integrable function on R. Since every interval integral in step 3.1 is nonnegative, Gz(t)=∫0tgz(s) ds is nondecreasing. At almost every interior t, [F8] gives lim⁡r↓012r∫t−rt+rgz(s) ds=gz(t). For every sufficiently small r>0, the average on the left is (Gz(t+r)−Gz(t−r))/(2r)≥0 because Gz is nondecreasing. Taking the limit yields gz(t)≥0 almost everywhere for each fixed z∈C.

5.1A1F1F2F9F10F11step 4.1givenchoose

Fix a bijection ρ:N→Q from [F9]. Define π1(n1)=n1 and, recursively, πk+1(n1,…,nk+1)=J(πk(n1,…,nk),nk+1). Since J is a bijection, induction using [F10] shows that each πk:Nk→N is a bijection. In particular, decoding n by πd−1 and applying ρ coordinatewise gives a surjection s:N→Qd. Thus D0={PC(s(n)):n∈N} is countable. It is dense in C: for z∈C and η>0, choose in each of the finitely many coordinates a rational qj strictly between zj−η/(2d) and zj+η/(2d), using the interval-density conclusion of [F10]. For q=(q1,…,qd), [F10] gives ∥q−z∥22=∑j<d∣qj−zj∣2<d(η2d)2≤η24, so ∥q−z∥2<η/2. Since PC(z)=z, nonexpansiveness [F2] gives ∥PC(q)−z∥2=∥PC(q)−PC(z)∥2≤∥q−z∥2<η. For each n, put zn=PC(s(n))∈D0. Step 4.1 gives a null exceptional set where gzn<0. Countable Choice [A1] and [F11] make their union, together with the null set where x˙ does not exist, null. Outside it, gz(t)≥0 for every z∈D0. For each such t, the expression gz(t) is continuous in z; if it were negative at some z∈C, it would be negative on a neighborhood of z meeting the dense set D0, a contradiction. Hence the inequality holds for every z∈C, so f(t,x(t))−x˙(t)∈NC(x(t)) almost everywhere by [F1]. This proves existence of a solution along the selected subsequence.

6.1A1A2F3F4step 2.1step 1.2step 5.1givenassume-hypcontradiction∎

The uniqueness lemma [F4], under the same choice assumptions through its FTC supplier, shows that every uniformly convergent subsequence limit of the Euler interpolants is this same solution x. If the full sequence did not converge uniformly to x, some subsequence would stay at uniform distance at least δ>0; [F3] would give a further uniformly convergent subsequence, whose limit is a solution by steps 1.2–5.1 and hence equals x, a contradiction. Therefore the entire sequence converges uniformly to x.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

A square-root global error bound for projected Euler with certified projection tolerances

Statement

Assume the hypotheses of Existence and uniqueness for projected dynamics and convergence of projection Euler under countable and dependent choice, including Countable Choice and Dependent Choice, and let x be its unique solution. Let D be any finite bound for the diameter of C, set M=∥f(0,x0)∥2+L(T+D),C0=8M2+L2(1+M)2T,Kerr=C0Te(2L+1)T. For h=T/N, let Xh be the affine interpolant of the exact projection Euler recurrence. If a complete run of Projected Euler with certified inexact projection solves returns nodes x~k with certified residuals sup⁡z∈C⟨x~k+hf(tk,x~k)−x~k+1,z−x~k+1⟩≤εk2, and X~h is their affine interpolant, then sup⁡0≤t≤T∥X~h(t)−x(t)∥2≤Kerrh+eLT∑k=0N−1εk. In particular, the exact-projection branch has uniform error O(h). Certified projection errors with ∑kεk=O(h) retain that rate; no rate follows from an uncertified solver tolerance alone.

Facts & Assumptions

Given: The data, Countable Choice and Dependent Choice assumptions of Existence and uniqueness for projected dynamics and convergence of projection Euler under countable and dependent choice, and a completed inexact projected-Euler run with the residual certificates in the Statement.

[A1]

The Axiom of Countable Choice (ACω) is assumed as in [F1] to obtain the exact solution x; the estimates use no additional countable choices.

[A2]

The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain is assumed as in [F1] to obtain the exact solution x; the estimates use no additional dependent choices.

[F1]

Existence and uniqueness for projected dynamics and convergence of projection Euler under countable and dependent choice: there is a unique absolutely continuous x satisfying f(t,x)−x˙∈NC(x) almost everywhere.

[F4]

A certified projection variational residual bounds the projection error: a feasible candidate with variational residual at most ε2 is within distance ε of its exact projection.

[F5]

Projected Euler with certified inexact projection solves: a completed run returns feasible nodes with the residual certificates specified in the algorithm Definition.

[F7]

The product of two absolutely continuous functions is absolutely continuous and Fundamental theorem of calculus for absolutely continuous functions: products of AC components are AC with the product derivative a.e., and the derivative integrates to the endpoint difference.

[F10]

Gronwall's integral inequality with variable and constant coefficients: if u≥0 is continuous and u(t)≤A+∫0tbu for constants A,b≥0, then u(t)≤Aebt.

[F11]

Projected contact dynamics and explicit projection Euler step: the outward cone is NC(x)={n:⟨n,z−x⟩≤0 for every z∈C}, and an exact projection step satisfies xk+1=PC(xk+hf(tk,xk)).

Proof

1.1A1A2F1F3F6F8F11F12givenchoosealgebra

By [F12], compactness makes C closed, so the projection and normal-cone hypotheses in [F11] and [F3] apply to the stated set. Let Xh be the exact affine Euler interpolant, Xˉh(t)=xk+1 on [tk,tk+1), Fh(t)=f(tk,xk), and nh=Fh−X˙h. The projection variational inequality in [F11] gives nh(t)∈NC(Xˉh(t)). Nonexpansiveness [F3] gives ∥X˙h∥2≤M and ∥Xˉh−Xh∥2≤hM, so ∥nh∥2≤2M. For the exact solution put n(t)=f(t,x(t))−x˙(t)∈NC(x(t)). At almost every differentiability point, x(t+s)∈C on both sides of t; the normal inequality with z=x(t+s), divided by positive and negative s and passed to the limit, gives ⟨n(t),x˙(t)⟩=0. Hence ∥x˙(t)∥22=⟨f(t,x(t)),x˙(t)⟩, so Cauchy–Schwarz [F8] gives ∥x˙(t)∥2≤M and ∥n(t)∥2≤2M.

1.2F3F4F5F9givenalgebrainduction

By [F4] and [F5], each inexact node is within εk of the exact projection of its own unprojected input. Comparing it with the exact node and using [F3] and the state-Lipschitz bound gives ∥x~k+1−xk+1∥2≤(1+hL)∥x~k−xk∥2+εk. Iteration from the common initial point yields max⁡k∥x~k−xk∥2≤(1+hL)N∑kεk. By [F9], (1+hL)N≤eNhL=eLT.

2.1F1F2F6F7F8step 1.1givenalgebra

Put eh=Xh−x and Eh=∥eh∥22. By [F6]–[F7], Eh is absolutely continuous and Eh′=2⟨X˙h−x˙,eh⟩ almost everywhere. Monotonicity [F2] at Xˉh and x gives ⟨nh−n,Xˉh−x⟩≥0. Since ∥Xˉh−Xh∥2≤hM and ∥nh−n∥2≤4M, differentiation yields 12Eh′≤LEh+Lh(1+M)Eh+4M2h. Indeed, ∥Fh−f(t,x)∥2≤L(h+∥xk−x(t)∥2)≤L(∥eh∥2+h(1+M)) using the within-step displacement bound; [F8] bounds its inner product with eh.

3.1F7F10step 2.1givenalgebra

Since (Eh−Lh(1+M))2≥0, we have Lh(1+M)Eh≤12Eh+12L2(1+M)2h2. Thus Eh′≤(2L+1)Eh+8M2h+L2(1+M)2h2≤(2L+1)Eh+C0h, since h≤T. Integrating the inequality and using Eh(0)=0 gives Eh(t)≤C0hT+(2L+1)∫0tEh(s) ds. By [F10], sup⁡tEh(t)≤C0hTe(2L+1)T, hence sup⁡t∥Xh(t)−x(t)∥2≤Kerrh.

4.1step 3.1step 1.2givenalgebra∎

On each mesh cell, X~h−Xh is the affine interpolation of its endpoint errors, so its norm is at most the larger endpoint norm. The triangle inequality with step 3.1 gives sup⁡t∥X~h(t)−x(t)∥2≤Kerrh+eLT∑kεk, which is the claimed estimate. If εk=0 all k, or if their sum is O(h) along a refining mesh, the stated O(h) rate follows.

5 · Examples, counterexamples and false statements

None yet.

Sources