Actual PBPS finite-count complete-path law

Chen, Chewi, Lu and Zhang, arXiv:2609.06905v1, Appendix A.1 and A.2; attributed ASTIS completion of a source-implicit finite-count path ingredient, not verbatim source text.

arXiv2609.06905v1 · Chen-Chewi-Lu-Zhang arXiv2609.06905v1 Appendix A.1 (A.1),(A.2),(A.7), half-open arcs and prescribed-path paragraph; Appendix A.2 measurable realization. Source-implicit finite-count path ingredient with explicit ASTIS completions. · faithful paraphrase

Complete source statement (Samplinglib restatement)

Let E be any finite-dimensional real inner-product Borel space, including dimension zero. Let V:E→ℝ be C², α,β≥0 and η∈ℝ with α>0, α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, η>0 and βη≤1. Fix any deterministic y,r∈E and initial phase z₀∈E×E. Put c=y−η∇V(r), Φ_t(x,p)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p), g_r(x)=∇V(x)−∇V(r), S_r(x,p)=(x,p−2〈p,g_r(x)〉g_r(x)/‖g_r(x)‖²), λ_r(x,p)=√η max{0,〈p,g_r(x)〉}, Λ_z(t)=∫₀ᵗλ_r(Φ_s(z))ds and τ_z(e)=inf{t≥0:Λ_z(t)≥e}∈[0,∞], with inf empty=∞. Total real division makes S_r the identity at g_r(x)=0. The record space is D=([0,∞)×(E×E))⊕{stopped}, with Borel sum structure. Define next(e,stopped)=stopped; for a live record (T,z), next(e,(T,z))=stopped if τ_z(e)=∞, and otherwise next(e,(T,z))=(T+τ_z(e),S_rΦ_(τ_z(e))(z)). In the Lean definition untopD0 is used only in this non-top branch. Define R₀(e)=live(0,z₀) and R_(j+1)(e)=next(e_j,R_j(e)). Let Ω=ℝ^ℕ with its product Borel structure and P=⊗_(k≥0)Exp(1). Let ε(w)_k=max{w_k,0}; this is an ambient coordinate extension on a P-null nonpositive-clock set, not new source dynamics for negative clocks. Write T_j(w)=a for a live record R_j(ε(w))=live(a,z), and T_j(w)=∞ for a stopped record. Define I_n(T)={T_n≤T<T_(n+1)}, and the total selector N(T,w)=min{n:w∈I_n(T)} when such an n exists, and 0 otherwise. For n≥0 let Hist_n=D^(Fin(n+1)) and H_n(w)_j=R_j(ε(w)). Write readTime(live(a,z))=a and readTime(stopped)=0. The abstract guard A_n(T) consists of histories all of whose records are live, whose read times are strictly increasing and whose positive-index read times are strictly below T; it does not constrain record0 itself. Actual H_n starts at live(0,z₀). For h∈Hist_n set d_n(T,h)=max{T−readTime(h_n),0}. Define survival(live(a,z),u,e) to mean u<τ_z(max{e,0}); on stopped it is false. Define W(live(a,z),u)=exp(−Λ_z(u)); on stopped W=0. Put C_n(T)={w:H_n(w)∈A_n(T), survival(R_n(ε(w)),d_n(T,H_n(w)),w_n)}. For a fixed finite T≥0 let Path_T be all functions from [0,T] into E×E, with its coordinate-product sigma algebra. On every history, including unrealizable ones, define Ψ_n(T,h)(s) by starting at z₀ and visiting j=0,…,n in increasing order: a live record (a,z) with a≤s replaces the current value by Φ_(s−a)(z), and an ineligible live or stopped record leaves it unchanged. All elapsed times in this total definition use nonnegative subtraction. Define Δ_n(T)={t∈ℝ^n:0<t₁<⋯<t_n<T}, and let m_n be the comap of product Lebesgue measure to this subtype, without normalization. For t∈Δ_n(T), put s₀=0,s_i=t_i, z₀ equal to the prescribed initial phase and z_i=S_rΦ_(s_i−s_(i−1))(z_(i−1)). Set K_n(t)_j=live(s_j,z_j), Γ_n(T,t)=Ψ_n(T,K_n(t)), q_n(t)=ofReal(∏_(i=1)^n λ_r(Φ_(s_i−s_(i−1))(z_(i−1)))exp[−Λ_(z_(i−1))(s_i−s_(i−1))]), and ρ_n(T,t)=q_n(t)W(K_n(t)_n,d_n(T,K_n(t))). The literal toNNReal conversions agree with these nonnegative simplex times. There exists one actual phase representative Z(y,r,z₀,t,w), jointly Borel in all deterministic parameters, finite time and raw input, with the following properties. On every raw covering interval T_n(w)≤s<T_(n+1)(w), if R_n(ε(w))=live(a,z), then Z(s,w)=Φ_(s−a)(z). If no interval covers s, Z(s,w)=z₀. For each fixed parameter tuple, Z(0,w)=z₀ almost surely. For every n≥0 and finite T≥0, Ψ_n, Γ_n and ρ_n are jointly measurable for the stated sigma algebras in their deterministic parameters and history or simplex input. For each fixed parameter tuple, H_n, Z_T:w↦(s↦Z(s,w)), N(T,·) and C_n(T) are measurable. For every prescribed t and s∈[0,T], if s_j≤s and every later s_k>s, then Γ_n(T,t)(s)=Φ_(s−s_j)(z_j). For every raw w∈C_n(T), Ψ_n(T,H_n(w))=Z_T(w) as entire functions on [0,T]. For each fixed parameter tuple and T, on one P-full event simultaneously for every j>0 and every k≥0: T_j(w)≠T, N(T,w)=k if and only if w∈C_k(T), both sets {j>0:T_j(w)<T} and {j>0:T_j(w)≤T} are finite, and both cardinalities equal N(T,w). This is not a single no-jump event valid for all T. The raw sets C_k(T) are pairwise disjoint, and P(⋃_(k≥0)C_k(T))=1. The exact unnormalized joint history/path law is (H_n,Z_T)_*(P restricted to {N(T)=n})=(K_n,Γ_n)_*(ρ_n m_n). Equivalently, for every F:Hist_n×Path_T→[0,∞] measurable for the stated sigma algebras, ∫_{N(T)=n}F(H_n(w),Z_T(w))P(dw)=∫_{Δ_n(T)}F(K_n(t),Γ_n(t))ρ_n(T,t)m_n(dt). Moreover ∫ρ_n dm_n=P{N(T)=n}≤1. No test boundedness, integrability, positive event probability, provider of densities, independence, finite waits or process measurability is assumed. The result includes n=0,T=0, rank0, infinite waits and explicit raw exceptional fallbacks; at n=0 the terminal survival factor remains, so the mass is not generally one for T>0. This is an attributed ASTIS completion of the finite-count complete-path ingredient implicit in Appendix A.1(A.7), using Appendix A.2. It is a faithful mathematical restatement with disclosed rank-zero, extended-test and coordinate-product-path choices, not a quoted standalone theorem. Hazard stitching along the path, pre-jump left limits, Skorokhod compatibility, the infinite full A.7 expansion, restart/Markovness, invariance, hypocoercivity, implementation errors, expected query costs, full paper results and actual-input composition are separate remaining obligations.

