Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Actual PBPS next absolute-event-time law

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. This explicit actual-history absolute-time density is attributed ASTIS completion of an implicit coordinate step; it is not a quoted standalone source theorem.

arXiv2609.06905v1 · Chen-Chewi-Lu-Zhang arXiv2609.06905v1 Appendix A.1 (A.1),(A.2), one absolute-time coordinate ingredient of (A.7), and Appendix A.2; 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 define Rec=([0,∞)×(E×E))⊕{stopped}, Hist_n=Rec^(Fin(n+1)), H_n(w)=(R_j(ε(w)))_(0≤j≤n), H_next=H_(n+1), and μ_n=(H_n)_*P. Let readTime(live(T,z))=T and readTime(stopped)=0; a(h)=readTime(h_n), and U(w)=readTime(H_next(w)_(n+1)). Thus U reads the actual next record, rather than being defined as a shifted waiting time. Set W(live(T,z),e)=τ_z(max(e,0)), W(stopped,e)=0 and t(r,e)=real(untopD_0 W(r,e)). Set ρ(live(T,z),s)=ofReal[λ_r(Φ_s z) exp(−Λ_z(max(s,0)))] and ρ(stopped,s)=0. The relative append A_rel(h,s) preserves every old coordinate and appends live(T+max(s,0),S_rΦ_s z) when h_n=live(T,z), and stopped when h_n=stopped. Define A_abs(h,u)=A_rel(h,u−a(h)) and L_abs(h,u)=(A_abs(h,u),u). The raw harmonic flow at negative real time, clipped cumulative increment and stopped time0 are auxiliary totalizations. H_n,H_next,a,U,A_abs,L_abs are Borel; for every abstract (h,u) and every 0≤j≤n, A_abs(h,u)_j=h_j. For any fixed Borel b:Hist_n→[0,∞), finite at every history but not required uniformly bounded, put d(h)=max(b(h)−a(h),0) and D_b(h,u)=1_{a(h)<u<b(h)}ρ(h_n,u−a(h)). Define B_rel={w:0<W(R_n(ε(w)),w_n)<d(H_n(w))} and B={w:H_n(w)_n and H_next(w)_(n+1) are live, a(H_n(w))<U(w)<b(H_n(w))}. Let X(w)=(H_n(w),U(w)), Y(w)=(H_next(w),U(w)), and ν_b=D_b(μ_n⊗du), where du is real Lebesgue measure. D_b is jointly Borel and ∫_ℝD_b(h,u)du≤1 for EVERY abstract history h. B,X,Y are Borel and B_rel=B pointwise. For every w∈B, U(w)=a(H_n(w))+t(R_n(ε(w)),w_n) and H_next(w)=A_abs(X(w)). The exact restricted laws are X_*(P|B)=ν_b, Y_*(P|B)=(L_abs)_*ν_b and (H_next)_*(P|B)=(A_abs)_*ν_b, with ν_b(univ)≤1. For every jointly Borel G:Hist_n×ℝ→[0,∞], the parameter integral h↦∫G(h,u)D_b(h,u)du is Borel and, for every Borel A⊆Hist_n, ∫_{B∩{H_n∈A}}G(X(w))P(dw)=∫_A[∫G(h,u)D_b(h,u)du]μ_n(dh). For every jointly Borel F:Hist_(n+1)×ℝ→[0,∞], the parameter integral h↦∫F(L_abs(h,u))D_b(h,u)du is Borel and ∫_{B∩{H_n∈A}}F(Y(w))P(dw)=∫_A[∫F(L_abs(h,u))D_b(h,u)du]μ_n(dh). No boundedness or integrability of F,G, positive μ_n(A), normalized conditioning, finite wait, no-atom, probability or density provider is assumed. This includes n=0, rank zero, zero hazard, stopped records, live infinite waits, b(h)≤a(h), null A and unrealizable histories; missing mass is not normalized. This is attributed ASTIS completion of one absolute-coordinate ingredient implicit in Appendix A.1(A.7), not a standalone printed theorem. Finite ordered iteration, terminal survival/full path/count assembly, full(A.7), physical-time restart/Markovness, invariance, hypocoercivity, implementation/errors/unbounded query costs/main/composition/wholepaper/Goal remain OPEN.

  • E is a finite-dimensional real inner-product space with its Borel structure, including rank zero.
  • Exactly six source analytic hypotheses: α>0, α≤β, V∈C², α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v, η>0 and βη≤1; α,β≥0.
  • y,xRef,z₀ and deterministic n are universally quantified; the exponential product, clipped thresholds, stopped recursion and observations are literal definitions.
  • b is any fixed Borel finite-valued history function, possibly globally unbounded. F and G are arbitrary jointly Borel extended nonnegative tests; A is any Borel old-history event.
  • Joint measurability, actual clock/append identities, fiber mass and all distribution/integration statements are conclusions. No independence, normalization, no-atom or finite-wait premise is supplied.

Absolute-time law 1

\[a(h)=\operatorname{time}(h_n),\quad U(w)=\operatorname{time}(H_{n+1}(w)_{n+1}),\quad A_{\rm abs}(h,u)=A_{\rm rel}(h,u-a(h)).\]

Absolute-time law 2

\[D_b(h,u)=\mathbf1_{\{a(h)<u<b(h)\}}\rho(h_n,u-a(h)),\quad d(h)=(b(h)-a(h))_+,\quad D_b(h,a(h)+s)=D_d^{\rm rel}(h,s).\]

Absolute-time law 3

\[B=B_{\rm rel},\quad w\in B\Longrightarrow U(w)=a(H_n(w))+t_n(w),\quad H_{n+1}(w)=A_{\rm abs}(H_n(w),U(w)).\]

Absolute-time law 4

\[X_*(P|_B)=\nu_b,\quad Y_*(P|_B)=(L_{\rm abs})_*\nu_b,\quad(H_{n+1})_*(P|_B)=(A_{\rm abs})_*\nu_b,\quad\nu_b=D_b(\mu_n\otimes du).\]

Absolute-time law 5

\[\int_{B\cap\{H_n\in A\}}G(H_n,U)\,dP=\int_A\int_{\mathbb R}G(h,u)D_b(h,u)\,du\,\mu_n(dh).\]

Absolute-time law 6

