Actual PBPS event-time nonaccumulation

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, arXiv2609.06905v1 Appendix A.1 (A.2), Ex8-Ex9 and the following SLLN/nonaccumulation paragraph. The actual finite-prefix and exponential-product realization are ASTIS completions; the bounded-horizon finite-index set is an explicit ASTIS consequence, not a quotation or the full Proposition3.1.

arXiv2609.06905v1 · arXiv2609.06905v1 Appendix A.1 (A.2), Ex8-Ex9 and following SLLN/nonaccumulation clauses; Algorithm1 actual flow/bounce/rate and standing six analytic conditions. · faithful paraphrase

Complete source statement (Samplinglib restatement)

Let E be any finite-dimensional real inner-product space, including dimension zero, with its Borel measurable structure. Let V:E→ℝ be C². Let α,β be nonnegative reals and η a real number satisfying α>0, α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, η>0, and βη≤1. Fix any y,xRef∈E and initial phase z0=(x0,p0)∈E×E. Set c=y−η∇V(xRef). For z=(x,p), define the actual harmonic flow Φ_t(z)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p), reflection S(z)=(x,p−[2〈p,g(x)〉/‖g(x)‖²]g(x)), residual g(x)=∇V(x)−∇V(xRef), and rate λ(z)=√η max{0,〈p,g(x)〉}. The reflection uses total real division, hence is the identity when g(x)=0. Define Λ(z,t)=∫_0^t λ(Φ_s(z)) ds for finite t≥0 and τ(z,e)=inf{t≥0:Λ(z,t)≥e}, with inf empty=∞. Let P be the actual countable product of rate-one exponential Borel measures on Ω=ℝ^ℕ; let ε_k(sample)=max{sample_k,0} viewed as a nonnegative real. Define active records (T,z) and an absorbing stopped record carrying no phase. Initialize record0=(0,z0). At index k, a stopped record stays stopped; an active record (T,z) becomes stopped if τ(z,ε_k)=∞ and otherwise becomes (T+τ(z,ε_k), S(Φ_{τ(z,ε_k)}(z))). Its event time T_k is the finite time component if active and ∞ if stopped. Then for these fixed y,xRef,z0, for P-almost every sample, simultaneously: (i) for every finite nonnegative horizon t, all sufficiently large k satisfy t<T_k; (ii) for every such t the set {k∈ℕ:T_k≤t} is finite. Initialization index0 is included, and ε_k is source E_(k+1). The result includes both eventual stopping and infinite continuing paths with unbounded event times; it does not assert eventual stopping. It is an actual-input, fixed-reference nonaccumulation conclusion of Appendix A.1 Ex9, with ASTIS total-record and finite-index adapters. The global physical-time process and its additional properties are separate obligations.

E is finite-dimensional real inner-product with its Borel measurable structure; no positive-dimension restriction. V is C² and α,β≥0.
The six exact source conditions are α>0; α≤β; V∈C²; for all x,v, α‖v‖²≤D²V(x)[v,v]≤β‖v‖²; η>0; βη≤1. No third or higher derivative condition.
y,xRef,z0 are arbitrary deterministic parameters. P and ε are literal canonical definitions. No probability, iid, positivity, divergence, cap, energy, waiting-time or recurrence certificate is a public premise.
Threshold positivity and faithful clamp/raw equality hold simultaneously only almost surely. The all-finite-horizon conclusion is pathwise on the common good-input event for each fixed parameter triple; no uncountable intersection over triples is assumed.
Stopped records have eventTime=∞ with no phase at infinity. The statement counts indices including index0, not a physical bounce-count expectation. The author direct Exp mean-one strong-law route is distinct from the reused ASTIS bounded-indicator sufficient route.

Actual source objects 1

\[c=y-\eta\nabla V(x_{\rm ref}),\quad g(x)=\nabla V(x)-\nabla V(x_{\rm ref}),\quad\lambda(x,p)=\sqrt\eta\max\{0,\langle p,g(x)\rangle\}.\]