Finite-dimensional real inner-product Borel space E, including the disclosed rank-zero extension.
Exactly six analytic assumptions: α>0, α≤β, V∈C², α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v, η>0, βη≤1; α,β are nonnegative.
All finite n,T≥0 and deterministic y,r,z₀ are universal. The actual iid Exp(1) input, stopped recursion, count, history/path maps and density are literal definitions, not supplied certificates.
Path_T carries the coordinate-product sigma algebra. Each test F:Hist_n×Path_T→[0,∞] is arbitrary measurable for these sigma algebras.
Joint measurability, existence, initialization, endpoint nullity, finite counts, all laws and mass bounds are derived; no additional boundedness, integrability, positive mass, finite waiting time or independence premise.

Finite-count path formula 1

\[C_n(T)=\{H_n\in A_n(T),\ T-T_n<\tau_{z_n}(\epsilon_n)\},\quad \rho_n=q_n\exp[-\Lambda_{z_n}(T-s_n)].\]

Finite-count path formula 2

\[\Psi_n(h)(s)=\Phi_{s-a_j}(z_j),\quad j=\max\{i\le n:h_i=\operatorname{live}(a_i,z_i),\ a_i\le s\},\quad\text{if this set is nonempty; otherwise }\Psi_n(h)(s)=z_0.\]

Finite-count path formula 3

\[\forall T\ge0,\quad P\{\exists j>0:T_j=T\}=0.\]

Finite-count path formula 4

