Actual PBPS prescribed-path hazard and density identity

Chen, Chewi, Lu and Zhang, arXiv:2609.06905v1, Appendix A.1; faithful attributed restatement and ASTIS proof of the source-implicit finite prescribed-path density ingredient, not verbatim text.

arXiv2609.06905v1 · Chen-Chewi-Lu-Zhang arXiv2609.06905v1 Appendix A.1 (A.1),(A.2), prescribed trajectories and (A.7) finite-sector density. Source graph DENSITY94/HAZARD93/LEFT93/TERM93. · faithful paraphrase

Complete source statement (Samplinglib restatement)

Let E be a finite-dimensional real inner-product space equipped with its Borel sigma algebra; zero dimension is allowed. Let alpha,beta>=0, eta be real, V:E->R. Assume exactly alpha>0, alpha<=beta, V is C2, alpha||v||^2<=D2V(x)[v,v]<=beta||v||^2 for every x,v, eta>0 and beta*eta<=1. All conclusions hold for every y,r in E, initial phase z0=(x0,p0), integer n>=0 and finite T>=0. Set c=y-eta*grad V(r). For z=(x,p), define Phi_u(z)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p). Define h_r(x)=grad V(x)-grad V(r), S_r(x,p)=(x,p-[2<p,h_r(x)>/||h_r(x)||^2]h_r(x)) with real division totalized by 0/0=0, lambda_r(x,p)=sqrt(eta)max(0,<p,h_r(x)>), and Lambda_z(u)=integral from0 to u of lambda_r(Phi_s(z)) ds for u>=0, using Lebesgue measure. A tagged record is either live(a,z), with a>=0, or stopped; Hist_n is the type of all n+1 records. Let Delta_n(T) be the strict simplex 0<t1<...<tn<T. Write a0=0, ai=ti (1<=i<=n), a_(n+1)=T. Given t in Delta_n(T), define z_i=S_r(Phi_(a_i-a_(i-1))(z_(i-1))) for1<=i<=n and K_n(t)_j=live(a_j,z_j). The literal Lean nonnegative conversions preserve these nonnegative times. Define qReal_n(t)=product_(i=1)^n [lambda_r(Phi_(a_i-a_(i-1))(z_(i-1))) exp(-Lambda_(z_(i-1))(a_i-a_(i-1)))], q_n=ofReal(qReal_n). For arbitrary histories let readTime(live(a,z))=a and readTime(stopped)=0; d_n(T,h)=max(T-readTime(h_n),0). Put W(live(a,z),u)=ofReal(exp(-Lambda_z(u))) and W(stopped,u)=0. Define rho_n(T,t)=q_n(t) W(K_n(t)_n,d_n(T,K_n(t))). Here ofReal(x) is max(x,0) embedded into extended nonnegative reals; no probability law or normalization is assumed in this deterministic identity. Define Path_T as all phase-valued functions on[0,T]. The total interpolation Psi_n(h)(s) starts at z0 and scans records j=0,...,n in order: a live(a,z) record with a<=s replaces the accumulator by Phi_(max(s-a,0))(z); otherwise it is unchanged. Set Gamma_n(t)=Psi_n(K_n(t)). Extend this particular prescribed path to all real times by gamma(s)=Gamma_n(t)(min(max(s,0),T)). This extension agrees with Gamma on[0,T]; no topology on an entire function space is asserted. Then lambda_r(gamma(s)) is Lebesgue interval integrable on[0,T], and integral_0^T lambda_r(gamma(s)) ds=sum_(j=0)^n Lambda_(z_j)(a_(j+1)-a_j). For every1<=i<=n, gamma(s) tends from the left at a_i to Phi_(a_i-a_(i-1))(z_(i-1)), and lambda_r(gamma(s)) tends from the left to lambda_r of that same incoming phase. Consequently rho_n(T,t)=ofReal(exp(-integral_0^T lambda_r(gamma(s))ds) * product_(i=1)^n lambda_r(Phi_(a_i-a_(i-1))(z_(i-1)))). The density evaluates the incoming phase, not the reflected value at the jump. These conclusions include n=0 (one survival arc, empty product1), T=0 (only the zero-event simplex is inhabited), zero-dimensional E and zero rates; no positivity of event densities is assumed. All integrability, continuity along arcs, left limits and identities are proved, not additional premises. This is an attributed ASTIS completion of the prescribed-trajectory hazard/left-limit ingredient of Appendix A.1 around(A.7), not a quoted standalone theorem. Composing it with the finite-count path law, summing over all counts, signed-observable convergence, Skorokhod compatibility, restart/Markovness, invariance, hypocoercivity, implementation errors, unbounded expected costs and the main paper/composition results remain separate obligations.