Actual source objects 2

\[\Phi_t(x,p)=\left(c+\cos t(x-c)+\sqrt\eta\sin t\,p,\ -\frac{\sin t}{\sqrt\eta}(x-c)+\cos t\,p\right),\quad S(x,p)=\left(x,p-\frac{2\langle p,g(x)\rangle}{\|g(x)\|^2}g(x)\right).\]

Actual source objects 3

\[\Lambda(z,t)=\int_0^t\lambda(\Phi_s z)\,ds,\quad\tau(z,e)=\inf\{t\ge0:\Lambda(z,t)\ge e\},\quad\inf\varnothing=\infty.\]

Actual source objects 4

\[P=\mathrm{Exp}(1)^{\otimes\mathbb N},\quad\varepsilon_k=\max\{\omega_k,0\},\quad P\text{-a.s.}:\ \forall t<\infty,\quad T_n>t\text{ eventually},\quad\#\{n:T_n\le t\}<\infty.\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Actual PBPS event-time nonaccumulation

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNonaccumulation.actual_fixed_reference_event_time_nonaccumulation · theorem · Teaching coverage

Read this first

Mathematical statement

\[P=\mathrm{Exp}(1)^{\otimes\mathbb N},\quad\varepsilon_k=\max\{\omega_k,0\},\quad P\text{-a.s.}:\ \forall t<\infty,\quad T_n>t\text{ eventually},\quad\#\{n:T_n\le t\}<\infty.\]

Lean statement · actual_fixed_reference_event_time_nonaccumulation

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem actual_fixed_reference_event_time_nonaccumulation
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ) * ‖v‖ ^ 2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) :
    actual_fixed_reference_event_time_nonaccumulation_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_fixed_reference_event_time_nonaccumulation_statement

This literal definition stores the complete proposition asserted above. It supplies no mathematical proof or additional hypothesis; the theorem proof must establish its value.

Download module (.lean)

private def actual_fixed_reference_event_time_nonaccumulation_statement
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ) * ‖v‖ ^ 2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) : Prop :=
    let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
    let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun sample k => Real.toNNReal (sample k)
    let c : E → E → E := fun y xRef => y - η • gradient V xRef
    let Φ : E → E → ℝ → (E × E) → (E × E) := fun y xRef t z =>
      (c y xRef + Real.cos t • (z.1 - c y xRef) +
          (Real.sqrt η * Real.sin t) • z.2,
       (-Real.sin t / Real.sqrt η) • (z.1 - c y xRef) + Real.cos t • z.2)
    let S : E → (E × E) → (E × E) := fun xRef z =>
      (z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
        ‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
    let rate : E → (E × E) → ℝ := fun xRef z =>
      Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V xRef))
    let Λ : E → E → (E × E) → ℝ≥0 → ℝ := fun y xRef z t =>
      ∫ s in (0 : ℝ)..(t : ℝ), rate xRef (Φ y xRef s z)
    let τ : E → E → (E × E) → ℝ≥0 → WithTop ℝ≥0 := fun y xRef z e =>
      MeasureTheory.hittingAfter
        (fun t : ℝ≥0 => fun a : (E × E) × (E × E) × ℝ≥0 =>
          Λ a.1.1 a.1.2 a.2.1 t - (a.2.2 : ℝ))
        (Set.Ici (0 : ℝ)) 0 ((y, xRef), z, e)
    let next : E → E → ℝ≥0 → ((ℝ≥0 × (E × E)) ⊕ Unit) →
        ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef e r =>
      match r with
      | Sum.inr _ => Sum.inr ()
      | Sum.inl a =>
        if τ y xRef a.2 e = ⊤ then Sum.inr () else
          Sum.inl (a.1 + (τ y xRef a.2 e).untopD 0,
            S xRef (Φ y xRef (((τ y xRef a.2 e).untopD 0 : ℝ≥0) : ℝ) a.2))
    let record : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ →
        ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef z₀ e n =>
      Nat.rec (Sum.inl (0, z₀)) (fun k r => next y xRef (e k) r) n
    let eventTime : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ → WithTop ℝ≥0 :=
      fun y xRef z₀ e n => (record y xRef z₀ e n).elim
        (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
    ∀ y xRef : E, ∀ z₀ : E × E, ∀ᵐ sample ∂P,
      (∀ t : ℝ≥0, ∀ᶠ n : ℕ in atTop,
        (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) n) ∧
      (∀ t : ℝ≥0, {n : ℕ | eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0)}.Finite)