\[N(T)=n\ \Longleftrightarrow\ C_n(T)\quad P\text{-a.s.},\qquad N(T)=\#\{j>0:T_j<T\}=\#\{j>0:T_j\le T\}.\]

Finite-count path formula 5

\[(H_n,Z_T)_*(P|_{\{N(T)=n\}})=(K_n,\Gamma_n)_*(\rho_nm_n).\]

Finite-count path formula 6

\[\int_{N(T)=n}F(H_n,Z_T)\,dP=\int_{\Delta_n(T)}F(K_n,\Gamma_n)\rho_n\,dm_n,\quad \int\rho_n\,dm_n=P\{N(T)=n\}\le1.\]

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 finite-count complete-path law

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteCountPath.actual_finite_count_path_law · theorem · Teaching coverage

Read this first

Mathematical statement

\[(H_n,Z_T)_*(P|_{\{N(T)=n\}})=(K_n,\Gamma_n)_*(\rho_nm_n).\]

Lean statement · actual_finite_count_path_law

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_finite_count_path_law
    {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_finite_count_path_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_finite_count_path_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_finite_count_path_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 := by
  classical
  exact
    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 P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
    let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun w k => Real.toNNReal (w k)
    let history : E → E → (E × E) → (n : ℕ) → (ℕ → ℝ) →
        (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) :=
      fun y xRef z₀ n w j => record y xRef z₀ (ε w) j.val
    let Rec := (ℝ≥0 × (E × E)) ⊕ Unit
    let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
    let readTime : Rec → ℝ := fun r => match r with
      | Sum.inl q => (q.1 : ℝ)
      | Sum.inr _ => 0
    let Δ : (n : ℕ) → ℝ≥0 → Set (Fin n → ℝ) := fun n T =>
      {t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < (T : ℝ)}
    let Prefix : (n : ℕ) → ℝ≥0 → Type := fun n T => {t : Fin n → ℝ // t ∈ Δ n T}
    let m : (n : ℕ) → (T : ℝ≥0) → Measure (Prefix n T) := fun n T =>
      Measure.comap (fun t : Prefix n T => t.val) (volume : Measure (Fin n → ℝ))
    let zAt : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Fin (n + 1) → (E × E) := fun y xRef z₀ n T t =>
      Fin.induction z₀ (fun i z =>
        S xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc) z))
    let K : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Hist n := fun y xRef z₀ n T t j =>
      Sum.inl (Real.toNNReal ((Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) j), zAt y xRef z₀ n T t j)
    let qReal : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → ℝ := fun y xRef z₀ n T t =>
      ∏ i : Fin n,
        rate xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc)
          (zAt y xRef z₀ n T t i.castSucc)) *
        Real.exp (-Λ y xRef (zAt y xRef z₀ n T t i.castSucc)
          (Real.toNNReal (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc)))
    let q : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → ℝ≥0∞ := fun y xRef z₀ n T t =>
      ENNReal.ofReal (qReal y xRef z₀ n T t)
    let A : (n : ℕ) → ℝ≥0 → Set (Hist n) := fun n T =>
      {h | (∀ j, ∃ a : ℝ≥0 × (E × E), h j = Sum.inl a) ∧
        StrictMono (fun j => readTime (h j)) ∧
        ∀ i : Fin n, readTime (h i.succ) < (T : ℝ)}
    let eventTime : E → E → (E × E) → (ℕ → ℝ) → ℕ → WithTop ℝ≥0 :=
      fun y xRef z₀ w j => (record y xRef z₀ (ε w) j).elim
        (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
    let I : E → E → (E × E) → ℝ≥0 → ℕ → Set (ℕ → ℝ) :=
      fun y xRef z₀ T n => {w | eventTime y xRef z₀ w n ≤ (T : WithTop ℝ≥0) ∧
        (T : WithTop ℝ≥0) < eventTime y xRef z₀ w (n + 1)}
    let N : E → E → (E × E) → ℝ≥0 → (ℕ → ℝ) → ℕ := fun y xRef z₀ T w =>
      if h : ∃ n, w ∈ I y xRef z₀ T n then Nat.find h else 0
    let liveTime : Rec → ℝ≥0 := fun r => r.elim Prod.fst (fun _ => 0)
    let d : (n : ℕ) → ℝ≥0 → Hist n → ℝ≥0 :=
      fun n T h => T - liveTime (h ⟨n, Nat.lt_succ_self n⟩)
    let survival : E → E → Rec → ℝ≥0 → ℝ → Prop :=
      fun y xRef r u e => r.elim
        (fun a => (u : WithTop ℝ≥0) < τ y xRef a.2 (Real.toNNReal e)) (fun _ => False)
    let weight : E → E → Rec → ℝ≥0 → ℝ≥0∞ :=
      fun y xRef r u => r.elim
        (fun a => ENNReal.ofReal (Real.exp (-Λ y xRef a.2 u))) (fun _ => 0)
    let C : E → E → (E × E) → (n : ℕ) → ℝ≥0 → Set (ℕ → ℝ) :=
      fun y xRef z₀ n T => {w | history y xRef z₀ n w ∈ A n T ∧
        survival y xRef (record y xRef z₀ (ε w) n) (d n T (history y xRef z₀ n w)) (w n)}
    let Path : ℝ≥0 → Type _ := fun T => {s : ℝ≥0 // s ≤ T} → E × E
    let Ψ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Hist n → Path T :=
      fun y xRef z₀ n T h s =>
        Fin.foldl (n + 1) (fun z j => (h j).elim
          (fun a => if a.1 ≤ s.val then Φ y xRef ((s.val - a.1 : ℝ≥0) : ℝ) a.2 else z)
          (fun _ => z)) z₀
    let Γ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → Path T :=
      fun y xRef z₀ n T t => Ψ y xRef z₀ n T (K y xRef z₀ n T t)
    let ρ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → ℝ≥0∞ :=
      fun y xRef z₀ n T t => q y xRef z₀ n T t *
        weight y xRef ((K y xRef z₀ n T t) ⟨n, Nat.lt_succ_self n⟩)
          (d n T (K y xRef z₀ n T t))
    ∃ Z : E → E → (E × E) → ℝ≥0 → (ℕ → ℝ) → (E × E),
      Measurable (fun a : ((E × E) × (E × E)) × ℝ≥0 × (ℕ → ℝ) =>
        Z a.1.1.1 a.1.1.2 a.1.2 a.2.1 a.2.2) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ w : ℕ → ℝ, ∀ s : ℝ≥0,
        ∀ n : ℕ, ∀ a : ℝ≥0 × (E × E), w ∈ I y xRef z₀ s n →
          record y xRef z₀ (ε w) n = Sum.inl a →
          Z y xRef z₀ s w = Φ y xRef ((s - a.1 : ℝ≥0) : ℝ) a.2) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ w : ℕ → ℝ, ∀ s : ℝ≥0,
        (¬ ∃ n, w ∈ I y xRef z₀ s n) → Z y xRef z₀ s w = z₀) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ᵐ w ∂P, Z y xRef z₀ 0 w = z₀) ∧
      (∀ n : ℕ, ∀ T : ℝ≥0,
        Measurable (fun p : ((E × E) × (E × E)) × Hist n =>
          Ψ p.1.1.1 p.1.1.2 p.1.2 n T p.2) ∧
        Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
          Γ p.1.1.1 p.1.1.2 p.1.2 n T p.2) ∧
        Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
          ρ p.1.1.1 p.1.1.2 p.1.2 n T p.2) ∧
        (∀ y xRef : E, ∀ z₀ : E × E,
          let H := history y xRef z₀ n
          let ZT : (ℕ → ℝ) → Path T := fun w s => Z y xRef z₀ s.val w
          Measurable H ∧ Measurable ZT ∧ Measurable (N y xRef z₀ T) ∧
          MeasurableSet (C y xRef z₀ n T) ∧
          (∀ t : Prefix n T, ∀ s : {s : ℝ≥0 // s ≤ T}, ∀ j : Fin (n + 1),
            (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) j ≤ (s.val : ℝ) →
            (∀ k : Fin (n + 1), j < k → (s.val : ℝ) < (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) k) →
            Γ y xRef z₀ n T t s =
              Φ y xRef ((s.val : ℝ) - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) j) (zAt y xRef z₀ n T t j)) ∧
          (∀ w ∈ C y xRef z₀ n T, Ψ y xRef z₀ n T (H w) = ZT w) ∧
          (∀ᵐ w ∂P, (∀ j : ℕ, 0 < j → eventTime y xRef z₀ w j ≠ (T : WithTop ℝ≥0)) ∧
            (∀ k : ℕ, N y xRef z₀ T w = k ↔ w ∈ C y xRef z₀ k T) ∧
            {j : ℕ | 0 < j ∧ eventTime y xRef z₀ w j < (T : WithTop ℝ≥0)}.Finite ∧
            {j : ℕ | 0 < j ∧ eventTime y xRef z₀ w j ≤ (T : WithTop ℝ≥0)}.Finite ∧
            N y xRef z₀ T w = {j : ℕ | 0 < j ∧ eventTime y xRef z₀ w j < (T : WithTop ℝ≥0)}.ncard ∧
            N y xRef z₀ T w = {j : ℕ | 0 < j ∧ eventTime y xRef z₀ w j ≤ (T : WithTop ℝ≥0)}.ncard) ∧
          (Pairwise fun i j : ℕ => Disjoint (C y xRef z₀ i T) (C y xRef z₀ j T)) ∧
          P (⋃ k : ℕ, C y xRef z₀ k T) = 1 ∧
          Measure.map (fun w => (H w, ZT w)) (P.restrict {w | N y xRef z₀ T w = n}) =
            Measure.map (fun t => (K y xRef z₀ n T t, Γ y xRef z₀ n T t))
              ((m n T).withDensity (ρ y xRef z₀ n T)) ∧
          (∀ F : Hist n × Path T → ℝ≥0∞, Measurable F →
            (∫⁻ w in {w | N y xRef z₀ T w = n}, F (H w, ZT w) ∂P) =
              ∫⁻ t : Prefix n T, F (K y xRef z₀ n T t, Γ y xRef z₀ n T t) *
                ρ y xRef z₀ n T t ∂m n T) ∧
          (∫⁻ t : Prefix n T, ρ y xRef z₀ n T t ∂m n T) = P {w | N y xRef z₀ T w = n} ∧
          P {w | N y xRef z₀ T w = n} ≤ 1))

