Actual PBPS one-step complete finite-history extension

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, arXiv2609.06905v1 Appendix A.1(A.1),(A.2),(A.7) and Appendix A.2. The explicit Borel complete-history append and its restricted next-history transport are attributed ASTIS completion of one iteration ingredient, not a printed standalone theorem. Full A.7 remains open.

arXiv2609.06905v1 · Chen-Chewi-Lu-Zhang arXiv2609.06905v1 Appendix A.1 (A.1),(A.2), one density/update iteration ingredient of (A.7), and Appendix A.2 finite-recursion Borel paragraph; attributed ASTIS source-implicit completion. · 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. For every deterministic n≥0 let Hist_n=D^(Fin(n+1)), H_n(w)=(R_j(ε(w)))_(0≤j≤n), and μ_n=(H_n)_*P. Define W(live(T,z),e)=τ_z(max(e,0)), W(stopped,e)=0 and t(r,e)=real(untopD_0 W(r,e)). Define ρ(live(T,z),s)=ofReal[λ_r(Φ_s z)exp(−Λ_z(max(s,0)))] and ρ(stopped,s)=0. Write A_n(h,s) for the complete history obtained by preserving every old coordinate h_j and appending live(T+max(s,0),S_rΦ_s z) when h_n=live(T,z), and appending stopped when h_n=stopped. Put L_n(h,s)=(A_n(h,s),s). Negative real times use the displayed raw-real harmonic flow with a clipped cumulative increment; this and the stopped branch are auxiliary totalizations, with actual positive finite jump identification only on the guard below. H_(n+1), A_n and L_n are Borel, and A_n(h,s)_j=h_j for every old index0≤j≤n and every abstract(h,s). For every fixed Borel d:Hist_n→[0,∞), each value finite but with no uniform bound, define D_d(h,s)=1_{0<s<d(h)}ρ(h_n,s), B_d={w:0<W(R_n(ε(w)),w_n)<d(H_n(w))}, X_n(w)=(H_n(w),t(R_n(ε(w)),w_n)), Y_n(w)=(H_(n+1)(w),t(R_n(ε(w)),w_n)) and ν_d=D_d(μ_n⊗real Lebesgue). B_d and Y_n are Borel. For every w∈B_d, H_(n+1)(w)=A_n(X_n(w)), preserving the actual old records and appending exactly the actual cumulative next time and post-bounce state. The actual restricted laws satisfy (Y_n)_*(P|B_d)=(L_n)_*ν_d and (H_(n+1))_*(P|B_d)=(A_n)_*ν_d, and ((L_n)_*ν_d)(Hist_(n+1)×ℝ)≤1. These are restricted finite-component laws; no unrestricted next-history law is asserted. For every jointly Borel F:Hist_(n+1)×ℝ→[0,∞], the function h↦∫_ℝF(L_n(h,s))D_d(h,s)ds is Borel. For every Borel A⊆Hist_n, ∫_{B_d∩{H_n∈A}}F(Y_n(w))P(dw)=∫_A[∫_ℝF(L_n(h,s))D_d(h,s)ds]μ_n(dh). No boundedness/integrability hypothesis on F, positive μ_n(A), normalized conditioning, constructor-law or measurability provider is assumed. The cases n=0, d=0, null A, stopped/infinite waits, zero hazard/normal, rank zero and unrealizable histories are included; infinite waits and zero/cutoff endpoints fail the strict guard, without an atom-equivalence assertion. This is attributed ASTIS completion of one actual complete-history extension ingredient implicit in Appendix A.1(A.7), using the already verified conditional finite-density law. Ordered absolute-time iteration, final survival/path-factor assembly, full(A.7), physical-time residual restart/Markovness, global conclusions, implementation/error/unbounded cost/main/composition/wholepaper/Goal remain OPEN. Survival88 and a separate no-atom theorem are not proof prerequisites.