\[\int_{B\cap\{H_n\in A\}}F(H_{n+1},U)\,dP=\int_A\int_{\mathbb R}F(L_{\rm abs}(h,u))D_b(h,u)\,du\,\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 next absolute-event-time law

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualAbsoluteNextEventTime.actual_absolute_next_event_time_law · theorem · Teaching coverage

Read this first

Mathematical statement

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 define Rec=([0,∞)×(E×E))⊕{stopped}, Hist_n=Rec^(Fin(n+1)), H_n(w)=(R_j(ε(w)))_(0≤j≤n), H_next=H_(n+1), and μ_n=(H_n)_*P. Let readTime(live(T,z))=T and readTime(stopped)=0; a(h)=readTime(h_n), and U(w)=readTime(H_next(w)_(n+1)). Thus U reads the actual next record, rather than being defined as a shifted waiting time. Set W(live(T,z),e)=τ_z(max(e,0)), W(stopped,e)=0 and t(r,e)=real(untopD_0 W(r,e)). Set ρ(live(T,z),s)=ofReal[λ_r(Φ_s z) exp(−Λ_z(max(s,0)))] and ρ(stopped,s)=0. The relative append A_rel(h,s) preserves every old coordinate and appends live(T+max(s,0),S_rΦ_s z) when h_n=live(T,z), and stopped when h_n=stopped. Define A_abs(h,u)=A_rel(h,u−a(h)) and L_abs(h,u)=(A_abs(h,u),u). The raw harmonic flow at negative real time, clipped cumulative increment and stopped time0 are auxiliary totalizations. H_n,H_next,a,U,A_abs,L_abs are Borel; for every abstract (h,u) and every 0≤j≤n, A_abs(h,u)_j=h_j. For any fixed Borel b:Hist_n→[0,∞), finite at every history but not required uniformly bounded, put d(h)=max(b(h)−a(h),0) and D_b(h,u)=1_{a(h)<u<b(h)}ρ(h_n,u−a(h)). Define B_rel={w:0<W(R_n(ε(w)),w_n)<d(H_n(w))} and B={w:H_n(w)_n and H_next(w)_(n+1) are live, a(H_n(w))<U(w)<b(H_n(w))}. Let X(w)=(H_n(w),U(w)), Y(w)=(H_next(w),U(w)), and ν_b=D_b(μ_n⊗du), where du is real Lebesgue measure. D_b is jointly Borel and ∫_ℝD_b(h,u)du≤1 for EVERY abstract history h. B,X,Y are Borel and B_rel=B pointwise. For every w∈B, U(w)=a(H_n(w))+t(R_n(ε(w)),w_n) and H_next(w)=A_abs(X(w)). The exact restricted laws are X_*(P|B)=ν_b, Y_*(P|B)=(L_abs)_*ν_b and (H_next)_*(P|B)=(A_abs)_*ν_b, with ν_b(univ)≤1. For every jointly Borel G:Hist_n×ℝ→[0,∞], the parameter integral h↦∫G(h,u)D_b(h,u)du is Borel and, for every Borel A⊆Hist_n, ∫_{B∩{H_n∈A}}G(X(w))P(dw)=∫_A[∫G(h,u)D_b(h,u)du]μ_n(dh). For every jointly Borel F:Hist_(n+1)×ℝ→[0,∞], the parameter integral h↦∫F(L_abs(h,u))D_b(h,u)du is Borel and ∫_{B∩{H_n∈A}}F(Y(w))P(dw)=∫_A[∫F(L_abs(h,u))D_b(h,u)du]μ_n(dh). No boundedness or integrability of F,G, positive μ_n(A), normalized conditioning, finite wait, no-atom, probability or density provider is assumed. This includes n=0, rank zero, zero hazard, stopped records, live infinite waits, b(h)≤a(h), null A and unrealizable histories; missing mass is not normalized. This is attributed ASTIS completion of one absolute-coordinate ingredient implicit in Appendix A.1(A.7), not a standalone printed theorem. Finite ordered iteration, terminal survival/full path/count assembly, full(A.7), physical-time restart/Markovness, invariance, hypocoercivity, implementation/errors/unbounded query costs/main/composition/wholepaper/Goal remain OPEN.

\[\int_{B\cap\{H_n\in A\}}F(H_{n+1},U)\,dP=\int_A\int_{\mathbb R}F(L_{\rm abs}(h,u))D_b(h,u)\,du\,\mu_n(dh).\]
Lean statement · actual_absolute_next_event_time_law

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 define Rec=([0,∞)×(E×E))⊕{stopped}, Hist_n=Rec^(Fin(n+1)), H_n(w)=(R_j(ε(w)))_(0≤j≤n), H_next=H_(n+1), and μ_n=(H_n)_*P. Let readTime(live(T,z))=T and readTime(stopped)=0; a(h)=readTime(h_n), and U(w)=readTime(H_next(w)_(n+1)). Thus U reads the actual next record, rather than being defined as a shifted waiting time. Set W(live(T,z),e)=τ_z(max(e,0)), W(stopped,e)=0 and t(r,e)=real(untopD_0 W(r,e)). Set ρ(live(T,z),s)=ofReal[λ_r(Φ_s z) exp(−Λ_z(max(s,0)))] and ρ(stopped,s)=0. The relative append A_rel(h,s) preserves every old coordinate and appends live(T+max(s,0),S_rΦ_s z) when h_n=live(T,z), and stopped when h_n=stopped. Define A_abs(h,u)=A_rel(h,u−a(h)) and L_abs(h,u)=(A_abs(h,u),u). The raw harmonic flow at negative real time, clipped cumulative increment and stopped time0 are auxiliary totalizations. H_n,H_next,a,U,A_abs,L_abs are Borel; for every abstract (h,u) and every 0≤j≤n, A_abs(h,u)_j=h_j. For any fixed Borel b:Hist_n→[0,∞), finite at every history but not required uniformly bounded, put d(h)=max(b(h)−a(h),0) and D_b(h,u)=1_{a(h)<u<b(h)}ρ(h_n,u−a(h)). Define B_rel={w:0<W(R_n(ε(w)),w_n)<d(H_n(w))} and B={w:H_n(w)_n and H_next(w)_(n+1) are live, a(H_n(w))<U(w)<b(H_n(w))}. Let X(w)=(H_n(w),U(w)), Y(w)=(H_next(w),U(w)), and ν_b=D_b(μ_n⊗du), where du is real Lebesgue measure. D_b is jointly Borel and ∫_ℝD_b(h,u)du≤1 for EVERY abstract history h. B,X,Y are Borel and B_rel=B pointwise. For every w∈B, U(w)=a(H_n(w))+t(R_n(ε(w)),w_n) and H_next(w)=A_abs(X(w)). The exact restricted laws are X_*(P|B)=ν_b, Y_*(P|B)=(L_abs)_*ν_b and (H_next)_*(P|B)=(A_abs)_*ν_b, with ν_b(univ)≤1. For every jointly Borel G:Hist_n×ℝ→[0,∞], the parameter integral h↦∫G(h,u)D_b(h,u)du is Borel and, for every Borel A⊆Hist_n, ∫_{B∩{H_n∈A}}G(X(w))P(dw)=∫_A[∫G(h,u)D_b(h,u)du]μ_n(dh). For every jointly Borel F:Hist_(n+1)×ℝ→[0,∞], the parameter integral h↦∫F(L_abs(h,u))D_b(h,u)du is Borel and ∫_{B∩{H_n∈A}}F(Y(w))P(dw)=∫_A[∫F(L_abs(h,u))D_b(h,u)du]μ_n(dh). No boundedness or integrability of F,G, positive μ_n(A), normalized conditioning, finite wait, no-atom, probability or density provider is assumed. This includes n=0, rank zero, zero hazard, stopped records, live infinite waits, b(h)≤a(h), null A and unrealizable histories; missing mass is not normalized. This is attributed ASTIS completion of one absolute-coordinate ingredient implicit in Appendix A.1(A.7), not a standalone printed theorem. Finite ordered iteration, terminal survival/full path/count assembly, full(A.7), physical-time restart/Markovness, invariance, hypocoercivity, implementation/errors/unbounded query costs/main/composition/wholepaper/Goal remain OPEN.

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_absolute_next_event_time_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_absolute_next_event_time_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_absolute_next_event_time_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.

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)
private def actual_absolute_next_event_time_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 lastNext : Fin (n + 2) := ⟨n + 1, Nat.lt_succ_self (n + 1)⟩
      let H : (ℕ → ℝ) → Hist := history y xRef z₀ n
      let Hnext : (ℕ → ℝ) → HistNext := history y xRef z₀ (n + 1)
      let readTime : Rec → ℝ := fun r => match r with
        | Sum.inl q => (q.1 : ℝ)
        | Sum.inr _ => 0
      let a : Hist → ℝ := fun h => readTime (h last)
      let U : (ℕ → ℝ) → ℝ := fun w => readTime (Hnext w lastNext)
      let appendRel : Hist × ℝ → HistNext := fun p =>
        Fin.snoc p.1 (match p.1 last with
          | Sum.inl q => Sum.inl (q.1 + Real.toNNReal p.2,
              S xRef (Φ y xRef p.2 q.2))
          | Sum.inr _ => Sum.inr ())
      let appendAbs : Hist × ℝ → HistNext := fun p => appendRel (p.1, p.2 - a p.1)
      let liftAbs : Hist × ℝ → HistNext × ℝ := fun p => (appendAbs p, p.2)
      Measurable H ∧ Measurable Hnext ∧ Measurable a ∧ Measurable U ∧
      Measurable appendAbs ∧ Measurable liftAbs ∧
      (∀ p : Hist × ℝ, ∀ j : Fin (n + 1), appendAbs p j.castSucc = p.1 j) ∧
      (∀ b : Hist → ℝ≥0, Measurable b →
        let d : Hist → ℝ≥0 := fun h => Real.toNNReal ((b h : ℝ) - a h)
        let μ : Measure Hist := Measure.map H P
        let D : Hist → ℝ → ℝ≥0∞ := fun h u =>
          if a h < u ∧ u < (b h : ℝ) then density y xRef (h last, u - a h) else 0
        let Brel : 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 B : Set (ℕ → ℝ) := {w |
          (∃ q, H w last = Sum.inl q) ∧
          (∃ q, Hnext w lastNext = Sum.inl q) ∧
          a (H w) < U w ∧ U w < (b (H w) : ℝ)}
        let X : (ℕ → ℝ) → Hist × ℝ := fun w => (H w, U w)
        let Y : (ℕ → ℝ) → HistNext × ℝ := fun w => (Hnext w, U w)
        let ν : Measure (Hist × ℝ) := (μ.prod (volume : Measure ℝ)).withDensity
          (fun p => D p.1 p.2)
        Measurable (Function.uncurry D) ∧
        (∀ h : Hist, (∫⁻ u : ℝ, D h u) ≤ 1) ∧
        MeasurableSet B ∧ Measurable X ∧ Measurable Y ∧ Brel = B ∧
        (∀ w ∈ B, U w = a (H w) +
          timeObs y xRef (record y xRef z₀ (ε w) n, w n)) ∧
        (∀ w ∈ B, Hnext w = appendAbs (X w)) ∧
        Measure.map X (P.restrict B) = ν ∧
        Measure.map Y (P.restrict B) = Measure.map liftAbs ν ∧
        Measure.map Hnext (P.restrict B) = Measure.map appendAbs ν ∧
        ν Set.univ ≤ 1 ∧
        (∀ G : Hist × ℝ → ℝ≥0∞, Measurable G →
          Measurable (fun h => ∫⁻ u : ℝ, G (h, u) * D h u) ∧
          (∀ A : Set Hist, MeasurableSet A →
            (∫⁻ w in B ∩ H ⁻¹' A, G (X w) ∂P) =
              ∫⁻ h in A, (∫⁻ u : ℝ, G (h, u) * D h u) ∂μ)) ∧
        (∀ F : HistNext × ℝ → ℝ≥0∞, Measurable F →
          Measurable (fun h => ∫⁻ u : ℝ, F (liftAbs (h, u)) * D h u) ∧
          (∀ A : Set Hist, MeasurableSet A →
            (∫⁻ w in B ∩ H ⁻¹' A, F (Y w) ∂P) =
              ∫⁻ h in A, (∫⁻ u : ℝ, F (liftAbs (h, u)) * D h u) ∂μ)))

set_option maxHeartbeats 2400000 in

Exact module and namespace context

Proof roadmap

  1. 1Retain the literal model and actual next record

    Expand the sealed literal clock, reflection, harmonic flow, stopped recursion and complete histories. Reuse the complete-history extension and conditional-density producers with the same six source hypotheses. Define U by reading the next record itself, a by reading the old last record, and absolute append by subtracting a(h) before relative append. No clock identity is assumed.

  2. 2Prove Borel observers and preserve every old coordinate

    The complete next history is Borel by the preceding producer; each old coordinate is its projection. readTime is a Borel sum-elimination, with constant0 on stopped. Composition gives Borel a and U. The Borel map (h,u)↦(h,u−a(h)), followed by the existing relative append, gives Borel absolute append; pairing with u gives its lift. The relative prefix identity preserves all old coordinates for every real u, including auxiliary off-support inputs.

  3. 3Translate the strict density and its fiber mass

    For fixed Borel b, the positive part d=(b−a)₊ is Borel. The strict region a(h)<u<b(h) is Borel, so multiplying the shifted old density by its indicator gives jointly Borel D_b. Elementary real inequalities show a<a+s<b iff 0<s<d; the assertion remains true when b≤a, when both sides are false. Thus D_b(h,a+s)=D_rel(h,s). Lebesgue translation invariance in each fixed history fiber preserves its nonnegative integral, and the verified relative density bound gives ∫D_b≤1 for every history. This is a fiberwise change of variables, with no unproved product-shear certificate.

  4. 4Identify the actual clock and absolute append on exactly the strict event

    Split the actual old record into stopped and live. Stopped remains stopped and has zero wait, so neither strict event occurs. For a live record, an infinite threshold-crossing time produces stopped next record and violates the finite relative upper bound. A finite wait v produces exactly live(T+v,SΦ_v z). Reading that record gives U=T+v; the cutoff equivalence proves B_rel=B pointwise, including v=0. This establishes Borel B and the actual clock equality. Substitute U−a=t in the preceding guarded relative-history identity to obtain H_next=A_abs(X) throughout B.

  5. 5Transfer all old-history and absolute-time tests

    Let π drop the last record from an extended history. It is Borel, π(H_next)=H_n and π(A_rel(h,s))=h. For any jointly Borel G, use G_rel(h_next,s)=G(πh_next,a(πh_next)+s) in the existing complete-history law. The actual clock identity identifies its left integrand with G(H_n,U) on B. In each right fiber, Lebesgue translation converts G(h,a+s)D_rel(h,s) to G(h,u)D_b(h,u). Integrating over any Borel A gives the unnormalized identity, including null A. Borel parameter integration follows from joint nonnegative measurability, without boundedness or integrability assumptions.

  6. 6Recover the weighted joint measure and its actual-history marginals

    Reuse only the probability-normalization component of the canonical exponential-product theorem to obtain probability P and its Borel pushforward μ_n. Apply the preceding test identity at A=univ. Equality against every Borel nonnegative test, Tonelli and the withDensity integral formula yield X_*(P|B)=D_b(μ_n⊗du). On B, Y=L_abs(X) and H_next=A_abs(X), so measurable pushforward composition gives both remaining laws. Their reference measure ν_b has total mass P(B)≤1. Missing mass is never renormalized.

  7. 7Obtain every next-history test and retain the remaining boundary

    For jointly Borel F, apply the old-history test identity to G=F∘L_abs. Its parameter integral is Borel. The pointwise Y=L_abs(X) identity replaces the integrand throughout B∩{H_n∈A}, giving the displayed identity for every Borel A. This proves one strict next absolute-time step; iteration over ordered times, terminal survival, full path/count identification and full A.7 still require separate proofs.

Full assumptions and notation

All objects and hypotheses

  • E is a finite-dimensional real inner-product space with its Borel structure, including rank zero.
  • Exactly six source analytic hypotheses: α>0, α≤β, V∈C², α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v, η>0 and βη≤1; α,β≥0.
  • y,xRef,z₀ and deterministic n are universally quantified; the exponential product, clipped thresholds, stopped recursion and observations are literal definitions.
  • b is any fixed Borel finite-valued history function, possibly globally unbounded. F and G are arbitrary jointly Borel extended nonnegative tests; A is any Borel old-history event.
  • Joint measurability, actual clock/append identities, fiber mass and all distribution/integration statements are conclusions. No independence, normalization, no-atom or finite-wait premise is supplied.

Mathematical proof

1. Retain the literal model and actual next record

Expand the sealed literal clock, reflection, harmonic flow, stopped recursion and complete histories. Reuse the complete-history extension and conditional-density producers with the same six source hypotheses. Define U by reading the next record itself, a by reading the old last record, and absolute append by subtracting a(h) before relative append. No clock identity is assumed.

\[a(h)=\operatorname{time}(h_n),\quad U(w)=\operatorname{time}(H_{n+1}(w)_{n+1}),\quad A_{\rm abs}(h,u)=A_{\rm rel}(h,u-a(h)).\]
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 lastNext : Fin (n + 2) := ⟨n + 1, Nat.lt_succ_self (n + 1)⟩
      let H : (ℕ → ℝ) → Hist := history y xRef z₀ n
      let Hnext : (ℕ → ℝ) → HistNext := history y xRef z₀ (n + 1)
      let readTime : Rec → ℝ := fun r => match r with
        | Sum.inl q => (q.1 : ℝ)
        | Sum.inr _ => 0
      let a : Hist → ℝ := fun h => readTime (h last)
      let U : (ℕ → ℝ) → ℝ := fun w => readTime (Hnext w lastNext)
      let appendRel : Hist × ℝ → HistNext := fun p =>
        Fin.snoc p.1 (match p.1 last with
          | Sum.inl q => Sum.inl (q.1 + Real.toNNReal p.2,
              S xRef (Φ y xRef p.2 q.2))
          | Sum.inr _ => Sum.inr ())
      let appendAbs : Hist × ℝ → HistNext := fun p => appendRel (p.1, p.2 - a p.1)
      let liftAbs : Hist × ℝ → HistNext × ℝ := fun p => (appendAbs p, p.2)
      Measurable H ∧ Measurable Hnext ∧ Measurable a ∧ Measurable U ∧
      Measurable appendAbs ∧ Measurable liftAbs ∧
      (∀ p : Hist × ℝ, ∀ j : Fin (n + 1), appendAbs p j.castSucc = p.1 j) ∧
      (∀ b : Hist → ℝ≥0, Measurable b →
        let d : Hist → ℝ≥0 := fun h => Real.toNNReal ((b h : ℝ) - a h)
        let μ : Measure Hist := Measure.map H P
        let D : Hist → ℝ → ℝ≥0∞ := fun h u =>
          if a h < u ∧ u < (b h : ℝ) then density y xRef (h last, u - a h) else 0
        let Brel : 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 B : Set (ℕ → ℝ) := {w |
          (∃ q, H w last = Sum.inl q) ∧
          (∃ q, Hnext w lastNext = Sum.inl q) ∧
          a (H w) < U w ∧ U w < (b (H w) : ℝ)}
        let X : (ℕ → ℝ) → Hist × ℝ := fun w => (H w, U w)
        let Y : (ℕ → ℝ) → HistNext × ℝ := fun w => (Hnext w, U w)
        let ν : Measure (Hist × ℝ) := (μ.prod (volume : Measure ℝ)).withDensity
          (fun p => D p.1 p.2)
        Measurable (Function.uncurry D) ∧
        (∀ h : Hist, (∫⁻ u : ℝ, D h u) ≤ 1) ∧
        MeasurableSet B ∧ Measurable X ∧ Measurable Y ∧ Brel = B ∧
        (∀ w ∈ B, U w = a (H w) +
          timeObs y xRef (record y xRef z₀ (ε w) n, w n)) ∧
        (∀ w ∈ B, Hnext w = appendAbs (X w)) ∧
        Measure.map X (P.restrict B) = ν ∧
        Measure.map Y (P.restrict B) = Measure.map liftAbs ν ∧
        Measure.map Hnext (P.restrict B) = Measure.map appendAbs ν ∧
        ν Set.univ ≤ 1 ∧
        (∀ G : Hist × ℝ → ℝ≥0∞, Measurable G →
          Measurable (fun h => ∫⁻ u : ℝ, G (h, u) * D h u) ∧
          (∀ A : Set Hist, MeasurableSet A →
            (∫⁻ w in B ∩ H ⁻¹' A, G (X w) ∂P) =
              ∫⁻ h in A, (∫⁻ u : ℝ, G (h, u) * D h u) ∂μ)) ∧
        (∀ F : HistNext × ℝ → ℝ≥0∞, Measurable F →
          Measurable (fun h => ∫⁻ u : ℝ, F (liftAbs (h, u)) * D h u) ∧
          (∀ A : Set Hist, MeasurableSet A →
            (∫⁻ w in B ∩ H ⁻¹' A, F (Y w) ∂P) =
              ∫⁻ h in A, (∫⁻ u : ℝ, F (liftAbs (h, u)) * D h u) ∂μ)))

  have h90 := ActualFiniteHistoryExtension.actual_finite_history_extension
    hα hαβ hV hH hη hβη
  have h89 := ActualConditionalNextWaitDensity.actual_conditional_next_wait_density
    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 lastNext : Fin (n + 2) := ⟨n + 1, Nat.lt_succ_self (n + 1)⟩
  let H : (ℕ → ℝ) → Hist := history y xRef z₀ n
  let Hnext : (ℕ → ℝ) → HistNext := history y xRef z₀ (n + 1)
  let readTime : Rec → ℝ := fun r => match r with
    | Sum.inl q => (q.1 : ℝ)
    | Sum.inr _ => 0
  let a : Hist → ℝ := fun h => readTime (h last)
  let U : (ℕ → ℝ) → ℝ := fun w => readTime (Hnext w lastNext)
  let appendRel : Hist × ℝ → HistNext := fun p =>
    Fin.snoc p.1 (match p.1 last with
      | Sum.inl q => Sum.inl (q.1 + Real.toNNReal p.2,
          S xRef (Φ y xRef p.2 q.2))
      | Sum.inr _ => Sum.inr ())
  let appendAbs : Hist × ℝ → HistNext := fun p => appendRel (p.1, p.2 - a p.1)
  let liftAbs : Hist × ℝ → HistNext × ℝ := fun p => (appendAbs p, p.2)
  change Measurable H ∧ Measurable Hnext ∧ Measurable a ∧ Measurable U ∧
    Measurable appendAbs ∧ Measurable liftAbs ∧
    (∀ p : Hist × ℝ, ∀ j : Fin (n + 1), appendAbs p j.castSucc = p.1 j) ∧ _

Exact contiguous compiled proof region; mathematical dependencies are discharged inside the proof.

2. Prove Borel observers and preserve every old coordinate

The complete next history is Borel by the preceding producer; each old coordinate is its projection. readTime is a Borel sum-elimination, with constant0 on stopped. Composition gives Borel a and U. The Borel map (h,u)↦(h,u−a(h)), followed by the existing relative append, gives Borel absolute append; pairing with u gives its lift. The relative prefix identity preserves all old coordinates for every real u, including auxiliary off-support inputs.

\[H_n,H_{n+1},a,U,A_{\rm abs},L_{\rm abs}\ \text{are Borel};\quad A_{\rm abs}(h,u)_j=h_j\ (j\le n).\]
Corresponding Lean step
  have hnext : Measurable Hnext := (h90 y xRef z₀ n).1
  have hrel : Measurable appendRel := (h90 y xRef z₀ n).2.1
  have hprefix (p : Hist × ℝ) (j : Fin (n + 1)) : appendRel p j.castSucc = p.1 j :=
    (h90 y xRef z₀ n).2.2.2.1 p j
  have hhistory : Measurable H := by
    apply measurable_pi_lambda
    intro j
    exact (measurable_pi_apply j.castSucc).comp hnext
  have hread : Measurable readTime := by
    change Measurable (Sum.elim (fun q : ℝ≥0 × (E × E) => (q.1 : ℝ))
      (fun _ : Unit => (0 : ℝ)))
    exact (measurable_coe_nnreal_real.comp measurable_fst).sumElim measurable_const
  have ha : Measurable a := hread.comp (measurable_pi_apply last)
  have hU : Measurable U := hread.comp ((measurable_pi_apply lastNext).comp hnext)
  have happend : Measurable appendAbs :=
    hrel.comp (measurable_fst.prodMk (measurable_snd.sub (ha.comp measurable_fst)))
  have hlift : Measurable liftAbs := happend.prodMk measurable_snd
  refine ⟨hhistory, hnext, ha, hU, happend, hlift,
    (fun p j => hprefix (p.1, p.2 - a p.1) j), ?_⟩

Exact contiguous compiled proof region; mathematical dependencies are discharged inside the proof.

3. Translate the strict density and its fiber mass

For fixed Borel b, the positive part d=(b−a)₊ is Borel. The strict region a(h)<u<b(h) is Borel, so multiplying the shifted old density by its indicator gives jointly Borel D_b. Elementary real inequalities show a<a+s<b iff 0<s<d; the assertion remains true when b≤a, when both sides are false. Thus D_b(h,a+s)=D_rel(h,s). Lebesgue translation invariance in each fixed history fiber preserves its nonnegative integral, and the verified relative density bound gives ∫D_b≤1 for every history. This is a fiberwise change of variables, with no unproved product-shear certificate.

\[D_b(h,u)=\mathbf1_{\{a(h)<u<b(h)\}}\rho(h_n,u-a(h)),\quad d(h)=(b(h)-a(h))_+,\quad D_b(h,a(h)+s)=D_d^{\rm rel}(h,s).\]
Corresponding Lean step
  intro b hb
  let d : Hist → ℝ≥0 := fun h => Real.toNNReal ((b h : ℝ) - a h)
  let μ : Measure Hist := Measure.map H P
  let D : Hist → ℝ → ℝ≥0∞ := fun h u =>
    if a h < u ∧ u < (b h : ℝ) then density y xRef (h last, u - a h) else 0
  let Brel : 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 B : Set (ℕ → ℝ) := {w |
    (∃ q, H w last = Sum.inl q) ∧
    (∃ q, Hnext w lastNext = Sum.inl q) ∧
    a (H w) < U w ∧ U w < (b (H w) : ℝ)}
  let X : (ℕ → ℝ) → Hist × ℝ := fun w => (H w, U w)
  let Y : (ℕ → ℝ) → HistNext × ℝ := fun w => (Hnext w, U w)
  let ν : Measure (Hist × ℝ) := (μ.prod (volume : Measure ℝ)).withDensity
    (fun p => D p.1 p.2)
  change Measurable (Function.uncurry D) ∧
    (∀ h : Hist, (∫⁻ u : ℝ, D h u) ≤ 1) ∧ _
  have hd : Measurable d := measurable_real_toNNReal.comp
    ((measurable_coe_nnreal_real.comp hb).sub ha)
  have hrho : Measurable (density y xRef) := (h89 y xRef z₀ n).2.1
  have hD : Measurable (Function.uncurry D) := by
    have hguard : MeasurableSet {p : Hist × ℝ |
        a p.1 < p.2 ∧ p.2 < (b p.1 : ℝ)} :=
      (measurableSet_lt (ha.comp measurable_fst) measurable_snd).inter
        (measurableSet_lt measurable_snd
          (measurable_coe_nnreal_real.comp (hb.comp measurable_fst)))
    exact (hrho.comp (((measurable_pi_apply last).comp measurable_fst).prodMk
      (measurable_snd.sub (ha.comp measurable_fst)))).piecewise hguard measurable_const
  let Drel : Hist → ℝ → ℝ≥0∞ := fun h s =>
    if 0 < s ∧ s < (d h : ℝ) then density y xRef (h last, s) else 0
  have h89d := (h89 y xRef z₀ n).2.2.2 d hd
  have hcutoff (h : Hist) (s : ℝ) :
      (a h < a h + s ∧ a h + s < (b h : ℝ)) ↔
        (0 < s ∧ s < (d h : ℝ)) := by
      change (a h < a h + s ∧ a h + s < (b h : ℝ)) ↔
        (0 < s ∧ s < (Real.toNNReal ((b h : ℝ) - a h) : ℝ))
      rw [Real.coe_toNNReal']
      constructor
      · intro hs
        refine ⟨by linarith [hs.1], ?_⟩
        exact lt_of_lt_of_le (by linarith [hs.2]) (le_max_left _ _)
      · intro hs
        refine ⟨by linarith [hs.1], ?_⟩
        rcases lt_max_iff.mp hs.2 with hb' | hzero
        · linarith
        · linarith [hs.1]
  have hshift (h : Hist) (s : ℝ) : D h (a h + s) = Drel h s := by
    simp only [D, Drel, add_sub_cancel_left, hcutoff h s]
  have hrelative_fiber (h : Hist) : (∫⁻ s : ℝ, Drel h s) ≤ 1 := by
    calc
      (∫⁻ s : ℝ, Drel h s) =
          ((volume : Measure ℝ).withDensity (Drel h)) Set.univ := by
        rw [withDensity_apply _ MeasurableSet.univ, setLIntegral_univ]
      _ ≤ 1 := by
        have hbnd := h89d.2.2.2.1 h
        rw [h89d.2.1 h] at hbnd
        exact hbnd
  have hfiber (h : Hist) : (∫⁻ u : ℝ, D h u) ≤ 1 := by
    calc
      (∫⁻ u : ℝ, D h u) = ∫⁻ s : ℝ, D h (a h + s) :=
        ((measurePreserving_add_left (volume : Measure ℝ) (a h)).lintegral_comp
          hD.of_uncurry_left).symm
      _ = ∫⁻ s : ℝ, Drel h s := lintegral_congr (hshift h)
      _ ≤ 1 := hrelative_fiber h

Exact contiguous compiled proof region; mathematical dependencies are discharged inside the proof.

4. Identify the actual clock and absolute append on exactly the strict event

Split the actual old record into stopped and live. Stopped remains stopped and has zero wait, so neither strict event occurs. For a live record, an infinite threshold-crossing time produces stopped next record and violates the finite relative upper bound. A finite wait v produces exactly live(T+v,SΦ_v z). Reading that record gives U=T+v; the cutoff equivalence proves B_rel=B pointwise, including v=0. This establishes Borel B and the actual clock equality. Substitute U−a=t in the preceding guarded relative-history identity to obtain H_next=A_abs(X) throughout B.

\[B=B_{\rm rel},\quad w\in B\Longrightarrow U(w)=a(H_n(w))+t_n(w),\quad H_{n+1}(w)=A_{\rm abs}(H_n(w),U(w)).\]
Corresponding Lean step
  have h90d := (h90 y xRef z₀ n).2.2.2.2 d hd
  have hBrel : MeasurableSet Brel := h90d.1
  have hactualRel (w : ℕ → ℝ) (hw : w ∈ Brel) :
      Hnext w = appendRel (H w, timeObs y xRef (record y xRef z₀ (ε w) n, w n)) :=
    h90d.2.2.1 w hw
  have hguarded (w : ℕ → ℝ) :
      (w ∈ Brel ↔ w ∈ B) ∧
      (w ∈ Brel → U w = a (H w) +
        timeObs y xRef (record y xRef z₀ (ε w) n, w n)) := by
    cases hrec : record y xRef z₀ (ε w) n with
    | inr q =>
      have hold : H w last = Sum.inr q := hrec
      have hnew : Hnext w lastNext = Sum.inr () := by
        change next y xRef (ε w n) (record y xRef z₀ (ε w) n) = _
        simp only [next, hrec]
      simp [Brel, B, waitObs, hrec, hold, hnew]
    | inl q =>
      have hold : H w last = Sum.inl q := hrec
      have htime : a (H w) = (q.1 : ℝ) := by simp only [a, readTime, hold]
      cases ht : τ y xRef q.2 (Real.toNNReal (w n)) using WithTop.recTopCoe with
      | top =>
        have hnew : Hnext w lastNext = Sum.inr () := by
          change next y xRef (ε w n) (record y xRef z₀ (ε w) n) = _
          simp [next, hrec, ε, ht]
        simp [Brel, B, waitObs, hrec, ht, hnew]
        constructor
        · exact not_lt_of_ge le_top
        · intro hw
          exact ((not_lt_of_ge le_top) hw).elim
      | coe v =>
        have hnew : Hnext w lastNext =
            Sum.inl (q.1 + v, S xRef (Φ y xRef (v : ℝ) q.2)) := by
          change next y xRef (ε w n) (record y xRef z₀ (ε w) n) = _
          simp only [next, hrec, ε, ht, WithTop.coe_ne_top, if_false,
            WithTop.untopD_coe]
        have hu : U w = (q.1 : ℝ) + (v : ℝ) := by
          simp only [U, readTime, hnew, NNReal.coe_add]
        have hz : (0 : WithTop ℝ≥0) < (v : WithTop ℝ≥0) ↔ 0 < v := by
          simpa only [WithTop.coe_zero] using
            (WithTop.coe_lt_coe : ((0 : ℝ≥0) : WithTop ℝ≥0) < (v : WithTop ℝ≥0) ↔ 0 < v)
        constructor
        · have hcore : (0 < v ∧ v < d (H w)) ↔
              ((q.1 : ℝ) < (q.1 : ℝ) + (v : ℝ) ∧
                (q.1 : ℝ) + (v : ℝ) < (b (H w) : ℝ)) := by
            simpa only [htime, NNReal.coe_pos, NNReal.coe_lt_coe] using
              (hcutoff (H w) (v : ℝ)).symm
          simp only [Brel, B, Set.mem_ofPred_eq, waitObs, hrec, ht, hz,
            WithTop.coe_lt_coe, hold, hnew, htime, hu]
          constructor
          · intro hv
            exact ⟨⟨q, rfl⟩, ⟨(q.1 + v, S xRef (Φ y xRef (v : ℝ) q.2)), rfl⟩,
              hcore.mp hv⟩
          · intro hw
            exact hcore.mpr hw.2.2
        · intro _
          simp only [hu, htime, timeObs, waitObs, hrec, ht, WithTop.untopD_coe]
  have hBeq : Brel = B := Set.ext (fun w => (hguarded w).1)
  have hB : MeasurableSet B := hBeq ▸ hBrel
  have hX : Measurable X := hhistory.prodMk hU
  have hY : Measurable Y := hnext.prodMk hU
  have hclock (w : ℕ → ℝ) (hw : w ∈ B) : U w = a (H w) +
      timeObs y xRef (record y xRef z₀ (ε w) n, w n) :=
    (hguarded w).2 ((hguarded w).1.mpr hw)
  have hactual (w : ℕ → ℝ) (hw : w ∈ B) : Hnext w = appendAbs (X w) := by
    have htime : U w - a (H w) =
        timeObs y xRef (record y xRef z₀ (ε w) n, w n) := by
      rw [hclock w hw, add_sub_cancel_left]
    change Hnext w = appendRel (H w, U w - a (H w))
    rw [htime]
    exact hactualRel w ((hguarded w).1.mpr hw)

Exact contiguous compiled proof region; mathematical dependencies are discharged inside the proof.

5. Transfer all old-history and absolute-time tests

Let π drop the last record from an extended history. It is Borel, π(H_next)=H_n and π(A_rel(h,s))=h. For any jointly Borel G, use G_rel(h_next,s)=G(πh_next,a(πh_next)+s) in the existing complete-history law. The actual clock identity identifies its left integrand with G(H_n,U) on B. In each right fiber, Lebesgue translation converts G(h,a+s)D_rel(h,s) to G(h,u)D_b(h,u). Integrating over any Borel A gives the unnormalized identity, including null A. Borel parameter integration follows from joint nonnegative measurability, without boundedness or integrability assumptions.

\[\int_{B\cap\{H_n\in A\}}G(H_n,U)\,dP=\int_A\int_{\mathbb R}G(h,u)D_b(h,u)\,du\,\mu_n(dh).\]
Corresponding Lean step
  let oldPrefix : HistNext → Hist := fun h j => h j.castSucc
  have hprefixM : Measurable oldPrefix := by
    apply measurable_pi_lambda
    intro j
    exact measurable_pi_apply j.castSucc
  have hprefixRel (p : Hist × ℝ) : oldPrefix (appendRel p) = p.1 := by
    funext j
    exact hprefix p j
  have hprefixActual (w : ℕ → ℝ) : oldPrefix (Hnext w) = H w := rfl
  have htranslate (G : Hist × ℝ → ℝ≥0∞) (hG : Measurable G) (h : Hist) :
      (∫⁻ s : ℝ, G (h, a h + s) * Drel h s) =
        ∫⁻ u : ℝ, G (h, u) * D h u := by
    calc
      (∫⁻ s : ℝ, G (h, a h + s) * Drel h s) =
          ∫⁻ s : ℝ, G (h, a h + s) * D h (a h + s) :=
        lintegral_congr (fun s => by rw [hshift h s])
      _ = ∫⁻ u : ℝ, G (h, u) * D h u :=
        (measurePreserving_add_left (volume : Measure ℝ) (a h)).lintegral_comp
          ((hG.comp (measurable_const.prodMk measurable_id)).mul hD.of_uncurry_left)
  have hGtests (G : Hist × ℝ → ℝ≥0∞) (hG : Measurable G) :
      Measurable (fun h => ∫⁻ u : ℝ, G (h, u) * D h u) ∧
      (∀ A : Set Hist, MeasurableSet A →
        (∫⁻ w in B ∩ H ⁻¹' A, G (X w) ∂P) =
          ∫⁻ h in A, (∫⁻ u : ℝ, G (h, u) * D h u) ∂μ) := by
    let Grel : HistNext × ℝ → ℝ≥0∞ := fun q =>
      G (oldPrefix q.1, a (oldPrefix q.1) + q.2)
    have hp : Measurable (fun q : HistNext × ℝ => oldPrefix q.1) :=
      hprefixM.comp measurable_fst
    have hGrel : Measurable Grel := hG.comp (hp.prodMk ((ha.comp hp).add measurable_snd))
    have htest := h90d.2.2.2.2.2.2 Grel hGrel
    refine ⟨(hG.mul hD).lintegral_prod_right', ?_⟩
    intro A hA
    have htestA :
        (∫⁻ w in Brel ∩ H ⁻¹' A,
          Grel (Hnext w, timeObs y xRef (record y xRef z₀ (ε w) n, w n)) ∂P) =
          ∫⁻ h in A, (∫⁻ s : ℝ, Grel (appendRel (h, s), s) * Drel h s) ∂μ :=
      htest.2 A hA
    rw [hBeq] at htestA
    calc
      (∫⁻ w in B ∩ H ⁻¹' A, G (X w) ∂P) =
          ∫⁻ w in B ∩ H ⁻¹' A,
            Grel (Hnext w, timeObs y xRef (record y xRef z₀ (ε w) n, w n)) ∂P := by
        apply setLIntegral_congr_fun (hB.inter (hA.preimage hhistory))
        intro w hw
        change G (H w, U w) =
          G (oldPrefix (Hnext w), a (oldPrefix (Hnext w)) +
            timeObs y xRef (record y xRef z₀ (ε w) n, w n))
        rw [hprefixActual, hclock w hw.1]
      _ = ∫⁻ h in A, (∫⁻ s : ℝ, Grel (appendRel (h, s), s) * Drel h s) ∂μ := htestA
      _ = ∫⁻ h in A, (∫⁻ u : ℝ, G (h, u) * D h u) ∂μ := by
        apply setLIntegral_congr_fun hA
        intro h _
        simpa only [Grel, hprefixRel] using htranslate G hG h

Exact contiguous compiled proof region; mathematical dependencies are discharged inside the proof.

6. Recover the weighted joint measure and its actual-history marginals

Reuse only the probability-normalization component of the canonical exponential-product theorem to obtain probability P and its Borel pushforward μ_n. Apply the preceding test identity at A=univ. Equality against every Borel nonnegative test, Tonelli and the withDensity integral formula yield X_*(P|B)=D_b(μ_n⊗du). On B, Y=L_abs(X) and H_next=A_abs(X), so measurable pushforward composition gives both remaining laws. Their reference measure ν_b has total mass P(B)≤1. Missing mass is never renormalized.

\[X_*(P|_B)=\nu_b,\quad Y_*(P|_B)=(L_{\rm abs})_*\nu_b,\quad(H_{n+1})_*(P|_B)=(A_{\rm abs})_*\nu_b,\quad\nu_b=D_b(\mu_n\otimes du).\]
Corresponding Lean step
  -- Reuse the canonical actual input probability; no new normalization premise.
  letI : IsProbabilityMeasure P :=
    AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
  letI : IsProbabilityMeasure μ := Measure.isProbabilityMeasure_map hhistory.aemeasurable
  have hmapX : Measure.map X (P.restrict B) = ν := by
    apply Measure.ext_of_lintegral
    intro G hG
    have huniv := (hGtests G hG).2 Set.univ MeasurableSet.univ
    simp only [Set.preimage_univ, Set.inter_univ, setLIntegral_univ] at huniv
    calc
      (∫⁻ p, G p ∂Measure.map X (P.restrict B)) =
          ∫⁻ w in B, G (X w) ∂P := lintegral_map hG hX
      _ = ∫⁻ h, (∫⁻ u : ℝ, G (h, u) * D h u) ∂μ := huniv
      _ = ∫⁻ p : Hist × ℝ, G p * D p.1 p.2 ∂μ.prod (volume : Measure ℝ) :=
        (lintegral_prod _ (hG.mul hD).aemeasurable).symm
      _ = ∫⁻ p, G p ∂ν := by
        change _ = ∫⁻ p, G p ∂(μ.prod (volume : Measure ℝ)).withDensity (Function.uncurry D)
        exact ((lintegral_withDensity_eq_lintegral_mul _ hD hG).trans
          (lintegral_congr fun p => mul_comm _ _)).symm
  have hYactual (w : ℕ → ℝ) (hw : w ∈ B) : Y w = liftAbs (X w) :=
    Prod.ext (hactual w hw) rfl
  have hmapY : Measure.map Y (P.restrict B) = Measure.map liftAbs ν := by
    rw [← hmapX, Measure.map_map hlift hX]
    exact Measure.map_congr (ae_restrict_of_forall_mem hB hYactual)
  have hmarginal : Measure.map Hnext (P.restrict B) = Measure.map appendAbs ν := by
    rw [← hmapX, Measure.map_map happend hX]
    exact Measure.map_congr (ae_restrict_of_forall_mem hB hactual)
  have hmass : ν Set.univ ≤ 1 := by
    rw [← hmapX, Measure.map_apply hX MeasurableSet.univ, Set.preimage_univ,
      Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
    exact prob_le_one

Exact contiguous compiled proof region; mathematical dependencies are discharged inside the proof.

7. Obtain every next-history test and retain the remaining boundary

For jointly Borel F, apply the old-history test identity to G=F∘L_abs. Its parameter integral is Borel. The pointwise Y=L_abs(X) identity replaces the integrand throughout B∩{H_n∈A}, giving the displayed identity for every Borel A. This proves one strict next absolute-time step; iteration over ordered times, terminal survival, full path/count identification and full A.7 still require separate proofs.

\[\int_{B\cap\{H_n\in A\}}F(H_{n+1},U)\,dP=\int_A\int_{\mathbb R}F(L_{\rm abs}(h,u))D_b(h,u)\,du\,\mu_n(dh).\]
Corresponding Lean step
  refine ⟨hD, hfiber, hB, hX, hY, hBeq, hclock, hactual,
    hmapX, hmapY, hmarginal, hmass, hGtests, ?_⟩
  intro F hF
  have htest := hGtests (F ∘ liftAbs) (hF.comp hlift)
  refine ⟨htest.1, ?_⟩
  intro A hA
  calc
    (∫⁻ w in B ∩ H ⁻¹' A, F (Y w) ∂P) =
        ∫⁻ w in B ∩ H ⁻¹' A, (F ∘ liftAbs) (X w) ∂P := by
      apply setLIntegral_congr_fun (hB.inter (hA.preimage hhistory))
      intro w hw
      exact congrArg F (hYactual w hw.1)
    _ = ∫⁻ h in A, (∫⁻ u : ℝ, F (liftAbs (h, u)) * D h u) ∂μ := htest.2 A hA

Exact contiguous compiled proof region; mathematical dependencies are discharged inside the proof.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · actual_absolute_next_event_time_law

Retain the literal model and actual next record; Prove Borel observers and preserve every old coordinate; Translate the strict density and its fiber mass; Identify the actual clock and absolute append on exactly the strict event; Transfer all old-history and absolute-time tests; Recover the weighted joint measure and its actual-history marginals; Obtain every next-history test and retain the remaining boundary

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_absolute_next_event_time_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_absolute_next_event_time_statement hα hαβ hV hH hη hβη := 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 τ : 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 lastNext : Fin (n + 2) := ⟨n + 1, Nat.lt_succ_self (n + 1)⟩
      let H : (ℕ → ℝ) → Hist := history y xRef z₀ n
      let Hnext : (ℕ → ℝ) → HistNext := history y xRef z₀ (n + 1)
      let readTime : Rec → ℝ := fun r => match r with
        | Sum.inl q => (q.1 : ℝ)
        | Sum.inr _ => 0
      let a : Hist → ℝ := fun h => readTime (h last)
      let U : (ℕ → ℝ) → ℝ := fun w => readTime (Hnext w lastNext)
      let appendRel : Hist × ℝ → HistNext := fun p =>
        Fin.snoc p.1 (match p.1 last with
          | Sum.inl q => Sum.inl (q.1 + Real.toNNReal p.2,
              S xRef (Φ y xRef p.2 q.2))
          | Sum.inr _ => Sum.inr ())
      let appendAbs : Hist × ℝ → HistNext := fun p => appendRel (p.1, p.2 - a p.1)
      let liftAbs : Hist × ℝ → HistNext × ℝ := fun p => (appendAbs p, p.2)
      Measurable H ∧ Measurable Hnext ∧ Measurable a ∧ Measurable U ∧
      Measurable appendAbs ∧ Measurable liftAbs ∧
      (∀ p : Hist × ℝ, ∀ j : Fin (n + 1), appendAbs p j.castSucc = p.1 j) ∧
      (∀ b : Hist → ℝ≥0, Measurable b →
        let d : Hist → ℝ≥0 := fun h => Real.toNNReal ((b h : ℝ) - a h)
        let μ : Measure Hist := Measure.map H P
        let D : Hist → ℝ → ℝ≥0∞ := fun h u =>
          if a h < u ∧ u < (b h : ℝ) then density y xRef (h last, u - a h) else 0
        let Brel : 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 B : Set (ℕ → ℝ) := {w |
          (∃ q, H w last = Sum.inl q) ∧
          (∃ q, Hnext w lastNext = Sum.inl q) ∧
          a (H w) < U w ∧ U w < (b (H w) : ℝ)}
        let X : (ℕ → ℝ) → Hist × ℝ := fun w => (H w, U w)
        let Y : (ℕ → ℝ) → HistNext × ℝ := fun w => (Hnext w, U w)
        let ν : Measure (Hist × ℝ) := (μ.prod (volume : Measure ℝ)).withDensity
          (fun p => D p.1 p.2)
        Measurable (Function.uncurry D) ∧
        (∀ h : Hist, (∫⁻ u : ℝ, D h u) ≤ 1) ∧
        MeasurableSet B ∧ Measurable X ∧ Measurable Y ∧ Brel = B ∧
        (∀ w ∈ B, U w = a (H w) +
          timeObs y xRef (record y xRef z₀ (ε w) n, w n)) ∧
        (∀ w ∈ B, Hnext w = appendAbs (X w)) ∧
        Measure.map X (P.restrict B) = ν ∧
        Measure.map Y (P.restrict B) = Measure.map liftAbs ν ∧
        Measure.map Hnext (P.restrict B) = Measure.map appendAbs ν ∧
        ν Set.univ ≤ 1 ∧
        (∀ G : Hist × ℝ → ℝ≥0∞, Measurable G →
          Measurable (fun h => ∫⁻ u : ℝ, G (h, u) * D h u) ∧
          (∀ A : Set Hist, MeasurableSet A →
            (∫⁻ w in B ∩ H ⁻¹' A, G (X w) ∂P) =
              ∫⁻ h in A, (∫⁻ u : ℝ, G (h, u) * D h u) ∂μ)) ∧
        (∀ F : HistNext × ℝ → ℝ≥0∞, Measurable F →
          Measurable (fun h => ∫⁻ u : ℝ, F (liftAbs (h, u)) * D h u) ∧
          (∀ A : Set Hist, MeasurableSet A →
            (∫⁻ w in B ∩ H ⁻¹' A, F (Y w) ∂P) =
              ∫⁻ h in A, (∫⁻ u : ℝ, F (liftAbs (h, u)) * D h u) ∂μ)))

  have h90 := ActualFiniteHistoryExtension.actual_finite_history_extension
    hα hαβ hV hH hη hβη
  have h89 := ActualConditionalNextWaitDensity.actual_conditional_next_wait_density
    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 lastNext : Fin (n + 2) := ⟨n + 1, Nat.lt_succ_self (n + 1)⟩
  let H : (ℕ → ℝ) → Hist := history y xRef z₀ n
  let Hnext : (ℕ → ℝ) → HistNext := history y xRef z₀ (n + 1)
  let readTime : Rec → ℝ := fun r => match r with
    | Sum.inl q => (q.1 : ℝ)
    | Sum.inr _ => 0
  let a : Hist → ℝ := fun h => readTime (h last)
  let U : (ℕ → ℝ) → ℝ := fun w => readTime (Hnext w lastNext)
  let appendRel : Hist × ℝ → HistNext := fun p =>
    Fin.snoc p.1 (match p.1 last with
      | Sum.inl q => Sum.inl (q.1 + Real.toNNReal p.2,
          S xRef (Φ y xRef p.2 q.2))
      | Sum.inr _ => Sum.inr ())
  let appendAbs : Hist × ℝ → HistNext := fun p => appendRel (p.1, p.2 - a p.1)
  let liftAbs : Hist × ℝ → HistNext × ℝ := fun p => (appendAbs p, p.2)
  change Measurable H ∧ Measurable Hnext ∧ Measurable a ∧ Measurable U ∧
    Measurable appendAbs ∧ Measurable liftAbs ∧
    (∀ p : Hist × ℝ, ∀ j : Fin (n + 1), appendAbs p j.castSucc = p.1 j) ∧ _
  have hnext : Measurable Hnext := (h90 y xRef z₀ n).1
  have hrel : Measurable appendRel := (h90 y xRef z₀ n).2.1
  have hprefix (p : Hist × ℝ) (j : Fin (n + 1)) : appendRel p j.castSucc = p.1 j :=
    (h90 y xRef z₀ n).2.2.2.1 p j
  have hhistory : Measurable H := by
    apply measurable_pi_lambda
    intro j
    exact (measurable_pi_apply j.castSucc).comp hnext
  have hread : Measurable readTime := by
    change Measurable (Sum.elim (fun q : ℝ≥0 × (E × E) => (q.1 : ℝ))
      (fun _ : Unit => (0 : ℝ)))
    exact (measurable_coe_nnreal_real.comp measurable_fst).sumElim measurable_const
  have ha : Measurable a := hread.comp (measurable_pi_apply last)
  have hU : Measurable U := hread.comp ((measurable_pi_apply lastNext).comp hnext)
  have happend : Measurable appendAbs :=
    hrel.comp (measurable_fst.prodMk (measurable_snd.sub (ha.comp measurable_fst)))
  have hlift : Measurable liftAbs := happend.prodMk measurable_snd
  refine ⟨hhistory, hnext, ha, hU, happend, hlift,
    (fun p j => hprefix (p.1, p.2 - a p.1) j), ?_⟩
  intro b hb
  let d : Hist → ℝ≥0 := fun h => Real.toNNReal ((b h : ℝ) - a h)
  let μ : Measure Hist := Measure.map H P
  let D : Hist → ℝ → ℝ≥0∞ := fun h u =>
    if a h < u ∧ u < (b h : ℝ) then density y xRef (h last, u - a h) else 0
  let Brel : 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 B : Set (ℕ → ℝ) := {w |
    (∃ q, H w last = Sum.inl q) ∧
    (∃ q, Hnext w lastNext = Sum.inl q) ∧
    a (H w) < U w ∧ U w < (b (H w) : ℝ)}
  let X : (ℕ → ℝ) → Hist × ℝ := fun w => (H w, U w)
  let Y : (ℕ → ℝ) → HistNext × ℝ := fun w => (Hnext w, U w)
  let ν : Measure (Hist × ℝ) := (μ.prod (volume : Measure ℝ)).withDensity
    (fun p => D p.1 p.2)
  change Measurable (Function.uncurry D) ∧
    (∀ h : Hist, (∫⁻ u : ℝ, D h u) ≤ 1) ∧ _
  have hd : Measurable d := measurable_real_toNNReal.comp
    ((measurable_coe_nnreal_real.comp hb).sub ha)
  have hrho : Measurable (density y xRef) := (h89 y xRef z₀ n).2.1
  have hD : Measurable (Function.uncurry D) := by
    have hguard : MeasurableSet {p : Hist × ℝ |
        a p.1 < p.2 ∧ p.2 < (b p.1 : ℝ)} :=
      (measurableSet_lt (ha.comp measurable_fst) measurable_snd).inter
        (measurableSet_lt measurable_snd
          (measurable_coe_nnreal_real.comp (hb.comp measurable_fst)))
    exact (hrho.comp (((measurable_pi_apply last).comp measurable_fst).prodMk
      (measurable_snd.sub (ha.comp measurable_fst)))).piecewise hguard measurable_const
  let Drel : Hist → ℝ → ℝ≥0∞ := fun h s =>
    if 0 < s ∧ s < (d h : ℝ) then density y xRef (h last, s) else 0
  have h89d := (h89 y xRef z₀ n).2.2.2 d hd
  have hcutoff (h : Hist) (s : ℝ) :
      (a h < a h + s ∧ a h + s < (b h : ℝ)) ↔
        (0 < s ∧ s < (d h : ℝ)) := by
      change (a h < a h + s ∧ a h + s < (b h : ℝ)) ↔
        (0 < s ∧ s < (Real.toNNReal ((b h : ℝ) - a h) : ℝ))
      rw [Real.coe_toNNReal']
      constructor
      · intro hs
        refine ⟨by linarith [hs.1], ?_⟩
        exact lt_of_lt_of_le (by linarith [hs.2]) (le_max_left _ _)
      · intro hs
        refine ⟨by linarith [hs.1], ?_⟩
        rcases lt_max_iff.mp hs.2 with hb' | hzero
        · linarith
        · linarith [hs.1]
  have hshift (h : Hist) (s : ℝ) : D h (a h + s) = Drel h s := by
    simp only [D, Drel, add_sub_cancel_left, hcutoff h s]
  have hrelative_fiber (h : Hist) : (∫⁻ s : ℝ, Drel h s) ≤ 1 := by
    calc
      (∫⁻ s : ℝ, Drel h s) =
          ((volume : Measure ℝ).withDensity (Drel h)) Set.univ := by
        rw [withDensity_apply _ MeasurableSet.univ, setLIntegral_univ]
      _ ≤ 1 := by
        have hbnd := h89d.2.2.2.1 h
        rw [h89d.2.1 h] at hbnd
        exact hbnd
  have hfiber (h : Hist) : (∫⁻ u : ℝ, D h u) ≤ 1 := by
    calc
      (∫⁻ u : ℝ, D h u) = ∫⁻ s : ℝ, D h (a h + s) :=
        ((measurePreserving_add_left (volume : Measure ℝ) (a h)).lintegral_comp
          hD.of_uncurry_left).symm
      _ = ∫⁻ s : ℝ, Drel h s := lintegral_congr (hshift h)
      _ ≤ 1 := hrelative_fiber h
  have h90d := (h90 y xRef z₀ n).2.2.2.2 d hd
  have hBrel : MeasurableSet Brel := h90d.1
  have hactualRel (w : ℕ → ℝ) (hw : w ∈ Brel) :
      Hnext w = appendRel (H w, timeObs y xRef (record y xRef z₀ (ε w) n, w n)) :=
    h90d.2.2.1 w hw
  have hguarded (w : ℕ → ℝ) :
      (w ∈ Brel ↔ w ∈ B) ∧
      (w ∈ Brel → U w = a (H w) +
        timeObs y xRef (record y xRef z₀ (ε w) n, w n)) := by
    cases hrec : record y xRef z₀ (ε w) n with
    | inr q =>
      have hold : H w last = Sum.inr q := hrec
      have hnew : Hnext w lastNext = Sum.inr () := by
        change next y xRef (ε w n) (record y xRef z₀ (ε w) n) = _
        simp only [next, hrec]
      simp [Brel, B, waitObs, hrec, hold, hnew]
    | inl q =>
      have hold : H w last = Sum.inl q := hrec
      have htime : a (H w) = (q.1 : ℝ) := by simp only [a, readTime, hold]
      cases ht : τ y xRef q.2 (Real.toNNReal (w n)) using WithTop.recTopCoe with
      | top =>
        have hnew : Hnext w lastNext = Sum.inr () := by
          change next y xRef (ε w n) (record y xRef z₀ (ε w) n) = _
          simp [next, hrec, ε, ht]
        simp [Brel, B, waitObs, hrec, ht, hnew]
        constructor
        · exact not_lt_of_ge le_top
        · intro hw
          exact ((not_lt_of_ge le_top) hw).elim
      | coe v =>
        have hnew : Hnext w lastNext =
            Sum.inl (q.1 + v, S xRef (Φ y xRef (v : ℝ) q.2)) := by
          change next y xRef (ε w n) (record y xRef z₀ (ε w) n) = _
          simp only [next, hrec, ε, ht, WithTop.coe_ne_top, if_false,
            WithTop.untopD_coe]
        have hu : U w = (q.1 : ℝ) + (v : ℝ) := by
          simp only [U, readTime, hnew, NNReal.coe_add]
        have hz : (0 : WithTop ℝ≥0) < (v : WithTop ℝ≥0) ↔ 0 < v := by
          simpa only [WithTop.coe_zero] using
            (WithTop.coe_lt_coe : ((0 : ℝ≥0) : WithTop ℝ≥0) < (v : WithTop ℝ≥0) ↔ 0 < v)
        constructor
        · have hcore : (0 < v ∧ v < d (H w)) ↔
              ((q.1 : ℝ) < (q.1 : ℝ) + (v : ℝ) ∧
                (q.1 : ℝ) + (v : ℝ) < (b (H w) : ℝ)) := by
            simpa only [htime, NNReal.coe_pos, NNReal.coe_lt_coe] using
              (hcutoff (H w) (v : ℝ)).symm
          simp only [Brel, B, Set.mem_ofPred_eq, waitObs, hrec, ht, hz,
            WithTop.coe_lt_coe, hold, hnew, htime, hu]
          constructor
          · intro hv
            exact ⟨⟨q, rfl⟩, ⟨(q.1 + v, S xRef (Φ y xRef (v : ℝ) q.2)), rfl⟩,
              hcore.mp hv⟩
          · intro hw
            exact hcore.mpr hw.2.2
        · intro _
          simp only [hu, htime, timeObs, waitObs, hrec, ht, WithTop.untopD_coe]
  have hBeq : Brel = B := Set.ext (fun w => (hguarded w).1)
  have hB : MeasurableSet B := hBeq ▸ hBrel
  have hX : Measurable X := hhistory.prodMk hU
  have hY : Measurable Y := hnext.prodMk hU
  have hclock (w : ℕ → ℝ) (hw : w ∈ B) : U w = a (H w) +
      timeObs y xRef (record y xRef z₀ (ε w) n, w n) :=
    (hguarded w).2 ((hguarded w).1.mpr hw)
  have hactual (w : ℕ → ℝ) (hw : w ∈ B) : Hnext w = appendAbs (X w) := by
    have htime : U w - a (H w) =
        timeObs y xRef (record y xRef z₀ (ε w) n, w n) := by
      rw [hclock w hw, add_sub_cancel_left]
    change Hnext w = appendRel (H w, U w - a (H w))
    rw [htime]
    exact hactualRel w ((hguarded w).1.mpr hw)
  let oldPrefix : HistNext → Hist := fun h j => h j.castSucc
  have hprefixM : Measurable oldPrefix := by
    apply measurable_pi_lambda
    intro j
    exact measurable_pi_apply j.castSucc
  have hprefixRel (p : Hist × ℝ) : oldPrefix (appendRel p) = p.1 := by
    funext j
    exact hprefix p j
  have hprefixActual (w : ℕ → ℝ) : oldPrefix (Hnext w) = H w := rfl
  have htranslate (G : Hist × ℝ → ℝ≥0∞) (hG : Measurable G) (h : Hist) :
      (∫⁻ s : ℝ, G (h, a h + s) * Drel h s) =
        ∫⁻ u : ℝ, G (h, u) * D h u := by
    calc
      (∫⁻ s : ℝ, G (h, a h + s) * Drel h s) =
          ∫⁻ s : ℝ, G (h, a h + s) * D h (a h + s) :=
        lintegral_congr (fun s => by rw [hshift h s])
      _ = ∫⁻ u : ℝ, G (h, u) * D h u :=
        (measurePreserving_add_left (volume : Measure ℝ) (a h)).lintegral_comp
          ((hG.comp (measurable_const.prodMk measurable_id)).mul hD.of_uncurry_left)
  have hGtests (G : Hist × ℝ → ℝ≥0∞) (hG : Measurable G) :
      Measurable (fun h => ∫⁻ u : ℝ, G (h, u) * D h u) ∧
      (∀ A : Set Hist, MeasurableSet A →
        (∫⁻ w in B ∩ H ⁻¹' A, G (X w) ∂P) =
          ∫⁻ h in A, (∫⁻ u : ℝ, G (h, u) * D h u) ∂μ) := by
    let Grel : HistNext × ℝ → ℝ≥0∞ := fun q =>
      G (oldPrefix q.1, a (oldPrefix q.1) + q.2)
    have hp : Measurable (fun q : HistNext × ℝ => oldPrefix q.1) :=
      hprefixM.comp measurable_fst
    have hGrel : Measurable Grel := hG.comp (hp.prodMk ((ha.comp hp).add measurable_snd))
    have htest := h90d.2.2.2.2.2.2 Grel hGrel
    refine ⟨(hG.mul hD).lintegral_prod_right', ?_⟩
    intro A hA
    have htestA :
        (∫⁻ w in Brel ∩ H ⁻¹' A,
          Grel (Hnext w, timeObs y xRef (record y xRef z₀ (ε w) n, w n)) ∂P) =
          ∫⁻ h in A, (∫⁻ s : ℝ, Grel (appendRel (h, s), s) * Drel h s) ∂μ :=
      htest.2 A hA
    rw [hBeq] at htestA
    calc
      (∫⁻ w in B ∩ H ⁻¹' A, G (X w) ∂P) =
          ∫⁻ w in B ∩ H ⁻¹' A,
            Grel (Hnext w, timeObs y xRef (record y xRef z₀ (ε w) n, w n)) ∂P := by
        apply setLIntegral_congr_fun (hB.inter (hA.preimage hhistory))
        intro w hw
        change G (H w, U w) =
          G (oldPrefix (Hnext w), a (oldPrefix (Hnext w)) +
            timeObs y xRef (record y xRef z₀ (ε w) n, w n))
        rw [hprefixActual, hclock w hw.1]
      _ = ∫⁻ h in A, (∫⁻ s : ℝ, Grel (appendRel (h, s), s) * Drel h s) ∂μ := htestA
      _ = ∫⁻ h in A, (∫⁻ u : ℝ, G (h, u) * D h u) ∂μ := by
        apply setLIntegral_congr_fun hA
        intro h _
        simpa only [Grel, hprefixRel] using htranslate G hG h
  -- Reuse the canonical actual input probability; no new normalization premise.
  letI : IsProbabilityMeasure P :=
    AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
  letI : IsProbabilityMeasure μ := Measure.isProbabilityMeasure_map hhistory.aemeasurable
  have hmapX : Measure.map X (P.restrict B) = ν := by
    apply Measure.ext_of_lintegral
    intro G hG
    have huniv := (hGtests G hG).2 Set.univ MeasurableSet.univ
    simp only [Set.preimage_univ, Set.inter_univ, setLIntegral_univ] at huniv
    calc
      (∫⁻ p, G p ∂Measure.map X (P.restrict B)) =
          ∫⁻ w in B, G (X w) ∂P := lintegral_map hG hX
      _ = ∫⁻ h, (∫⁻ u : ℝ, G (h, u) * D h u) ∂μ := huniv
      _ = ∫⁻ p : Hist × ℝ, G p * D p.1 p.2 ∂μ.prod (volume : Measure ℝ) :=
        (lintegral_prod _ (hG.mul hD).aemeasurable).symm
      _ = ∫⁻ p, G p ∂ν := by
        change _ = ∫⁻ p, G p ∂(μ.prod (volume : Measure ℝ)).withDensity (Function.uncurry D)
        exact ((lintegral_withDensity_eq_lintegral_mul _ hD hG).trans
          (lintegral_congr fun p => mul_comm _ _)).symm
  have hYactual (w : ℕ → ℝ) (hw : w ∈ B) : Y w = liftAbs (X w) :=
    Prod.ext (hactual w hw) rfl
  have hmapY : Measure.map Y (P.restrict B) = Measure.map liftAbs ν := by
    rw [← hmapX, Measure.map_map hlift hX]
    exact Measure.map_congr (ae_restrict_of_forall_mem hB hYactual)
  have hmarginal : Measure.map Hnext (P.restrict B) = Measure.map appendAbs ν := by
    rw [← hmapX, Measure.map_map happend hX]
    exact Measure.map_congr (ae_restrict_of_forall_mem hB hactual)
  have hmass : ν Set.univ ≤ 1 := by
    rw [← hmapX, Measure.map_apply hX MeasurableSet.univ, Set.preimage_univ,
      Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
    exact prob_le_one
  refine ⟨hD, hfiber, hB, hX, hY, hBeq, hclock, hactual,
    hmapX, hmapY, hmarginal, hmass, hGtests, ?_⟩
  intro F hF
  have htest := hGtests (F ∘ liftAbs) (hF.comp hlift)
  refine ⟨htest.1, ?_⟩
  intro A hA
  calc
    (∫⁻ w in B ∩ H ⁻¹' A, F (Y w) ∂P) =
        ∫⁻ w in B ∩ H ⁻¹' A, (F ∘ liftAbs) (X w) ∂P := by
      apply setLIntegral_congr_fun (hB.inter (hA.preimage hhistory))
      intro w hw
      exact congrArg F (hYactual w hw.1)
    _ = ∫⁻ h in A, (∫⁻ u : ℝ, F (liftAbs (h, u)) * D h u) ∂μ := htest.2 A hA

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualAbsoluteNextEventTime

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Actual source clock recursion and original smoothness/curvature/step assumptions.Literal stopped iid exponential recursion under the same six analytic hypotheses.source-implicitBorel tagged histories, clipped null-set inputs, rank-zero extension and auxiliary totalizations are explicit.
Event times in A.7 are cumulative absolute times.U reads the actual next record; strict relative/absolute guards and U=a+t are proved internally.source-implicitCoordinate equivalence, measurability and translation are dependency conclusions, not public assumptions.
A.7 uses ordered event densities and reflected states.One strict absolute-time joint law and complete-history transport, with all ENNReal joint tests and Borel history cutoffs.source-implicitThis single iteration ingredient preserves null events and missing mass without normalized conditional probabilities.
Full path-functional identity, ordered iteration and final survival.Only the next coordinate is proved; full A7 and downstream restart/main/composition remain open.unresolvedNo full ordered-time integral, path/count partition or terminal survival assembly is asserted.

Exactly six original analytic hypotheses and literal iid Exp(1) stopped recursion. Fixed y,xRef,z0 and deterministic event depth n; arbitrary fixed Borel finite-valued absolute horizon b may be unbounded across histories. U reads the actual next record. Strict live event a(Hn)<U<b(Hn) equals the positive relative-cap event. Borel absolute density, every-history fiber mass<=1, guarded actual clock/whole-history append, exact actual restricted joint/marginal laws and all joint ENNReal tests on every old-history event (including null ones) are derived internally. Stopped time0, raw negative flow and T+max(u-T,0) off-support append are auxiliary only. No normalization, integrability, finite-wait, no-atom, survival or coordinate/provider premise. Existing actual-input a.s. nonaccumulation78 and half-open coverage79 are retained and not reproved. Only one coordinate edge within S87-I5/G86-11 is targeted. Finite ordered iteration, final88 survival/hazard assembly, endpoint resolution when used, actual count/prescribed path identification, A7 summability/fullA7, physical-time residual restart/Markov, invariance/semigroup/L2/hypocoercivity, implementation/errors/unbounded costs/main/composition/full papers/Goal remain OPEN.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • objects: Absorbing stopped tag, time-zero observers, clipped raw thresholds and globally total append define explicit auxiliary semantics. They agree with source live finite recursion; B excludes stopped and nonpositive/infinite waits. The theorem never equates source infinite absolute time with its zero observer. — Independent source-only freeze, fresh canonical packet, complete blind reconstruction, full production statement/proof, exact lesson/publication, 27 source dispositions/9 byte spans and seven BODY regions compared. No blocking source mismatch or excess premise found. Compiler/fake-scan logs are supporting Lean evidence, not source-equivalence evidence.
  • domains: Coordinate-free finite-dimensional real inner-product carrier, including rank zero, and ENNReal joint tests are explicit elaborations/extensions. They introduce no extra analytic assumptions and do not replace the full-path target. — Independent source-only freeze, fresh canonical packet, complete blind reconstruction, full production statement/proof, exact lesson/publication, 27 source dispositions/9 byte spans and seven BODY regions compared. No blocking source mismatch or excess premise found. Compiler/fake-scan logs are supporting Lean evidence, not source-equivalence evidence.
  • quantifiers: History-dependent Borel finite cutoffs and unnormalized history-event integrals expose the source iteration ingredient; the fixed-horizon case is a specialization. Neither positive conditioning probability nor random physical-time restart is asserted. — Independent source-only freeze, fresh canonical packet, complete blind reconstruction, full production statement/proof, exact lesson/publication, 27 source dispositions/9 byte spans and seven BODY regions compared. No blocking source mismatch or excess premise found. Compiler/fake-scan logs are supporting Lean evidence, not source-equivalence evidence.
  • scopes: The infinite-wait/no-event atom and terminal survival are outside the strict restricted law; no mass is renormalized. Ordered iteration, final factor/path/count identification and full A.7 remain open. Existing actual-input nonaccumulation78/half-open coverage79 are upstream retained facts, not reopened or re-proved here. — Independent source-only freeze, fresh canonical packet, complete blind reconstruction, full production statement/proof, exact lesson/publication, 27 source dispositions/9 byte spans and seven BODY regions compared. No blocking source mismatch or excess premise found. Compiler/fake-scan logs are supporting Lean evidence, not source-equivalence evidence.
  • scopes: Planned S91-T text includes a broader unweighted shear/inverse preservation theorem. This implementation realizes exactly the needed weighted coordinate law via fixed-history translation plus Tonelli; it does not separately close that broader theorem. Current lesson and proposed implementation mapping state this accurately. — Independent source-only freeze, fresh canonical packet, complete blind reconstruction, full production statement/proof, exact lesson/publication, 27 source dispositions/9 byte spans and seven BODY regions compared. No blocking source mismatch or excess premise found. Compiler/fake-scan logs are supporting Lean evidence, not source-equivalence evidence.

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries
  • Exactly six original analytic hypotheses and literal iid Exp(1) stopped recursion. Fixed y,xRef,z0 and deterministic event depth n; arbitrary fixed Borel finite-valued absolute horizon b may be unbounded across histories. U reads the actual next record. Strict live event a(Hn)<U<b(Hn) equals the positive relative-cap event. Borel absolute density, every-history fiber mass≤1, guarded actual clock/whole-history append, exact actual restricted joint/marginal laws and all joint ENNReal tests on every old-history event (including null ones) are derived internally. Stopped time0, raw negative flow and T+max(u-T,0) off-support append are auxiliary only. No normalization, integrability, finite-wait, no-atom, survival or coordinate/provider premise. Existing actual-input a.s. nonaccumulation78 and half-open coverage79 are retained and not reproved. Only one coordinate edge within S87-I5/G86-11 is targeted. Finite ordered iteration, final88 survival/hazard assembly, endpoint resolution when used, actual count/prescribed path identification, A7 summability/fullA7, physical-time residual restart/Markov, invariance/semigroup/L2/hypocoercivity, implementation/errors/unbounded costs/main/composition/full papers/Goal remain OPEN.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • measurePreserving_add_left
  • MeasurePreserving.lintegral_comp
  • Measure.ext_of_lintegral
  • lintegral_prod
  • lintegral_withDensity_eq_lintegral_mul
  • Measurable.lintegral_prod_right'
  • Measure.map_map
  • Measure.map_congr
  • setLIntegral_congr_fun

Mathematical sources

  • Chen-Chewi-Lu-Zhang arXiv2609.06905v1 Appendix A.1 (A.1),(A.2), one absolute-time coordinate ingredient of (A.7), and Appendix A.2; attributed ASTIS source-implicit completion. — Exactly six original analytic hypotheses and literal iid Exp(1) stopped recursion. Fixed y,xRef,z0 and deterministic event depth n; arbitrary fixed Borel finite-valued absolute horizon b may be unbounded across histories. U reads the actual next record. Strict live event a(Hn)<U<b(Hn) equals the positive relative-cap event. Borel absolute density, every-history fiber mass<=1, guarded actual clock/whole-history append, exact actual restricted joint/marginal laws and all joint ENNReal tests on every old-history event (including null ones) are derived internally. Stopped time0, raw negative flow and T+max(u-T,0) off-support append are auxiliary only. No normalization, integrability, finite-wait, no-atom, survival or coordinate/provider premise. Existing actual-input a.s. nonaccumulation78 and half-open coverage79 are retained and not reproved. Only one coordinate edge within S87-I5/G86-11 is targeted. Finite ordered iteration, final88 survival/hazard assembly, endpoint resolution when used, actual count/prescribed path identification, A7 summability/fullA7, physical-time residual restart/Markov, invariance/semigroup/L2/hypocoercivity, implementation/errors/unbounded costs/main/composition/full papers/Goal remain OPEN.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Which proof obligations and prerequisites are covered?

  • Formalized proof edge; source adapter/review separate Actual strict next absolute-event-time law
  • TODO — not closed by these contributions Ordered iteration, terminal survival and full path/count identity A7