Exact module and namespace context

Proof roadmap

1Construct a total measurable finite-history interpolation
Fix one coordinate s of the path. Each tagged record either retains the accumulator or replaces it by the harmonic flow at s−a; the live/stopped tag and a≤s are Borel. Finite induction proves the fold measurable. The product sigma algebra then makes the entire function-valued map measurable by its coordinates. The last eligible record controls the fold, including when no record is eligible and z₀ remains. Reuse the actual harmonic-flow joint measurability to obtain Ψ for every parameter and arbitrary history.
2Convert conditional next-wait survival into a weighted history measure
The actual conditional survival theorem applies at the history-dependent residual d=max(T−lastTime,0). For every Borel history event A, its probability with survival is the history integral of W over A. Apply this to B∩A for an arbitrary Borel test set B; measure extensionality identifies H_*(P|_{H∈A,survival})=(H_*P|_A).withDensity(W). Measurability is inherited from actual history, the tagged time observer and the actual hazard. No positive conditioning probability or finite wait is required, and W vanishes on the stopped tag.
3Attach the terminal factor to the ordered-prefix law
Apply the weighted history identity to F(h,Ψ(h)). The actual ordered-prefix law applies to this nonnegative measurable function times W, giving the simplex integral of F(K,Ψ(K))qW. This is precisely F(K,Γ)ρ. Joint measurability of K, Ψ, q and the tagged terminal weight implies joint measurability of Γ and ρ for the stated sigma algebras. Equality of all nonnegative tests gives the joint history/interpolation pushforward, and F=1 gives its unnormalized mass P(C_n)≤1. This step does not yet identify C_n with a count event.
4Identify interpolation with one actual process on the raw event
Take the existing jointly measurable physical-time representative Z, with its exact covered-arc and uncovered-fallback behavior. On C_n all records through n are live, and strict terminal survival gives T<T_(n+1), also when the wait is infinite. At any s≤T choose the greatest index j≤n whose record time is at most s; initialization supplies index0. Every later index is ineligible and the next event lies after s. The finite fold therefore equals the harmonic arc selected by the actual Z. Function extensionality gives whole-path equality on every raw C_n sample, without assuming a measurable diagonal in the uncountable path space.
5Make the total count measurable and relate interval indices to cardinalities
Each half-open interval membership predicate is Borel because actual event times are jointly measurable. Their countable union is Borel. On that union the least successful index is measurable; use0 off it. Distinct half-open intervals cannot overlap for a monotone event-time sequence. If N selects the covering interval, monotonicity gives T_j≤T iff j≤N. In the absence of positive-index events exactly at T the strict and non-strict positive-index sets both equal {1,…,N}, hence are finite with cardinality N. The no-atom condition is an internal dependency supplied below.
6Read the prescribed path at its last eligible event
Every ordered simplex time is nonnegative. The real time and nonnegative-time coercions therefore agree, and the last-eligible fold identity yields Γ(t)(s)=Φ_(s−s_j)(z_j). The condition requires s_j≤s and all later s_k>s; at an event time the selected state is the post-bounce z_j. It also covers n=0 and T=0.
7Exclude fixed-horizon endpoint atoms from the actual input
A coordinate hyperplane {t_i=T} has zero finite-product Lebesgue measure. Comap to the simplex and multiplication by any nonnegative density preserve that null set. The prefix pushforward law transfers this to the actual history observer on the strict guard. Actual exponential inputs are simultaneously positive almost surely, and the actual finite recurrence then gives strict increases between live records. If the nth event equals T, the entire finite history belongs to the strict guard at T+1. Applying the guarded nullity there avoids excluding the endpoint by definition. A countable intersection over positive n proves no event exactly at this fixed T. No intersection over all real T is taken.
8Close count interpretation, disjointness and full probability
On every raw C_n, the last time is at most T (initial time0 handles n=0), and survival makes the next time strictly greater than T: thus C_n⊆I_n. Conversely, on the common full event of positive clocks, fixed-T no-atoms and physical-time coverage, any covering interval has a live history with strictly increasing times and all positive-index times below T, and its residual wait survives to T. Hence I_n=C_n on that event for all n. The least covering index is unique, so N=n iff C_n and the preceding cardinality lemma applies. Raw C disjointness follows from C_n⊆I_n and monotonicity. Almost-sure coverage then makes their countable union have mass1.
9Assemble the sealed actual history/path law
Keep the one actual Z and all original six assumptions. Its joint measurability gives each coordinate-measurable Z_T; combine this with H_n,N,Ψ,Γ,ρ measurability and prescribed path evaluation. The sets {N=n} and C_n agree almost surely, so their restricted measures agree. On C_n the whole paths Ψ(H_n) and Z_T agree pointwise. Substitution into the weighted joint pushforward and every nonnegative test identity gives the claimed actual law. The same almost-sure set equality transfers the mass formula ∫ρ=P(C_n) to P{N=n}. In particular the zero-event term retains terminal survival; it is not normalized to one for positive T.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real inner-product Borel space E, including the disclosed rank-zero extension.
Exactly six analytic assumptions: α>0, α≤β, V∈C², α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v, η>0, βη≤1; α,β are nonnegative.
All finite n,T≥0 and deterministic y,r,z₀ are universal. The actual iid Exp(1) input, stopped recursion, count, history/path maps and density are literal definitions, not supplied certificates.
Path_T carries the coordinate-product sigma algebra. Each test F:Hist_n×Path_T→[0,∞] is arbitrary measurable for these sigma algebras.
Joint measurability, existence, initialization, endpoint nullity, finite counts, all laws and mass bounds are derived; no additional boundedness, integrability, positive mass, finite waiting time or independence premise.