set_option maxHeartbeats 800000 in

Exact module and namespace context

Proof roadmap

1Fix the actual source objects and stopped event times
Use the literal harmonic flow, zero-safe reflection, integrated rate, first hitting time and stopped recursion from the actual finite-prefix theorem. Fix the canonical Exp1 product and its total nonnegative thresholds. The energy H and finite cap C are internal formulas: H(z)=(η⁻¹‖x−c‖²+‖p‖²)/2 and C=√η β√(2H(z0))(√(2ηH(z0))+‖c−xRef‖). They are proved recurrence invariants and bounds, not theorem assumptions.
2Join the two actual compiled parents
Apply the finite-recursion theorem to the six analytic source hypotheses. It supplies initialization, monotone times, absorbing stopping, C≥0, the positive-cap increment and zero-cap stopping. Apply the concrete product theorem to obtain a common positive-threshold event and divergent partial sums, with no supplied stochastic witness.
3Intersect the two good-input events
For arbitrary fixed y,xRef,z0, intersect the almost-sure all-coordinate positivity and divergent-sum events. Positivity makes every clamped ε_k strictly positive. Extract the cap laws for this actual sample; these facts remain internal to the proof.
4Handle zero cap by absorbing stopping
Split on C=0. The initial record is active and ε0>0, so its first update stops. Absorption proves T_(1+k)=∞ for every k. Every finite horizon is therefore exceeded at all indices n≥1. This includes zero-energy and dimension-zero cases.
5Sum the actual positive-cap increments
In the other branch C≥0 and C≠0 give C>0. Let cap=toNNReal(C), whose real coercion is C. Starting from S0=T0=0, apply the actual extended-valued increment inequality and induction: S_(n+1)/C=S_n/C+ε_n/C≤T_n+ε_n/C≤T_(n+1). The same inequality remains valid after stopping since times are top.
6Use divergent inputs to escape every finite horizon
For any finite t, divergence gives S_n>tC eventually. Because C>0 this implies S_n/C>t. Combine this strict finite inequality, lifted into WithTop NNReal, with the prefix lower bound. This proves finite-horizon escape without requiring eventual equality to infinity.
7Turn escape into a finite index set
For each t, choose N such that n≥N implies t<T_n. Any n with T_n≤t must satisfy n<N. The sublevel index set is therefore contained in the finite natural interval [0,N); index0 is retained. Assemble both almost-sure conclusions.

Full assumptions and notation

All objects and hypotheses

E is finite-dimensional real inner-product with its Borel measurable structure; no positive-dimension restriction. V is C² and α,β≥0.
The six exact source conditions are α>0; α≤β; V∈C²; for all x,v, α‖v‖²≤D²V(x)[v,v]≤β‖v‖²; η>0; βη≤1. No third or higher derivative condition.
y,xRef,z0 are arbitrary deterministic parameters. P and ε are literal canonical definitions. No probability, iid, positivity, divergence, cap, energy, waiting-time or recurrence certificate is a public premise.
Threshold positivity and faithful clamp/raw equality hold simultaneously only almost surely. The all-finite-horizon conclusion is pathwise on the common good-input event for each fixed parameter triple; no uncountable intersection over triples is assumed.
Stopped records have eventTime=∞ with no phase at infinity. The statement counts indices including index0, not a physical bounce-count expectation. The author direct Exp mean-one strong-law route is distinct from the reused ASTIS bounded-indicator sufficient route.