Finite-dimensional real inner-product Borel E, including rank zero; alpha,beta are nonnegative.
Six original analytic assumptions: alpha>0, alpha<=beta, V is C2, alpha||v||^2<=D2V(x)[v,v]<=beta||v||^2 for all x,v, eta>0, beta*eta<=1.
All y,r,z0, finite n and T>=0, and all strictly ordered prescribed event tuples are universally quantified.
Flow, reflection, rate, integrated arc hazard, tagged histories, finite interpolation and density are explicit definitions inherited literally from the actual finite-count law.
Integrability and incoming left limits are conclusions. No continuity of the reflection at a vanishing normal, positive density, supplied path law or stochastic independence premise is added.

Prescribed path identity 1

\[a_0=0,\quad a_i=t_i\ (1\le i\le n),\quad a_{n+1}=T;\qquad 0<t_1<\cdots<t_n<T\ (n>0),\quad z_i=S_r\Phi_{a_i-a_{i-1}}z_{i-1}.\]

Prescribed path identity 2

\[\gamma(s)=\Gamma_n(t)(\min\{\max\{s,0\},T\}),\quad \gamma(s)=\Phi_{s-a_j}z_j\quad(a_j<s<a_{j+1}).\]

Prescribed path identity 3

\[\int_0^T\lambda_r(\gamma(s))\,ds=\sum_{j=0}^{n}\Lambda_{z_j}(a_{j+1}-a_j).\]

Prescribed path identity 4

\[\lim_{s\uparrow a_i}\gamma(s)=\Phi_{a_i-a_{i-1}}z_{i-1},\qquad\lim_{s\uparrow a_i}\lambda_r(\gamma(s))=\lambda_r(\Phi_{a_i-a_{i-1}}z_{i-1}).\]

Prescribed path identity 5

\[\rho_n(T,t)=\operatorname{ofReal}\!\left[e^{-\int_0^T\lambda_r(\gamma(s))\,ds}\prod_{i=1}^{n}\lambda_r(\Phi_{a_i-a_{i-1}}z_{i-1})\right].\]

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 prescribed-path hazard and density identity

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedPathDensity.actual_prescribed_path_density_rewrite · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product space equipped with its Borel sigma algebra; zero dimension is allowed. Let alpha,beta≥0, eta be real, V:E→R. Assume exactly alpha>0, alpha≤beta, V is C2, alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for every x,v, eta>0 and beta*eta≤1. All conclusions hold for every y,r in E, initial phase z0=(x0,p0), integer n≥0 and finite T≥0. Set c=y-eta*grad V(r). For z=(x,p), define Phi_u(z)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p). Define h_r(x)=grad V(x)-grad V(r), S_r(x,p)=(x,p-[2<p,h_r(x)>/||h_r(x)||^2]h_r(x)) with real division totalized by 0/0=0, lambda_r(x,p)=sqrt(eta)max(0,<p,h_r(x)>), and Lambda_z(u)=integral from0 to u of lambda_r(Phi_s(z)) ds for u≥0, using Lebesgue measure. A tagged record is either live(a,z), with a≥0, or stopped; Hist_n is the type of all n+1 records. Let Delta_n(T) be the strict simplex 0<t1<...<tn<T. Write a0=0, ai=ti (1≤i≤n), a_(n+1)=T. Given t in Delta_n(T), define z_i=S_r(Phi_(a_i-a_(i-1))(z_(i-1))) for1≤i≤n and K_n(t)_j=live(a_j,z_j). The literal Lean nonnegative conversions preserve these nonnegative times. Define qReal_n(t)=product_(i=1)^n [lambda_r(Phi_(a_i-a_(i-1))(z_(i-1))) exp(-Lambda_(z_(i-1))(a_i-a_(i-1)))], q_n=ofReal(qReal_n). For arbitrary histories let readTime(live(a,z))=a and readTime(stopped)=0; d_n(T,h)=max(T-readTime(h_n),0). Put W(live(a,z),u)=ofReal(exp(-Lambda_z(u))) and W(stopped,u)=0. Define rho_n(T,t)=q_n(t) W(K_n(t)_n,d_n(T,K_n(t))). Here ofReal(x) is max(x,0) embedded into extended nonnegative reals; no probability law or normalization is assumed in this deterministic identity. Define Path_T as all phase-valued functions on[0,T]. The total interpolation Psi_n(h)(s) starts at z0 and scans records j=0,...,n in order: a live(a,z) record with a≤s replaces the accumulator by Phi_(max(s-a,0))(z); otherwise it is unchanged. Set Gamma_n(t)=Psi_n(K_n(t)). Extend this particular prescribed path to all real times by gamma(s)=Gamma_n(t)(min(max(s,0),T)). This extension agrees with Gamma on[0,T]; no topology on an entire function space is asserted. Then lambda_r(gamma(s)) is Lebesgue interval integrable on[0,T], and integral_0^T lambda_r(gamma(s)) ds=sum_(j=0)^n Lambda_(z_j)(a_(j+1)-a_j). For every1≤i≤n, gamma(s) tends from the left at a_i to Phi_(a_i-a_(i-1))(z_(i-1)), and lambda_r(gamma(s)) tends from the left to lambda_r of that same incoming phase. Consequently rho_n(T,t)=ofReal(exp(-integral_0^T lambda_r(gamma(s))ds) * product_(i=1)^n lambda_r(Phi_(a_i-a_(i-1))(z_(i-1)))). The density evaluates the incoming phase, not the reflected value at the jump. These conclusions include n=0 (one survival arc, empty product1), T=0 (only the zero-event simplex is inhabited), zero-dimensional E and zero rates; no positivity of event densities is assumed. All integrability, continuity along arcs, left limits and identities are proved, not additional premises. This is an attributed ASTIS completion of the prescribed-trajectory hazard/left-limit ingredient of Appendix A.1 around(A.7), not a quoted standalone theorem. Composing it with the finite-count path law, summing over all counts, signed-observable convergence, Skorokhod compatibility, restart/Markovness, invariance, hypocoercivity, implementation errors, unbounded expected costs and the main paper/composition results remain separate obligations.