Mathematical proof

1. Construct a total measurable finite-history interpolation

Fix one coordinate s of the path. Each tagged record either retains the accumulator or replaces it by the harmonic flow at s−a; the live/stopped tag and a≤s are Borel. Finite induction proves the fold measurable. The product sigma algebra then makes the entire function-valued map measurable by its coordinates. The last eligible record controls the fold, including when no record is eligible and z₀ remains. Reuse the actual harmonic-flow joint measurability to obtain Ψ for every parameter and arbitrary history.

\[\Psi_n(h)(s)=\Phi_{s-a_j}(z_j),\quad j=\max\{i\le n:h_i=\operatorname{live}(a_i,z_i),\ a_i\le s\},\quad\text{if this set is nonempty; otherwise }\Psi_n(h)(s)=z_0.\]

Corresponding Lean step

private theorem measurable_finite_fold {X Y : Type*}
    [MeasurableSpace X] [MeasurableSpace Y] (n : ℕ)
    (f : X → Y → Fin n → X)
    (hf : ∀ j, Measurable (fun p : X × Y => f p.1 p.2 j))
    (x : Y → X) (hx : Measurable x) :
    Measurable (fun y => Fin.foldl n (fun z j => f z y j) (x y)) := by
  induction n with
  | zero => simpa only [Fin.foldl_zero] using hx
  | succ n ih =>
    have hr := ih (fun z y j => f z y j.castSucc) (fun j => hf j.castSucc)
    simpa only [Fin.foldl_succ_last, Function.comp_def, id_eq] using
      (hf (Fin.last n)).comp (hr.prodMk measurable_id)