E is a finite-dimensional real inner-product space with its Borel structure, including rank zero; V:E→ℝ is C².
The six original analytic hypotheses are α>0, α≤β, V∈C², α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v, η>0 and βη≤1, with α,β≥0.
y,r,z₀ and deterministic depth n are universally quantified. The actual stopped recursion and raw iid Exp1 product P are literal definitions.
d:Hist_n→NNReal is any fixed Borel finite-valued cutoff, possibly unbounded across histories; F:Hist_(n+1)×ℝ→ENNReal is any jointly Borel test, and A is any Borel old-history event, including null events.
Every history/append/lift measurability fact, actual guarded constructor identity and transported law is a conclusion, not an input premise. The strict finite guard is never normalized.

Actual complete-history extension 1

\[A_n(h,s)=\operatorname{snoc}\!\left(h,\begin{cases}\operatorname{live}(T+\max\{s,0\},S_r\Phi_s z),&h_n=\operatorname{live}(T,z),\\\mathrm{stopped},&h_n=\mathrm{stopped},\end{cases}\right)\quad L_n(h,s)=(A_n(h,s),s).\]

Actual complete-history extension 2

\[B_d=\{0<W_n<d(H_n)\},\quad D_d(h,s)=\mathbf1_{\{0<s<d(h)\}}\rho(h_n,s),\quad \nu_d=D_d(\mu_n\otimes ds).\]

Actual complete-history extension 3

\[w\in B_d\ \Longrightarrow\ H_{n+1}(w)=A_n(H_n(w),t_n(w)),\quad A_n(h,s)_j=h_j\ (0\le j\le n).\]

Actual complete-history extension 4

\[(Y_n)_*(P|_{B_d})=(L_n)_*\nu_d,\qquad(H_{n+1})_*(P|_{B_d})=(A_n)_*\nu_d,\qquad((L_n)_*\nu_d)(\mathrm{univ})\le1.\]

Actual complete-history extension 5

\[\int_{B_d\cap\{H_n\in A\}}F(Y_n)\,dP=\int_A\left[\int_{\mathbb R}F(L_n(h,s))D_d(h,s)\,ds\right]\mu_n(dh).\]

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 one-step complete finite-history extension

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteHistoryExtension.actual_finite_history_extension · theorem · Teaching coverage

Read this first

Mathematical statement

\[\int_{B_d\cap\{H_n\in A\}}F(Y_n)\,dP=\int_A\left[\int_{\mathbb R}F(L_n(h,s))D_d(h,s)\,ds\right]\mu_n(dh).\]