\[\rho_n(T,t)=\operatorname{ofReal}\!\left[e^{-\int_0^T\lambda_r(\gamma(s))\,ds}\prod_{i=1}^{n}\lambda_r(\Phi_{a_i-a_{i-1}}z_{i-1})\right].\]

Lean statement · actual_prescribed_path_density_rewrite

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_prescribed_path_density_rewrite
    {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 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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
    let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
    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 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 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 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 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))
    ∀ y xRef : E, ∀ z₀ : E × E, ∀ n : ℕ, ∀ T : ℝ≥0, ∀ t : Prefix n T,
      let grid : Fin (n + 2) → ℝ :=
        Fin.snoc (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ)) (T : ℝ)
      let γ : ℝ → E × E := fun s =>
        Γ y xRef z₀ n T t ⟨min (Real.toNNReal s) T, min_le_right _ _⟩
      IntervalIntegrable (fun s => rate xRef (γ s)) volume 0 (T : ℝ) ∧
      (∫ s in (0 : ℝ)..(T : ℝ), rate xRef (γ s)) =
        ∑ j : Fin (n + 1), Λ y xRef (zAt y xRef z₀ n T t j)
          (Real.toNNReal (grid j.succ - grid j.castSucc)) ∧
      (∀ i : Fin n,
        Tendsto γ (𝓝[<] (t.val i))
          (𝓝 (Φ y xRef (t.val i - grid i.castSucc.castSucc)
            (zAt y xRef z₀ n T t i.castSucc))) ∧
        Tendsto (fun s => rate xRef (γ s)) (𝓝[<] (t.val i))
          (𝓝 (rate xRef (Φ y xRef (t.val i - grid i.castSucc.castSucc)
            (zAt y xRef z₀ n T t i.castSucc))))) ∧
      ρ y xRef z₀ n T t = ENNReal.ofReal
        (Real.exp (-(∫ s in (0 : ℝ)..(T : ℝ), rate xRef (γ s))) *
          ∏ i : Fin n, rate xRef (Φ y xRef (t.val i - grid i.castSucc.castSucc)
            (zAt y xRef z₀ n T t i.castSucc)))

Exact module and namespace context

Proof roadmap