private theorem measurable_record_step {X Y : Type*}
    [MeasurableSpace X] [MeasurableSpace Y]
    (Φ : Y → ℝ≥0 → X → X)
    (hΦ : Measurable (fun p : Y × ℝ≥0 × X => Φ p.1 p.2.1 p.2.2))
    (s : ℝ≥0) :
    Measurable (fun p : ((ℝ≥0 × X) ⊕ Unit) × (X × Y) =>
      p.1.elim (fun a => if a.1 ≤ s then Φ p.2.2 (s - a.1) a.2 else p.2.1)
        (fun _ => p.2.1)) := by
  classical
  let e := MeasurableEquiv.sumProdDistrib (ℝ≥0 × X) Unit (X × Y)
  have hl : Measurable (fun p : (ℝ≥0 × X) × (X × Y) =>
      if p.1.1 ≤ s then Φ p.2.2 (s - p.1.1) p.1.2 else p.2.1) := by
    apply Measurable.ite (measurableSet_le measurable_fst.fst measurable_const)
    · exact hΦ.comp (measurable_snd.snd.prodMk
        ((measurable_const.sub measurable_fst.fst).prodMk measurable_fst.snd))
    · exact measurable_snd.fst
  convert (hl.sumElim (measurable_snd.fst :
    Measurable (fun p : Unit × (X × Y) => p.2.1))).comp e.measurable using 1
  funext p
  rcases p with ⟨a | a, q⟩ <;> rfl

