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.
Nonsmooth contact time stepping and projections
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Absolute Continuity and the Sharp Fundamental Theorem of Calculus
- Adaptive ODE solvers and error estimation
- Areas of Elementary Plane Figures
- Banach-Space Differential Calculus and Banach Manifolds
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Bounded Variation and the Riemann–Stieltjes Integral
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Norms and Realification
- Complexification, Realification and Real Structures
- Connectedness
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Convergence: Nets and Filters
- Convex and Semicontinuous Functions on Rⁿ
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Density Separability and Convolution in Lᵖ
- Differentiation of Monotone Functions and the Vitali Covering Theorem
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Event location and hybrid trajectory error
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Probability and the Probabilistic Method
- Foundations of the Real Numbers for Analysis
- Fubini and Change of Variables
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inequality KKT duality and optimality certificates
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- One-step ODE Consistency and Local Error
- Order, Zorn's Lemma, and the Axiom of Choice
- Outer Measure and the Caratheodory Extension Theorem
- Outward rounded interval and ball arithmetic
- Picard-Lindelöf and First-Order Ordinary Differential Equations
- Pointwise Extended-Real Function Products
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Properties of the Integral and the Working FTC
- Proximal gradient and accelerated composite optimization
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Runge–Kutta Methods and Order
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Signed and Complex Measures Hahn and Jordan
- Simple Field Extensions and the Construction of the Complex Numbers
- Subspaces, Products, and Quotients
- Suprema and Infima
- The Analytic Hahn Banach Theorem
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Derivative and the Mean Value Theorems
- The Direct Method and Euler--Lagrange Equations
- The Exponential Function
- The Inverse and Implicit Function Theorems
- The Inverse Function Theorem Completed
- The Lebesgue Integral and the Convergence Theorems
- The Logarithm and General Powers
- The Lᵖ Spaces Holder Minkowski and Riesz Fischer
- The Maximal Function and Lebesgue Differentiation
- The Radon Nikodym Theorem and Lebesgue Decomposition
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Weak and Weak Star Topologies
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 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
Compactness of equi-Lipschitz curves with values in a compact Euclidean set
Statement
Let , , and let be nonempty, compact, and closed. Let . If satisfies then some subsequence converges uniformly to a map with the same Lipschitz bound.
Facts & Assumptions
Given: The set , interval , constant , and sequence of maps in the Statement. Compactness has its open-cover meaning; the Lipschitz inequality is displayed in the Statement.
Heine-Borel in : with the Euclidean metric a subset of 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 is bounded; Every complete ordered field is Archimedean: the natural numbers are cofinal in , so a bounded set is contained in a box for some integer .
The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement: a closed set has open complement; Open ball, closed ball and sphere in a metric space: every open neighborhood of a point contains an open ball about it.
Convergence of a sequence in a metric space: iff in : if a sequence converges to , then it is eventually in every open ball centered at .
The reals are complete: every Cauchy sequence of real numbers converges in .
The well-ordering principle and The recursion theorem: every nonempty subset of has a least element, and a uniquely specified recursive sequence on exists.
Integer part: for every real there is exactly one integer with : for each real there is an integer with .
Cauchy-Schwarz with its equality case, the triangle inequality for , the parallelogram law and polarisation: , each coordinate satisfies , and the Euclidean norm satisfies the triangle inequality.
The principle of mathematical induction: every finite initial segment of is finite.
Proof
By [F1], choose an integer with . For each natural , let and put . Let consist of the lattice points whose coordinates are with integers . 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 of coordinates shows their Cartesian product is finite. To verify its covering radius, fix . For each , [F6] applied to gives an integer with . Thus and , using for (from the power recursion and induction). The corresponding lattice point has in every coordinate, so [F8] gives and hence . Assign each value at each to the first lattice point within in a fixed ordering of . This gives one of finitely many patterns.
Starting from the positive index set , partition each infinite index set by the finitely many patterns at resolution . At least one class is infinite; choose the first such pattern in the fixed finite ordering and let be its infinite class. Then .
Set . For , recursively choose to be the least member of greater than . The infinite set is unbounded: if it were contained in some finite initial segment , that segment would be finite by [F9], contradicting that is infinite. Hence is nonempty, and [F5] supplies its least member. For every fixed , all with belong to , so the maps with those indices have the same resolution- pattern.
For and , choose with . At each lattice time, the common pattern assigns both values to the same lattice point, so the triangle inequality [F8] gives . Using the Lipschitz bounds and the triangle inequality again, By [F7], the right side tends to zero as , uniformly in , so is uniformly Cauchy.
At each , step 4.1 and [F8] make every coordinate sequence Cauchy; [F4] therefore gives a pointwise limit . Given , choose so , using [F7]. For every , step 4.1 gives for all and all . Passing to the coordinatewise limit in this finite sum yields , hence , uniformly in . Thus the subsequence converges uniformly. If , openness of the complement [F2] gives a ball about disjoint from , while convergence [F3] puts in that ball eventually, a contradiction. Thus . For fixed , coordinatewise convergence at those two points gives ; taking nonnegative square roots yields .
Projection onto a closed convex set is nonexpansive
Statement
Let , including . Let be nonempty, closed, and convex, and let denote the unique nearest point in to . Then
Facts & Assumptions
Given: The set and points in the Statement.
For , Metric projection onto a closed convex set satisfies the variational inequality: if , then for every .
The Euclidean inner product on : consists of its single zero vector, whose norm is .
Proof
If , then the nonempty set is , so is the constant zero map and the claimed inequality is .
Now assume . Put and . Applying [F1] first with and then with gives and . Therefore
By [F2], . If the result is immediate; otherwise divide by the positive number .
First-impact step for a one-dimensional unilateral contact
Definition
Input a gap , velocity , constant acceleration , step horizon , mass , restitution , and a candidate-root budget . Use exact real arithmetic and comparisons. Define and on . Return impact, free-flight, or unresolved by these instructions.
- If and , return
impactat with contact gap , , , and . - Otherwise form the complete candidate set of real roots of . If , set . If and , set . If , , and , set . If , put : for set ; for set ; and for set , with duplicate values removed. If , return
unresolved. From , retain exactly the values satisfying and , and order them increasingly. - If the retained list is nonempty, take its least value , set , , and , and return
impactwith time , contact gap , impulse , and post-impact velocity . - If the retained list is empty, compute the minimum of on by evaluating its two endpoints and, when and , its vertex . If this minimum is negative, return
unresolved; otherwise returnfree-flightwith endpoint and impulse .
The candidate set contains every root of the nonzero polynomial , 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.
Impulse, momentum, and kinetic-energy laws for an isolated frictionless sphere impact
Statement
Let two spheres of radii and masses have centers at contact, so . Let be the unit normal pointing from center to center . Suppose the pre-impact relative normal velocity is . For prescribed restitution , put Then , total linear momentum is conserved, the post-impact relative normal velocity is , each tangential velocity is unchanged, and where . 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.
The Euclidean inner product on : the Euclidean inner product is bilinear and symmetric, and .
Proof
Since , . Since and , . The impulse changes total momentum by .
Taking the relative normal component gives For either velocity, projection onto any vector orthogonal to is unchanged because the impulse term is parallel to .
Expanding the two squared norms with [F1] yields Substitute to obtain . Since , this is nonpositive; at it is the maximal loss in this law and at it is zero.
A certified projection variational residual bounds the projection error
Statement
Let , including . Let be nonempty, closed, and convex. If , , and satisfy then .
Facts & Assumptions
Given: The set , input , tolerance , and feasible candidate in the Statement.
For , Every point has a unique nearest point in a nonempty closed Euclidean convex set supplies the unique nearest point ; Metric projection onto a closed convex set satisfies the variational inequality gives for every .
The Euclidean inner product on : and its Euclidean norm and inner product are zero.
Proof
If , then , , and the residual supremum is ; the asserted distance is .
Now assume . Put and . The residual bound at gives . By [F1] with , . Since , this also gives .
Combining the two bounds yields . Both sides are nonnegative, so . This also covers .
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 be the reported gap (zero at an impact, the free-flight endpoint gap otherwise), let be the reported impulse, and let be the reported endpoint velocity. Then , , and . On a free-flight branch, and . On an impact branch at time , with incoming velocity , the post-impact velocity satisfies and When , the full resolved step has nonincreasing kinetic energy. For , 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.
First-impact step for a one-dimensional unilateral contact: an impact output has , , , and ; a free-flight output has , , and .
Proof
On an impact branch, [F1] gives , , and , since , , and . Hence . On a free-flight branch, [F1] gives and , so complementarity also holds.
On a free-flight branch, . On an impact branch, [F1] gives and . Therefore , using .
On an impact branch, [F1] gives , so the kinetic-energy difference is . If and the branch is free flight, and kinetic energy is unchanged; impact branches have the nonincrease just established. For nonzero , no claim is made about total free-flight work.
Sphere-contact guards, normals and binary resets have explicit tube bounds
Statement
Use the Euclidean norm on the full state of spheres in . Fix a pair , positive masses , positive radii , and a fixed restitution coefficient . Put Extend the binary reset formula of Impulse, momentum, and kinetic-energy laws for an isolated frictionless sphere impact to every state with by setting , replacing by and by , and leaving all other coordinates unchanged. Denote this time-independent reset extension by .
The functions are on the open set . For two states with both pair distances at least and both relative velocity norms at most , These pairwise bounds do not require a convex collision-free state set. Along a differentiable smooth segment with , The normal bound applies to differences of the relative vectors ; its full-state version includes the factor . 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.
The Euclidean inner product on fixes the bilinear inner product and squared Euclidean norm.
Cauchy-Schwarz with its equality case, the triangle inequality for , the parallelogram law and polarisation gives Cauchy–Schwarz, the Euclidean triangle inequality and norm homogeneity.
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.
The chain rule for total derivatives: and Sums, scalar multiples, products and quotients: , , , and when give the chain rule and the scalar coordinate sum, product and quotient rules with nonzero denominators.
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
Write and . By [F2], . Also . Subtracting the fixed radii gives the guard bound.
The identity and step 1.1 give . Applying the full-state estimate from step 1.1 gives the asserted normal bound.
Put and . The impulse formula in [F3], used as the stated extension, gives and . The two changed velocity increments have joint norm difference , which is at most .
Combining steps 2.1–3.1 bounds the reset-increment difference by . Each coordinate-block norm is at most . The identity part of the reset contributes at most by [F2], giving exactly the stated . This argument compares the two endpoints directly and uses no connecting line segment.
For a nonzero vector and increment , rationalization gives The denominator tends to , so the total derivative is , continuously dependent on . The coordinate rules in [F4] give continuous partial derivatives for the quotient defining and the products defining on this open set; [F5] makes them . Applying [F4] along proves the guard derivative formula.
Event-driven integration for isolated frictionless spherical impacts
Definition
Inputs. A dimension ; spheres with centers , velocities
, masses , radii and fixed restitution coefficients
; an initial state and horizon ; a positive time-bracket
tolerance , a separate positive guard-residual tolerance
, an event-separation bound , a certified
finite event-count bound , an event budget
, an endpoint policy ,
and a finite-budget certificate provider. The exact smooth-mode reference dynamics are
where is a specified force field on an open
neighborhood of an admitted compact tube. The exact reference initial state is
nonpenetrating: 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 .
The provider supplies finite relative-velocity bounds and state/field bounds
wherever they are used below.
The provider is an explicit admissible input, not an automatically constructed
oracle for arbitrary fields. It must supply the following valid data,
with any failed or undecidable certificate test returning unresolved.
-
From the last reported reset time , supply a continuous accumulated dense reconstruction . For a selected event with bracket , let be the exact incoming smooth-mode continuation launched from the aligned reference state at , and let be the exact solution of the same smooth field launched from the reported state there. Certify both continuations through , including the part after the true event . Supply (initially ) and a uniform bound for every . With , supply a state-Lipschitz constant 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 as the uniform bound relative to through . In a certified no-event branch replace by . 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 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.
-
For every pair , exact-reference guard enclosures for , and a certificate covering the whole physical smooth prefix from through the next reference event, or through if there is no next event, that proves 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 isunresolved. 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 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 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. -
For each candidate event, a bracket containing exactly one root of the selected incoming-continuation guard , with and . On the entire bracket, certify the incoming inequality , not just a derivative value at its root. Supply disjoint ordering certificates identifying the unique earliest event among all pairs. If , certify whether the exact root is ; 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. -
At , a certified bound with . The provider includes all evaluation errors in this bound. If , the root certificate gives ; set the lag bound . If , set 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 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 in these checks. For the selected pair use the state-reset bound 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 must come with a separate satisfying , where the norm is on the full state ; for an exact reset set .
-
A certificate that the matched isolated exact events have separation at least and count at most under the input endpoint policy. For an exact event at , policy
includeprocesses the reset and counts it; policypre-impactreports 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 does not establish another isolated transverse event after the reset.
Procedure. Initialize the current reported time , current state to
the input initial state, aligned-start error , accepted-event count ,
and an empty output ledger. While , request the provider certificates
for every unordered pair on the entire remaining horizon , 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 , append the segment, its error
bound and certificates, and return complete. Otherwise select the certified
unique earliest pair and its bracket , with upper endpoint
. If the provider certifies and
, append the incoming segment through and return
complete with the pre-impact endpoint; do not apply a reset or increment .
If or , 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 ; 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
The outgoing term accounts for the reference trajectory's flow
from its earlier true reset to the reported time. Append the reported reset,
set , update the current reported state and set . Restart the smooth integrator at , discard the previous local
reconstruction, and start the next accumulated dense-error ledger. If
, 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 and must fit within .
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 .
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 , so the incoming bracket condition is exactly . If one full mode graph is required, use an initial label and one label for each unordered contact pair, all carrying the identical smooth field. From every label, include a transition to each carrying that pair's guard and reset; this includes a self-transition at . Start in . 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 force or an irrational reported reset state.
Projected contact dynamics and explicit projection Euler step
Definition
Let , let be nonempty, closed, and convex, and let be the unique nearest point in to , whose existence and uniqueness are Every point has a unique nearest point in a nonempty closed Euclidean convex set. For , set for , set . On 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 exactly when and .
For , a solution of the projected contact dynamics with forcing and initial state is an absolutely continuous map satisfying Equivalently, . For an integer , put , , and define the exact explicit projection Euler nodes by starting from . Its affine interpolant joins consecutive nodes linearly on each interval .
For a map , absolutely continuous means that each coordinate is absolutely continuous in the scalar sense of Absolute continuity on a compact interval, and is the vector of coordinate derivatives, from The derivative of at a point that is a limit point of , and differentiability on a set, wherever they all exist. The solution condition requires a Lebesgue-null set such that for every all coordinate derivatives exist and the displayed inclusion holds. Here almost every is relative to Lebesgue measure from Lebesgue measurable sets, the family , and the restricted set function , with the convention of Measure-null sets and almost-everywhere statements relative to a measure.
Naive all-pairs sphere-contact search has quadratic work
Statement
For spheres, the naive search that evaluates every unordered pair guard exactly once per smooth segment performs pair-guard evaluations. Thus it uses 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 .
Facts & Assumptions
Given: The pair-enumeration loop of Event-driven integration for isolated frictionless spherical impacts and the particle count .
Event-driven integration for isolated frictionless spherical impacts: on each smooth segment, the naive search inspects each unordered pair once; event-certificate solves and reintegration are charged separately.
Laws of finite sums and finite products: finite sums split and telescope, and The principle of mathematical induction supplies induction on .
Proof
For each lower index , the loop tests exactly 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 .
Reindexing by gives . This sum is : it is for and , and increasing to adds exactly , which changes to ; induction gives the formula. For every , it is at most , proving the stated bound.
The convex normal-cone operator is maximal monotone and its resolvent is projection
Statement
Let be nonempty, closed, and convex, and let have the convention of Projected contact dynamics and explicit projection Euler step. In dimension , interpret this convention directly as , , and . An operator is monotone if for all and ; it is maximal monotone if its graph has no proper monotone graph extension. Then is maximal monotone. For every and , there is a unique with , and that point is . Equivalently, .
Facts & Assumptions
Given: The set and normal-cone convention in the Statement, and a scalar .
Scaled KKT residual and convex normal cone and Projected contact dynamics and explicit projection Euler step: for , ; outside , the operator is empty.
Extended-real indicator of a set: is on and outside .
Subdifferentials of proper extended-real convex functions: for proper convex and , means for every ; if , then .
Existence, resolvent characterization, and firm nonexpansiveness of the proximal map: for proper closed convex and , iff .
The proximal map of an indicator is Euclidean projection: the indicator of this nonempty closed convex set is proper, closed, and convex, and , the unique nearest point.
Proof
Let and . Testing the definition in [F1] with and gives and . Adding and changing signs yields . Thus is monotone.
The indicator is proper, closed, and convex by [F5], and its domain is by [F2]. At , [F2]–[F3] show exactly when for every ; inequalities for are automatic because . At , both and are empty. Hence .
Given any , put by [F5]. By [F4] and step 1.2, , so . If also , monotonicity [step 1.1] gives , hence . Therefore the resolvent exists uniquely at every and equals .
Suppose is monotonically related to the graph of , so for every . Apply step 2.1 to to obtain and . Then , and the relation gives . Thus and , so already lies in the graph. Every monotone extension adds no point; is maximal monotone.
Projected Euler with certified inexact projection solves
Definition
Input a nonempty compact, closed, and convex set , , an exact force evaluator , , integer step count , initial state , tolerances , finite budgets for , and a projection-certificate provider . The explicit closedness condition matches Projected contact dynamics and explicit projection Euler step. An admissible provider, queried with , must return after at most candidate checks, in either case: unresolved or certified(p,\Pi) with a finite exact certificate proving and
Set , , and start with the given . For , form and call . 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 . Otherwise set and continue. After all 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 and require the same residual certificate of A certified projection variational residual bounds the projection error.
Allow at most 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.
Solutions of projected contact dynamics are unique under the inherited choice assumptions
Statement
Assume Countable Choice and Dependent Choice. Let and , let be nonempty, closed, and convex, and let satisfy for all , with . 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 . For , extend the solution convention directly: , , and a solution is the sole map .
Facts & Assumptions
Given: Countable Choice, Dependent Choice, the set and forcing, and two absolutely continuous solution maps in the Statement.
The Axiom of Countable Choice () is inherited through [F4]'s absolutely-continuous FTC.
The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain is inherited through [F4]'s absolutely-continuous FTC.
For , Projected contact dynamics and explicit projection Euler step: a solution satisfies for almost every .
Gronwall's integral inequality with variable and constant coefficients: if continuous satisfies , then .
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.
The Euclidean inner product on : is the singleton zero vector space, with zero inner product and norm.
Proof
If , then and both solution maps are identically zero. Coordinatewise absolute continuity and differentiation are vacuous, and the inclusion is , so this agrees with the extended convention and uniqueness holds.
Assume and let be the two solutions and define and at almost every time where both inclusions hold. By [F1] these belong to and ; [F2] gives .
The function is absolutely continuous by [F4]. At almost every , [F1] and step 1.2 give using the Lipschitz hypothesis and [F5]. Since , [F4] integrates this differential inequality to . Applying [F3] gives for every , so . This argument uses no choices beyond the two axioms already required by [F4].
Existence and uniqueness for projected dynamics and convergence of projection Euler under countable and dependent choice
Statement
Let , let be nonempty, compact, and convex, let , and let . Suppose is Lipschitz in the explicit sense for some and all . Assume the Axioms of Countable Choice and Dependent Choice. Then the projected inclusion has a unique absolutely continuous solution . For each integer , define , , and the exact projection Euler nodes by Their affine interpolants converge uniformly to as . 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.
The Axiom of Countable Choice (): every countable family of nonempty sets has a choice function. It is used by the differentiability, Lebesgue-differentiation, and null-union suppliers below.
The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain: every serial relation on a nonempty set admits an infinite dependent sequence. It is inherited through [F7]'s absolutely-continuous FTC.
Projected contact dynamics and explicit projection Euler step: is the unique nearest-point projection, has the outward convention, and the exact projection Euler recurrence and affine interpolation are as in the Statement.
Projection onto a closed convex set is nonexpansive: is nonexpansive.
Compactness of equi-Lipschitz curves with values in a compact Euclidean set: a sequence of uniformly Lipschitz curves into compact closed has a uniformly convergent subsequence with limit in .
Solutions of projected contact dynamics are unique under the inherited choice assumptions: under Countable Choice and Dependent Choice, for a forcing Lipschitz in , any two absolutely continuous solutions with the same initial state agree.
implies Lipschitz, Lipschitz implies absolutely continuous, and absolutely continuous implies continuous and bounded variation and Every function of bounded variation is differentiable almost everywhere: a Lipschitz curve is absolutely continuous and differentiable almost everywhere, componentwise.
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, is absolutely continuous, has derivative almost everywhere, and its derivative integrates to its endpoint difference.
A locally integrable function on and Lebesgue differentiation theorem on : for a locally Lebesgue-integrable function on , at almost every the averages tend to as ; the theorem assumes Countable Choice.
is countably infinite gives a bijection , and gives a bijection .
The recursion theorem and The principle of mathematical induction allow the finite iterated pairing construction on ; The rationals embed densely in the reals gives rational approximants to each real coordinate; and Cauchy-Schwarz with its equality case, the triangle inequality for , the parallelogram law and polarisation gives the finite-sum Euclidean norm formula used to bound a vector from its coordinate errors.
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 is null.
Proof
Since , [F5] shows that compact 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 for . Put ; the Lipschitz hypothesis gives on . For each exact Euler step, , so [F2] gives . Convexity keeps the affine interpolant in , and its slope on each step has norm at most .
On each open mesh cell , write for the affine interpolant, , , and . By the projection variational inequality in [F1], . Consequently, for every fixed ,
Apply [F3] to the sequence of interpolants for . Along a subsequence , they converge uniformly to a map with and Lipschitz constant . By [F6], is absolutely continuous and differentiable almost everywhere; at each differentiability point, the Lipschitz inequality implies .
Fix and a fixed . We have and , so replacing by in the integral of step 1.2 changes it by at most . The term with is the endpoint difference of , where . Uniform convergence gives its limit as the endpoint difference of ; [F7] identifies that difference with . Also on each mesh cell, so uniformly along the selected subsequence. Passing to the limit in the integrated inequality yields
The function is Lebesgue-integrable: [F7] gives a measurable version of ; define it to be where the derivative is undefined. Boundedness of makes the other factors integrable. Extend this representative of by zero outside to obtain a locally integrable function on . Since every interval integral in step 3.1 is nonnegative, is nondecreasing. At almost every interior , [F8] gives For every sufficiently small , the average on the left is because is nondecreasing. Taking the limit yields almost everywhere for each fixed .
Fix a bijection from [F9]. Define and, recursively, . Since is a bijection, induction using [F10] shows that each is a bijection. In particular, decoding by and applying coordinatewise gives a surjection . Thus is countable. It is dense in : for and , choose in each of the finitely many coordinates a rational strictly between and , using the interval-density conclusion of [F10]. For , [F10] gives so . Since , nonexpansiveness [F2] gives . For each , put . Step 4.1 gives a null exceptional set where . Countable Choice [A1] and [F11] make their union, together with the null set where does not exist, null. Outside it, for every . For each such , the expression is continuous in ; if it were negative at some , it would be negative on a neighborhood of meeting the dense set , a contradiction. Hence the inequality holds for every , so almost everywhere by [F1]. This proves existence of a solution along the selected subsequence.
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 . If the full sequence did not converge uniformly to , some subsequence would stay at uniform distance at least ; [F3] would give a further uniformly convergent subsequence, whose limit is a solution by steps 1.2–5.1 and hence equals , a contradiction. Therefore the entire sequence converges uniformly to .
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 be its unique solution. Let be any finite bound for the diameter of , set For , let be the affine interpolant of the exact projection Euler recurrence. If a complete run of Projected Euler with certified inexact projection solves returns nodes with certified residuals and is their affine interpolant, then In particular, the exact-projection branch has uniform error . Certified projection errors with 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.
The Axiom of Countable Choice () is assumed as in [F1] to obtain the exact solution ; the estimates use no additional countable choices.
The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain is assumed as in [F1] to obtain the exact solution ; the estimates use no additional dependent choices.
Existence and uniqueness for projected dynamics and convergence of projection Euler under countable and dependent choice: there is a unique absolutely continuous satisfying almost everywhere.
Projection onto a closed convex set is nonexpansive: is nonexpansive.
A certified projection variational residual bounds the projection error: a feasible candidate with variational residual at most is within distance of its exact projection.
Projected Euler with certified inexact projection solves: a completed run returns feasible nodes with the residual certificates specified in the algorithm Definition.
implies Lipschitz, Lipschitz implies absolutely continuous, and absolutely continuous implies continuous and bounded variation and Every function of bounded variation is differentiable almost everywhere: Lipschitz curves are absolutely continuous and differentiable almost everywhere.
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.
for every real , hence : for every real .
Gronwall's integral inequality with variable and constant coefficients: if is continuous and for constants , then .
Projected contact dynamics and explicit projection Euler step: the outward cone is , and an exact projection step satisfies .
Heine-Borel in : with the Euclidean metric a subset of 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: because , compact is closed, as well as bounded.
Proof
By [F12], compactness makes closed, so the projection and normal-cone hypotheses in [F11] and [F3] apply to the stated set. Let be the exact affine Euler interpolant, on , , and . The projection variational inequality in [F11] gives . Nonexpansiveness [F3] gives and , so . For the exact solution put . At almost every differentiability point, on both sides of ; the normal inequality with , divided by positive and negative and passed to the limit, gives . Hence , so Cauchy–Schwarz [F8] gives and .
By [F4] and [F5], each inexact node is within of the exact projection of its own unprojected input. Comparing it with the exact node and using [F3] and the state-Lipschitz bound gives Iteration from the common initial point yields . By [F9], .
Put and . By [F6]–[F7], is absolutely continuous and almost everywhere. Monotonicity [F2] at and gives . Since and , differentiation yields Indeed, using the within-step displacement bound; [F8] bounds its inner product with .
Since , we have . Thus since . Integrating the inequality and using gives . By [F10], , hence .
On each mesh cell, 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 which is the claimed estimate. If all , or if their sum is along a refining mesh, the stated rate follows.
5 · Examples, counterexamples and false statements
None yet.