1Identify the actual prescribed open arcs
Append T to the strictly increasing list beginning at0. The resulting grid is nondecreasing, also when n=0 and T=0. For a_j<s<a_(j+1), monotonicity gives0≤s≤T, so the clamp equals s. Every later record has time greater than s. Apply the already proved last-eligible-record formula of the actual finite-count path law to obtain gamma(s)=Phi_(s-a_j)(z_j). This uses the existing interpolation rather than a newly postulated path.
2Ignore endpoint values only for integration
Assume a≤b. A continuous comparison function g is integrable on every finite interval. If f=g on the open interval(a,b), changing the two endpoint values does not change Lebesgue interval integrability or its integral. Transfer integrability with congr_uIoo and the integral with integral_congr_Ioo_of_le. The a=b case is included; no equality or continuity at a jump is required.
3Sum the finite adjacent integrals
Let the grid be nondecreasing; for every j assume g_j is continuous and f=g_j on(a_j,a_(j+1)). Induct on the number of grid intervals. The zero-interval integral and empty sum vanish. At the successor step, integrability of the prefix and last arc gives integrability of their union. The adjacent-interval identity adds the last integral, and the finite sum splits into its prefix and last index. This proves the exact sum for any nondecreasing finite grid without requiring positive lengths.
4Determine an incoming limit from the preceding arc
If a<b, the interval(a,b) is eventually visited by the left-neighborhood filter at b. On that interval the function equals its continuous incoming comparison arc. Restrict the continuous limit to the left filter and transfer it through eventual equality. The value assigned at b itself has no role; in particular a post-bounce value at b does not replace the incoming limit.
5Apply arc calculus to the actual phase and rate
The actual harmonic-flow theorem supplies joint flow continuity, and the actual bounce-rate theorem supplies rate continuity. Compose them with s→s-a_j to obtain continuous incoming phase and rate arcs. The open-arc identity supplies the comparison equalities. Apply finite integration and translate each interval by a_j; its nonnegative length is exactly the argument of Lambda_(z_j). For each strict interior event a_i, the predecessor gap is positive. Apply the left-limit lemma to that phase arc, then compose with the continuous rate. Clamping is only an auxiliary real-time extension and is inactive on these open arcs.
6Combine all exponential survival factors
Distribute the finite product into rate factors and exponential factors. The product of exponentials is the exponential of the sum. Multiply by the terminal survival exponential and append the final hazard term to the finite sum. This is a real algebraic identity for arbitrary rates and hazards, so zero rates and the empty product do not require division or positivity.
7Rewrite the original finite-count density
Retain the exact twenty inherited definitions and six analytic assumptions. The simplex shows0≤a_n≤T, so the truncated terminal duration T-toNNReal(a_n) equals toNNReal(T-a_n). Thus the original tagged terminal weight is precisely ofReal(exp(-h_n)). The prefix density is the product of the n incoming rates and their arc survivals. Since the terminal exponential is nonnegative, ofReal transports multiplication exactly. Apply the product identity and substitute the proved integrated-hazard sum. Together with integrability and both incoming limits this closes the full frozen proposition. No normalization, all-count summation or signed-observable convergence is asserted.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real inner-product Borel E, including rank zero; alpha,beta are nonnegative.
Six original analytic assumptions: alpha>0, alpha≤beta, V is C2, alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for all x,v, eta>0, beta*eta≤1.
All y,r,z0, finite n and T≥0, and all strictly ordered prescribed event tuples are universally quantified.
Flow, reflection, rate, integrated arc hazard, tagged histories, finite interpolation and density are explicit definitions inherited literally from the actual finite-count law.
Integrability and incoming left limits are conclusions. No continuity of the reflection at a vanishing normal, positive density, supplied path law or stochastic independence premise is added.

Mathematical proof

1. Identify the actual prescribed open arcs

Append T to the strictly increasing list beginning at0. The resulting grid is nondecreasing, also when n=0 and T=0. For a_j<s<a_(j+1), monotonicity gives0≤s≤T, so the clamp equals s. Every later record has time greater than s. Apply the already proved last-eligible-record formula of the actual finite-count path law to obtain gamma(s)=Phi_(s-a_j)(z_j). This uses the existing interpolation rather than a newly postulated path.

\[\gamma(s)=\Gamma_n(t)(\min\{\max\{s,0\},T\}),\quad \gamma(s)=\Phi_{s-a_j}z_j\quad(a_j<s<a_{j+1}).\]

Corresponding Lean step