private theorem measurable_history_interpolation {X Y : Type*}
    [MeasurableSpace X] [MeasurableSpace Y]
    (Φ : Y → ℝ≥0 → X → X)
    (hΦ : Measurable (fun p : Y × ℝ≥0 × X => Φ p.1 p.2.1 p.2.2))
    (n : ℕ) (T : ℝ≥0)
    (h : Y → Fin n → ((ℝ≥0 × X) ⊕ Unit)) (hh : Measurable h)
    (z₀ : Y → X) (hz₀ : Measurable z₀) :
    Measurable (fun y => fun s : {s : ℝ≥0 // s ≤ T} =>
      Fin.foldl n (fun z j => (h y j).elim
        (fun a => if a.1 ≤ s.val then Φ y (s.val - a.1) a.2 else z)
        (fun _ => z)) (z₀ y)) := by
  classical
  apply measurable_pi_lambda
  intro s
  apply measurable_finite_fold n _ _ z₀ hz₀
  intro j
  exact (measurable_record_step Φ hΦ s.val).comp
    (((measurable_pi_apply j).comp (hh.comp measurable_snd)).prodMk measurable_id)

/- The last eligible index, rather than a maximum chosen by an unmeasurable
path-space operation, determines each coordinate of the literal fold. -/

private theorem finite_fold_last_eligible {X : Type*} (n : ℕ)
    (b : Fin n → Prop) [DecidablePred b] (v : Fin n → X) (x : X)
    (j : Fin n) (hj : b j) (hafter : ∀ k : Fin n, j < k → ¬ b k) :
    Fin.foldl n (fun z k => if b k then v k else z) x = v j := by
  induction n with
  | zero => exact Fin.elim0 j
  | succ n ih =>
    induction j using Fin.lastCases with
    | last => simp only [Fin.foldl_succ_last, if_pos hj]
    | cast j =>
      rw [Fin.foldl_succ_last, if_neg (hafter (Fin.last n) (Fin.castSucc_lt_last j))]
      exact ih (fun k => b k.castSucc) (fun k => v k.castSucc) j hj
        (fun k hk => hafter k.castSucc (Fin.castSucc_lt_castSucc_iff.mpr hk))


/- Small constructor identity suggested by the independent fragment diagnostic.
Keep case elimination outside the actual theorem's large literal context. -/

private theorem terminal_elim_identity {X : Type*} (T : ℝ≥0)
    (g : X → ℝ≥0 → ℝ≥0∞) (r : (ℝ≥0 × X) ⊕ Unit) :
    r.elim (fun a => g a.2 (T - r.elim Prod.fst (fun _ => 0))) (fun _ => 0) =
      r.elim (fun a => g a.2 (T - a.1)) (fun _ => 0) := by
  cases r <;> rfl

private theorem measurable_terminal_record_weight {X Y : Type*}
    [MeasurableSpace X] [MeasurableSpace Y]
    (L : Y → X → ℝ≥0 → ℝ)
    (hL : Measurable (fun p : (Y × X) × ℝ≥0 => L p.1.1 p.1.2 p.2))
    (T : ℝ≥0) :
    Measurable (fun p : ((ℝ≥0 × X) ⊕ Unit) × Y =>
      p.1.elim (fun a => ENNReal.ofReal (Real.exp (-L p.2 a.2 (T - a.1)))) (fun _ => 0)) := by
  let e := MeasurableEquiv.sumProdDistrib (ℝ≥0 × X) Unit Y
  have hl : Measurable (fun p : (ℝ≥0 × X) × Y =>
      ENNReal.ofReal (Real.exp (-L p.2 p.1.2 (T - p.1.1)))) :=
    (hL.comp (f := fun p : (ℝ≥0 × X) × Y => ((p.2, p.1.2), T - p.1.1))
      ((measurable_snd.prodMk measurable_fst.snd).prodMk
        (measurable_const.sub measurable_fst.fst))).neg.exp.ennreal_ofReal
  convert (hl.sumElim (measurable_const : Measurable (fun _ : Unit × Y => (0 : ℝ≥0∞)))).comp
    e.measurable using 1
  funext p
  rcases p with ⟨a | a, q⟩ <;> rfl

private theorem real_time_history_fold {X : Type*} (Φ : ℝ → X → X)
    (n : ℕ) (t : Fin n → ℝ) (ht : ∀ k, 0 ≤ t k) (z : Fin n → X) (z₀ : X)
    (s : ℝ≥0) (j : Fin n) (hj : t j ≤ (s : ℝ))
    (hafter : ∀ k : Fin n, j < k → (s : ℝ) < t k) :
    Fin.foldl n (fun x k => if Real.toNNReal (t k) ≤ s then
      Φ (((s - Real.toNNReal (t k)) : ℝ≥0) : ℝ) (z k) else x) z₀ =
      Φ ((s : ℝ) - t j) (z j) := by
  have hcoe (k : Fin n) : (Real.toNNReal (t k) : ℝ) = t k := Real.coe_toNNReal (t k) (ht k)
  have hj' : Real.toNNReal (t j) ≤ s := by
    exact_mod_cast (show (Real.toNNReal (t j) : ℝ) ≤ (s : ℝ) by rw [hcoe]; exact hj)
  have ha (k : Fin n) (hjk : j < k) : ¬ Real.toNNReal (t k) ≤ s := by
    intro hk
    have hkr : (Real.toNNReal (t k) : ℝ) ≤ (s : ℝ) := by exact_mod_cast hk
    rw [hcoe] at hkr
    exact not_lt_of_ge hkr (hafter k hjk)
  rw [finite_fold_last_eligible n (fun k => Real.toNNReal (t k) ≤ s)
    (fun k => Φ (((s - Real.toNNReal (t k)) : ℝ≥0) : ℝ) (z k)) z₀ j hj' ha,
    NNReal.coe_sub hj', hcoe]

private theorem actual_history_interpolation_measurable
    {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) :
    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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
    let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
    let Path : ℝ≥0 → Type _ := fun T => {s : ℝ≥0 // s ≤ T} → E × E
    let Ψ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Hist n → Path T :=
      fun y xRef z₀ n T h s =>
        Fin.foldl (n + 1) (fun z j => (h j).elim
          (fun a => if a.1 ≤ s.val then Φ y xRef ((s.val - a.1 : ℝ≥0) : ℝ) a.2 else z)
          (fun _ => z)) z₀
    ∀ n : ℕ, ∀ T : ℝ≥0,
      Measurable (fun p : ((E × E) × (E × E)) × Hist n =>
        Ψ p.1.1.1 p.1.1.2 p.1.2 n T p.2) := by
  classical
  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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
  let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
  let Path : ℝ≥0 → Type _ := fun T => {s : ℝ≥0 // s ≤ T} → E × E
  let Ψ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Hist n → Path T :=
    fun y xRef z₀ n T h s =>
      Fin.foldl (n + 1) (fun z j => (h j).elim
        (fun a => if a.1 ≤ s.val then Φ y xRef ((s.val - a.1 : ℝ≥0) : ℝ) a.2 else z)
        (fun _ => z)) z₀
  change ∀ n : ℕ, ∀ T : ℝ≥0,
    Measurable (fun p : ((E × E) × (E × E)) × Hist n =>
      Ψ p.1.1.1 p.1.1.2 p.1.2 n T p.2)
  have hf := AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHarmonicFlow.actual_harmonic_flow_laws
    hα hαβ hV hH hη hβη
  have hΦ : Measurable (fun a : (E × E) × ℝ × (E × E) =>
      Φ a.1.1 a.1.2 a.2.1 a.2.2) := hf.2.1
  intro n T
  let Y := ((E × E) × (E × E)) × Hist n
  have hΦY : Measurable (fun p : Y × ℝ≥0 × (E × E) =>
      Φ p.1.1.1.1 p.1.1.1.2 (p.2.1 : ℝ) p.2.2) :=
    hΦ.comp (f := fun p : Y × ℝ≥0 × (E × E) =>
      (p.1.1.1, (p.2.1 : ℝ), p.2.2)) (measurable_fst.fst.fst.prodMk
      ((measurable_coe_nnreal_real.comp measurable_snd.fst).prodMk measurable_snd.snd))
  exact measurable_history_interpolation
    (fun p : Y => fun t z => Φ p.1.1.1 p.1.1.2 (t : ℝ) z)
    hΦY (n + 1) T (fun p : Y => p.2) measurable_snd
    (fun p : Y => p.1.2) measurable_fst.snd