Alphabeta Math
AlgorithmAlgorithm: AI-adaptedProof: Not applicablePipeline-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.

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.

Depends on

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