private theorem actual_arc
    {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 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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
    let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
    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 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 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 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 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))
    ∀ y xRef : E, ∀ z₀ : E × E, ∀ n : ℕ, ∀ T : ℝ≥0, ∀ t : Prefix n T,
      let grid : Fin (n + 2) → ℝ :=
        Fin.snoc (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ)) (T : ℝ)
      let γ : ℝ → E × E := fun s =>
        Γ y xRef z₀ n T t ⟨min (Real.toNNReal s) T, min_le_right _ _⟩
      Monotone grid ∧ grid 0 = 0 ∧ grid (Fin.last (n+1)) = (T : ℝ) ∧
      ∀ j : Fin (n+1), EqOn γ
        (fun s => Φ y xRef (s - grid j.castSucc) (zAt y xRef z₀ n T t j))
        (Ioo (grid j.castSucc) (grid j.succ)) := 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 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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
  let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
  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 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 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 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 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))
  change
    ∀ y xRef : E, ∀ z₀ : E × E, ∀ n : ℕ, ∀ T : ℝ≥0, ∀ t : Prefix n T,
      let grid : Fin (n + 2) → ℝ :=
        Fin.snoc (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ)) (T : ℝ)
      let γ : ℝ → E × E := fun s =>
        Γ y xRef z₀ n T t ⟨min (Real.toNNReal s) T, min_le_right _ _⟩
      Monotone grid ∧ grid 0 = 0 ∧ grid (Fin.last (n+1)) = (T : ℝ) ∧
      ∀ j : Fin (n+1), EqOn γ
        (fun s => Φ y xRef (s - grid j.castSucc) (zAt y xRef z₀ n T t j))
        (Ioo (grid j.castSucc) (grid j.succ))
  intro y xRef z₀ n T t
  let a : Fin (n+1) → ℝ := Fin.cons 0 t.val
  let grid : Fin (n+2) → ℝ := Fin.snoc a (T : ℝ)
  let γ : ℝ → E × E := fun s =>
    Γ y xRef z₀ n T t ⟨min (Real.toNNReal s) T, min_le_right _ _⟩
  change Monotone grid ∧ grid 0 = 0 ∧ grid (Fin.last (n+1)) = (T : ℝ) ∧ _
  have ham : StrictMono a := t.property.1
  have ha0 : a 0 = 0 := rfl
  have haT : ∀ j, a j ≤ (T : ℝ) := by
    intro j
    refine Fin.cases ?_ (fun i => ?_) j
    · simpa [a] using T.coe_nonneg
    · exact (t.property.2 i).le
  have hgrid : Monotone grid := by
    intro i j hij
    induction i using Fin.lastCases with
    | last =>
      have hj : j = Fin.last (n+1) := le_antisymm (Fin.le_last j) hij
      subst j
      exact le_rfl
    | cast i =>
      induction j using Fin.lastCases with
      | last => simpa [grid] using haT i
      | cast j => simpa [grid] using ham.monotone (show i ≤ j from hij)
  have hg0 : grid 0 = 0 := by simp [grid, a]
  have hgT : grid (Fin.last (n+1)) = (T : ℝ) := by simp [grid]
  refine ⟨hgrid, hg0, hgT, ?_⟩
  obtain ⟨Z, _, _, _, _, hlaw⟩ :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteCountPath.actual_finite_count_path_law
      hα hαβ hV hH hη hβη
  have harc := ((hlaw n T).2.2.2 y xRef z₀).2.2.2.2.1
  intro j s hs
  have hs0 : 0 ≤ s := by
    have := hgrid (show (0 : Fin (n+2)) ≤ j.castSucc from Fin.zero_le _)
    rw [hg0] at this
    exact (this.trans hs.1.le)
  have hsT : s ≤ (T : ℝ) := by
    have := hgrid (Fin.le_last j.succ)
    rw [hgT] at this
    exact hs.2.le.trans this
  have hclip : min (Real.toNNReal s) T = Real.toNNReal s :=
    min_eq_left (by exact_mod_cast (Real.toNNReal_le_iff_le_coe).2 hsT)
  have hclipcoe : ((min (Real.toNNReal s) T : ℝ≥0) : ℝ) = s := by
    rw [hclip, Real.coe_toNNReal s hs0]
  have hstart : a j ≤ s := by simpa [grid] using hs.1.le
  have hafter : ∀ k : Fin (n+1), j < k → s < a k := by
    intro k hjk
    have hidx : j.succ ≤ k.castSucc := by exact_mod_cast hjk
    have hle := hgrid hidx
    exact hs.2.trans_le (by simpa [grid] using hle)
  have hh := harc t ⟨min (Real.toNNReal s) T, min_le_right _ _⟩ j
    (by simpa only [hclipcoe] using hstart)
    (by simpa only [hclipcoe] using hafter)
  simpa only [hclipcoe, Fin.snoc_castSucc] using hh