Lean statement · actual_finite_history_extension

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_history_extension
    {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_history_extension_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_finite_history_extension_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_history_extension_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 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 waitObs : E → E → (((ℝ≥0 × (E × E)) ⊕ Unit) × ℝ) → WithTop ℝ≥0 :=
      fun y xRef q => match q.1 with
        | Sum.inl a => τ y xRef a.2 (Real.toNNReal q.2)
        | Sum.inr _ => 0
    let timeObs : E → E → (((ℝ≥0 × (E × E)) ⊕ Unit) × ℝ) → ℝ :=
      fun y xRef q => ((waitObs y xRef q).untopD 0 : ℝ≥0)
    let density : E → E → (((ℝ≥0 × (E × E)) ⊕ Unit) × ℝ) → ℝ≥0∞ :=
      fun y xRef q => match q.1 with
        | Sum.inl a => ENNReal.ofReal (rate xRef (Φ y xRef q.2 a.2) *
            Real.exp (-Λ y xRef a.2 (Real.toNNReal q.2)))
        | Sum.inr _ => 0
    ∀ y xRef : E, ∀ z₀ : E × E, ∀ n : ℕ,
      let Rec := (ℝ≥0 × (E × E)) ⊕ Unit
      let Hist := Fin (n + 1) → Rec
      let HistNext := Fin (n + 2) → Rec
      let last : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
      let H : (ℕ → ℝ) → Hist := history y xRef z₀ n
      let Hnext : (ℕ → ℝ) → HistNext := history y xRef z₀ (n + 1)
      let append : Hist × ℝ → HistNext := fun p =>
        Fin.snoc p.1 (match p.1 last with
          | Sum.inl a => Sum.inl (a.1 + Real.toNNReal p.2,
              S xRef (Φ y xRef p.2 a.2))
          | Sum.inr _ => Sum.inr ())
      let lift : Hist × ℝ → HistNext × ℝ := fun p => (append p, p.2)
      Measurable Hnext ∧ Measurable append ∧ Measurable lift ∧
      (∀ p : Hist × ℝ, ∀ j : Fin (n + 1), append p j.castSucc = p.1 j) ∧
      (∀ d : Hist → ℝ≥0, Measurable d →
        let μ : Measure Hist := Measure.map H P
        let D : Hist → ℝ → ℝ≥0∞ := fun h s =>
          if 0 < s ∧ s < (d h : ℝ) then density y xRef (h last, s) else 0
        let B : Set (ℕ → ℝ) := {w |
          (0 : WithTop ℝ≥0) < waitObs y xRef (record y xRef z₀ (ε w) n, w n) ∧
          waitObs y xRef (record y xRef z₀ (ε w) n, w n) <
            ((d (H w) : ℝ≥0) : WithTop ℝ≥0)}
        let X : (ℕ → ℝ) → Hist × ℝ := fun w =>
          (H w, timeObs y xRef (record y xRef z₀ (ε w) n, w n))
        let Y : (ℕ → ℝ) → HistNext × ℝ := fun w =>
          (Hnext w, timeObs y xRef (record y xRef z₀ (ε w) n, w n))
        let ν : Measure (Hist × ℝ) := (μ.prod (volume : Measure ℝ)).withDensity
          (fun p => D p.1 p.2)
        MeasurableSet B ∧ Measurable Y ∧
        (∀ w ∈ B, Hnext w = append (X w)) ∧
        Measure.map Y (P.restrict B) = Measure.map lift ν ∧
        Measure.map Hnext (P.restrict B) = Measure.map append ν ∧
        (Measure.map lift ν) Set.univ ≤ 1 ∧
        (∀ F : HistNext × ℝ → ℝ≥0∞, Measurable F →
          Measurable (fun h => ∫⁻ s : ℝ, F (lift (h, s)) * D h s) ∧
          (∀ A : Set Hist, MeasurableSet A →
            (∫⁻ w in B ∩ H ⁻¹' A, F (Y w) ∂P) =
              ∫⁻ h in A, (∫⁻ s : ℝ, F (lift (h, s)) * D h s) ∂μ)))

set_option maxHeartbeats 1600000 in

Exact module and namespace context

Proof roadmap

1Keep the actual model and complete next history
Retain all14 literal model/input/observer definitions. Consume the verified conditional density law, finite-history Borel law and actual harmonic flow/reflection producers under the same six source hypotheses. Fix n,y,r,z₀. Define the old and next complete histories, append A_n and paired lift L_n. The append uses Fin.snoc, so it retains every earlier record; its last entry is the literal cumulative-time and reflected-flow update. Its negative-time and stopped branches are declared auxiliary totalizations, not positive finite jump laws.
2Prove the complete append and next history are Borel
The verified actual-history theorem at n+1 gives Borel H_(n+1), including the integrated-hazard/threshold-crossing/finite-recursion ingredients already proved there. For the append update, distribute the live/stopped record sum over real time. On live records the actual harmonic flow is jointly continuous/Borel and the zero-safe reflection is Borel; adding max(s,0) to the cumulative time is Borel. The stopped branch is constant. For every next-history coordinate, split into the new last entry and an old castSucc entry. These are respectively the Borel update and an old-history projection, proving Borel A_n. Pairing with s gives Borel L_n. Fin.snoc_castSucc proves exact preservation of every old entry for all abstract histories and real times.
3Reuse the exact strict finite-density component
Fix any Borel finite-valued d, with no uniform bound. Define μ_n,D_d,B_d,X_n,Y_n and ν_d literally. Producer89 supplies Borel B_d and X_n, the exact restricted law (X_n)_*(P|B_d)=ν_d, ν_d mass≤1, and all nonnegative joint tests on old histories. Combining Borel H_(n+1) with the real-time projection of X_n gives Borel Y_n. No density, independence, finite wait or measurability is introduced as a new premise.
4Identify the actual full recursion on the finite guard
Take w∈B_d. If its current record is stopped then W_n=0 contradicts the positive guard. For a live record (T,z), τ_z(ε_n)=∞ contradicts the finite upper bound, so the actual next branch is live. Split the next finite history into its final index and the earlier indices. Earlier entries are unchanged by definition. At the final index, unfold Nat.rec once: the source next record is live(T+untopD₀τ,S_rΦ_(real untopD₀τ)z). The observed t_n is precisely real untopD₀τ and toNNReal(t_n)=untopD₀τ, so this equals the appended final record. Thus H_(n+1)=A_n∘X_n pointwise on B_d and Y_n=L_n∘X_n there. No endpoint-mass or restart argument is used.
5Transport the actual joint law and its marginal
Pointwise equality on the Borel event gives equality almost everywhere under P restricted to B_d. Replace Y_n by L_n∘X_n in its pushforward, compose measurable pushforwards, and use the exact89 joint law to obtain (L_n)_*ν_d. Apply the same argument directly to H_(n+1)=A_n∘X_n for the marginal. Since L_n is measurable, the total mass of its pushforward is exactly ν_d(univ), hence≤1 by89. This is a subprobability mass bound, without renormalizing missing mass or claiming an unrestricted next-history distribution.
6Integrate every joint test on every old-history event
For jointly Borel ENNReal F on the extended history and relative time, F∘L_n is a jointly Borel test admitted by89. Its parameter integral is Borel, even when infinite. For any Borel old-history A, use the pointwise Y_n=L_n(X_n) identity throughout B_d∩{H_n∈A} to replace the actual integrand. Producer89 then gives the displayed unnormalized iterated integral. Null A, unbounded F and unbounded finite-valued d require no additional premise. The result closes one actual next-history extension step; ordered absolute-time iteration and the terminal survival factor remain separate.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product space with its Borel structure, including rank zero; V:E→ℝ is C².
The six original analytic hypotheses are α>0, α≤β, V∈C², α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v, η>0 and βη≤1, with α,β≥0.
y,r,z₀ and deterministic depth n are universally quantified. The actual stopped recursion and raw iid Exp1 product P are literal definitions.
d:Hist_n→NNReal is any fixed Borel finite-valued cutoff, possibly unbounded across histories; F:Hist_(n+1)×ℝ→ENNReal is any jointly Borel test, and A is any Borel old-history event, including null events.
Every history/append/lift measurability fact, actual guarded constructor identity and transported law is a conclusion, not an input premise. The strict finite guard is never normalized.

Mathematical proof

1. Keep the actual model and complete next history

Retain all14 literal model/input/observer definitions. Consume the verified conditional density law, finite-history Borel law and actual harmonic flow/reflection producers under the same six source hypotheses. Fix n,y,r,z₀. Define the old and next complete histories, append A_n and paired lift L_n. The append uses Fin.snoc, so it retains every earlier record; its last entry is the literal cumulative-time and reflected-flow update. Its negative-time and stopped branches are declared auxiliary totalizations, not positive finite jump laws.

Corresponding Lean step

  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 τ : 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 waitObs : E → E → (((ℝ≥0 × (E × E)) ⊕ Unit) × ℝ) → WithTop ℝ≥0 :=
    fun y xRef q => match q.1 with
      | Sum.inl a => τ y xRef a.2 (Real.toNNReal q.2)
      | Sum.inr _ => 0
  let timeObs : E → E → (((ℝ≥0 × (E × E)) ⊕ Unit) × ℝ) → ℝ :=
    fun y xRef q => ((waitObs y xRef q).untopD 0 : ℝ≥0)
  let density : E → E → (((ℝ≥0 × (E × E)) ⊕ Unit) × ℝ) → ℝ≥0∞ :=
    fun y xRef q => match q.1 with
      | Sum.inl a => ENNReal.ofReal (rate xRef (Φ y xRef q.2 a.2) *
          Real.exp (-Λ y xRef a.2 (Real.toNNReal q.2)))
      | Sum.inr _ => 0
  change
    ∀ y xRef : E, ∀ z₀ : E × E, ∀ n : ℕ,
      let Rec := (ℝ≥0 × (E × E)) ⊕ Unit
      let Hist := Fin (n + 1) → Rec
      let HistNext := Fin (n + 2) → Rec
      let last : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
      let H : (ℕ → ℝ) → Hist := history y xRef z₀ n
      let Hnext : (ℕ → ℝ) → HistNext := history y xRef z₀ (n + 1)
      let append : Hist × ℝ → HistNext := fun p =>
        Fin.snoc p.1 (match p.1 last with
          | Sum.inl a => Sum.inl (a.1 + Real.toNNReal p.2,
              S xRef (Φ y xRef p.2 a.2))
          | Sum.inr _ => Sum.inr ())
      let lift : Hist × ℝ → HistNext × ℝ := fun p => (append p, p.2)
      Measurable Hnext ∧ Measurable append ∧ Measurable lift ∧
      (∀ p : Hist × ℝ, ∀ j : Fin (n + 1), append p j.castSucc = p.1 j) ∧
      (∀ d : Hist → ℝ≥0, Measurable d →
        let μ : Measure Hist := Measure.map H P
        let D : Hist → ℝ → ℝ≥0∞ := fun h s =>
          if 0 < s ∧ s < (d h : ℝ) then density y xRef (h last, s) else 0
        let B : Set (ℕ → ℝ) := {w |
          (0 : WithTop ℝ≥0) < waitObs y xRef (record y xRef z₀ (ε w) n, w n) ∧
          waitObs y xRef (record y xRef z₀ (ε w) n, w n) <
            ((d (H w) : ℝ≥0) : WithTop ℝ≥0)}
        let X : (ℕ → ℝ) → Hist × ℝ := fun w =>
          (H w, timeObs y xRef (record y xRef z₀ (ε w) n, w n))
        let Y : (ℕ → ℝ) → HistNext × ℝ := fun w =>
          (Hnext w, timeObs y xRef (record y xRef z₀ (ε w) n, w n))
        let ν : Measure (Hist × ℝ) := (μ.prod (volume : Measure ℝ)).withDensity
          (fun p => D p.1 p.2)
        MeasurableSet B ∧ Measurable Y ∧
        (∀ w ∈ B, Hnext w = append (X w)) ∧
        Measure.map Y (P.restrict B) = Measure.map lift ν ∧
        Measure.map Hnext (P.restrict B) = Measure.map append ν ∧
        (Measure.map lift ν) Set.univ ≤ 1 ∧
        (∀ F : HistNext × ℝ → ℝ≥0∞, Measurable F →
          Measurable (fun h => ∫⁻ s : ℝ, F (lift (h, s)) * D h s) ∧
          (∀ A : Set Hist, MeasurableSet A →
            (∫⁻ w in B ∩ H ⁻¹' A, F (Y w) ∂P) =
              ∫⁻ h in A, (∫⁻ s : ℝ, F (lift (h, s)) * D h s) ∂μ)))
  have hdensity := ActualConditionalNextWaitDensity.actual_conditional_next_wait_density
    hα hαβ hV hH hη hβη
  have hhistory := ActualFiniteHistoryTailLaw.actual_finite_history_tail_law
    hα hαβ hV hH hη hβη
  have hflow := ActualHarmonicFlow.actual_harmonic_flow_laws hα hαβ hV hH hη hβη
  have hbounce := ActualBounceRate.actual_bounce_rate_energy_laws hα hαβ hV hH hη hβη
  intro y xRef z₀ n
  let Rec := (ℝ≥0 × (E × E)) ⊕ Unit
  let Hist := Fin (n + 1) → Rec
  let HistNext := Fin (n + 2) → Rec
  let last : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
  let H : (ℕ → ℝ) → Hist := history y xRef z₀ n
  let Hnext : (ℕ → ℝ) → HistNext := history y xRef z₀ (n + 1)
  let append : Hist × ℝ → HistNext := fun p =>
    Fin.snoc p.1 (match p.1 last with
      | Sum.inl a => Sum.inl (a.1 + Real.toNNReal p.2,
          S xRef (Φ y xRef p.2 a.2))
      | Sum.inr _ => Sum.inr ())
  let lift : Hist × ℝ → HistNext × ℝ := fun p => (append p, p.2)
  change Measurable Hnext ∧ Measurable append ∧ Measurable lift ∧
    (∀ p : Hist × ℝ, ∀ j : Fin (n + 1), append p j.castSucc = p.1 j) ∧ _