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.
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.
Depends on
- Impulse, momentum, and kinetic-energy laws for an isolated frictionless sphere impact
- Sphere-contact guards, normals and binary resets have explicit tube bounds
- Smooth hybrid ODE modes, guards, resets, and deterministic event priority
- A transverse hybrid event time is stable under dense-output and root error
- Reset and smooth-mode flow propagate a transverse event-time error
- A Lipschitz ODE mode flow is stable to its initial state on a tube
Used by
Dependency tree · two levels
19 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- David E. Stewart, Dynamics with Inequalities: Impacts and Hard Constraints (standard reference, not scraped)
- Dimitri P. Bertsekas, 6.253 Convex Analysis and Optimization, Complete Lecture Notes (standard reference, not scraped)