Mathematical proof

1. Fix the actual source objects and stopped event times

Use the literal harmonic flow, zero-safe reflection, integrated rate, first hitting time and stopped recursion from the actual finite-prefix theorem. Fix the canonical Exp1 product and its total nonnegative thresholds. The energy H and finite cap C are internal formulas: H(z)=(η⁻¹‖x−c‖²+‖p‖²)/2 and C=√η β√(2H(z0))(√(2ηH(z0))+‖c−xRef‖). They are proved recurrence invariants and bounds, not theorem assumptions.

\[H(z)=\tfrac12(\eta^{-1}\|x-c\|^2+\|p\|^2),\quad C=\sqrt\eta\,\beta\sqrt{2H(z_0)}(\sqrt{2\eta H(z_0)}+\|c-x_{\rm ref}\|).\]

Corresponding Lean step

  classical
  let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
  let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun sample k => Real.toNNReal (sample k)
  let c : E → E → E := fun y xRef => y - η • gradient V xRef
  let Φ : E → E → ℝ → (E × E) → (E × E) := fun y xRef t z =>
    (c y xRef + Real.cos t • (z.1 - c y xRef) +
        (Real.sqrt η * Real.sin t) • z.2,
     (-Real.sin t / Real.sqrt η) • (z.1 - c y xRef) + Real.cos t • z.2)
  let S : E → (E × E) → (E × E) := fun xRef z =>
    (z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
      ‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
  let rate : E → (E × E) → ℝ := fun xRef z =>
    Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V xRef))
  let H : E → E → (E × E) → ℝ := fun y xRef z =>
    (η⁻¹ * ‖z.1 - c y xRef‖ ^ 2 + ‖z.2‖ ^ 2) / 2
  let C : E → E → (E × E) → ℝ := fun y xRef z =>
    Real.sqrt η * (β : ℝ) * Real.sqrt (2 * H y xRef z) *
      (Real.sqrt (2 * η * H y xRef z) + ‖c y xRef - xRef‖)
  let Λ : E → E → (E × E) → ℝ≥0 → ℝ := fun y xRef z t =>
    ∫ s in (0 : ℝ)..(t : ℝ), rate xRef (Φ y xRef s z)
  let τ : E → E → (E × E) → ℝ≥0 → WithTop ℝ≥0 := fun y xRef z e =>
    MeasureTheory.hittingAfter
      (fun t : ℝ≥0 => fun a : (E × E) × (E × E) × ℝ≥0 =>
        Λ a.1.1 a.1.2 a.2.1 t - (a.2.2 : ℝ))
      (Set.Ici (0 : ℝ)) 0 ((y, xRef), z, e)
  let next : E → E → ℝ≥0 → ((ℝ≥0 × (E × E)) ⊕ Unit) →
      ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef e r =>
    match r with
    | Sum.inr _ => Sum.inr ()
    | Sum.inl a =>
      if τ y xRef a.2 e = ⊤ then Sum.inr () else
        Sum.inl (a.1 + (τ y xRef a.2 e).untopD 0,
          S xRef (Φ y xRef (((τ y xRef a.2 e).untopD 0 : ℝ≥0) : ℝ) a.2))
  let record : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ →
      ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef z₀ e n =>
    Nat.rec (Sum.inl (0, z₀)) (fun k r => next y xRef (e k) r) n
  let eventTime : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ → WithTop ℝ≥0 :=
    fun y xRef z₀ e n => (record y xRef z₀ e n).elim
      (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
  change ∀ y xRef : E, ∀ z₀ : E × E, ∀ᵐ sample ∂P,
    (∀ t : ℝ≥0, ∀ᶠ n : ℕ in atTop,
      (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) n) ∧
    (∀ t : ℝ≥0, {n : ℕ | eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0)}.Finite)