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

Actual PBPS finite endpoint and event-time reversal

Chen, Chewi, Lu and Zhang, arXiv:2609.06905v1, Appendix A.1, endpoint/time substitution surrounding (A.8). Complete attributed ASTIS mathematical restatement with explicit finite-word, Borel, simplex-comap and product-volume completion; not verbatim source text and not the full weighted stationary identity.

arXiv2609.06905v1 · Chen-Chewi-Lu-Zhang arXiv2609.06905v1 Appendix A.1 A8 actual prescribed endpoint/time reversal and product-volume change of variables. · faithful paraphrase

Complete source statement (Samplinglib restatement)

Let E be a finite-dimensional real inner-product space with its Borel sigma algebra, including dimension zero. Let V:E->R, alpha,beta>=0 and eta in R. Assume alpha>0, alpha<=beta, V is C2, alpha||v||^2<=D2V(x)[v,v]<=beta||v||^2 for every x,v in E, eta>0 and beta*eta<=1. For y,r in E put c=y-eta grad V(r), h_r(x)=grad V(x)-grad V(r), R(x,p)=(x,-p), Phi_(y,r,u)(x,p)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p), S_r(x,p)=(x,p-(2<p,h_r(x)>/||h_r(x)||^2)h_r(x)). Real division by zero is zero, so a zero normal gives the identity bounce. Let ell=volume_E tensor volume_E, with canonical Hilbert-space Lebesgue measure. For every integer n>=0 and horizon T>=0, let Delta_n(T) consist of real tuples 0<t_0<...<t_(n-1)<T. Equivalently, prepending 0 produces a strictly increasing tuple and every entry is less than T. Let Prefix_n(T) be this subtype and m_n,T the comap of Lebesgue measure on R^n under its inclusion. This is unnormalized simplex volume. For n=0 the tuple is empty and its zero-dimensional volume is one; for T=0 and n>0 the subtype is empty. Write q_0=0 and q_(j+1)=t_j. Starting at z_0=z, define z_(j+1)=S_r(Phi_(y,r,t_j-q_j)(z_j)) for 0<=j<n. Define records K_j=(q_j,z_j), each embedded in the live branch of (R_nonnegative x (E x E)) plus a cemetery symbol. For a general history of n+1 such records, the path reconstruction Psi at s in [0,T] starts from z and visits records in increasing index order: a live record (a,w) replaces the accumulator by Phi_(y,r,s-a)(w) exactly when a<=s; future records and cemetery records leave it unchanged. Here s-a is nonnegative subtraction. Define Gamma_(y,r,z,t)=Psi(K), the actual finite prescribed path; thus its value at an event is the post-bounce value. Let A_(y,r)(z,t)=Gamma_(y,r,z,t)(T). There exists rho:Prefix_n(T)->Prefix_n(T) with (rho t)_i=T-t_(n-1-i) for every i. It is Borel measurable, involutive, and preserves m_n,T. For all y,r,z,t, the terminal identity is A_(y,r)(z,t)=Phi_(y,r,T-q_n)(z_n). The map (y,r,z,t)->A_(y,r)(z,t) is jointly Borel measurable. For each y,r,t, z->A_(y,r)(z,t) preserves ell. The reversed endpoint satisfies A_(y,r)(R(A_(y,r)(z,t)),rho t)=R(z). Define Theta_(y,r)(z,t)=(R(A_(y,r)(z,t)),rho t). The map (y,r,z,t)->Theta_(y,r)(z,t) is jointly Borel measurable. For each y,r, Theta_(y,r) is an involution and preserves ell tensor m_n,T, in phase-first order. Every measure-preservation assertion includes measurability and equality of pushforward measures. All conclusions include n=0, T=0, zero reflection normals and rank-zero E; measurability, inverses, sigma finiteness and volume identities are proved internally from the six analytic assumptions. This is the finite prescribed endpoint/time change of variables used in the Appendix A.1 reversal argument. It does not assert pointwise time reversal of right-continuous paths at event times. Gibbs-weight balance, stationary averaging and invariant probability laws, Markov properties, hypocoercivity, implementation error, expected oracle costs, main sampling results and actual-input composition remain separate obligations.

  • Finite-dimensional real inner-product Borel E, including rank zero.
  • alpha,beta>=0; alpha>0; alpha<=beta; V is C2; alpha||v||^2<=D2V(x)[v,v]<=beta||v||^2 for all x,v; eta>0; beta*eta<=1.
  • All n>=0, T>=0, y,r,z and strictly ordered event tuples; zero events and zero normals are included.
  • The exact unnormalized simplex comap m and phase-first product ell tensor m are fixed definitions. Measurability, sigma finiteness, inverses and volume preservation are proved dependencies or conclusions.

Endpoint inverse

\[A_{\rho t}(R A_t(z))=Rz,\qquad (A_t)_\#\ell=\ell.\]

Joint change of variables

\[\Theta^2=\mathrm{id},\qquad \Theta_\#(\ell\otimes m_{n,T})=\ell\otimes m_{n,T}.\]

Read the formalized proofs

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

Samplinglib mathematical lesson

Actual PBPS finite endpoint and event-time reversal

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualEndpointTimeReversal.actual_endpoint_time_reversal_laws · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product space with its Borel sigma algebra, including dimension zero. Let V:E→R, alpha,beta≥0 and eta in R. Assume alpha>0, alpha≤beta, V is C2, alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for every x,v in E, eta>0 and beta*eta≤1. For y,r in E put c=y-eta grad V(r), h_r(x)=grad V(x)-grad V(r), R(x,p)=(x,-p), Phi_(y,r,u)(x,p)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p), S_r(x,p)=(x,p-(2<p,h_r(x)>/||h_r(x)||^2)h_r(x)). Real division by zero is zero, so a zero normal gives the identity bounce. Let ell=volume_E tensor volume_E, with canonical Hilbert-space Lebesgue measure. For every integer n≥0 and horizon T≥0, let Delta_n(T) consist of real tuples 0<t_0<...<t_(n-1)<T. Equivalently, prepending 0 produces a strictly increasing tuple and every entry is less than T. Let Prefix_n(T) be this subtype and m_n,T the comap of Lebesgue measure on R^n under its inclusion. This is unnormalized simplex volume. For n=0 the tuple is empty and its zero-dimensional volume is one; for T=0 and n>0 the subtype is empty. Write q_0=0 and q_(j+1)=t_j. Starting at z_0=z, define z_(j+1)=S_r(Phi_(y,r,t_j-q_j)(z_j)) for 0≤j<n. Define records K_j=(q_j,z_j), each embedded in the live branch of (R_nonnegative x (E x E)) plus a cemetery symbol. For a general history of n+1 such records, the path reconstruction Psi at s in [0,T] starts from z and visits records in increasing index order: a live record (a,w) replaces the accumulator by Phi_(y,r,s-a)(w) exactly when a≤s; future records and cemetery records leave it unchanged. Here s-a is nonnegative subtraction. Define Gamma_(y,r,z,t)=Psi(K), the actual finite prescribed path; thus its value at an event is the post-bounce value. Let A_(y,r)(z,t)=Gamma_(y,r,z,t)(T). There exists rho:Prefix_n(T)→Prefix_n(T) with (rho t)_i=T-t_(n-1-i) for every i. It is Borel measurable, involutive, and preserves m_n,T. For all y,r,z,t, the terminal identity is A_(y,r)(z,t)=Phi_(y,r,T-q_n)(z_n). The map (y,r,z,t)→A_(y,r)(z,t) is jointly Borel measurable. For each y,r,t, z→A_(y,r)(z,t) preserves ell. The reversed endpoint satisfies A_(y,r)(R(A_(y,r)(z,t)),rho t)=R(z). Define Theta_(y,r)(z,t)=(R(A_(y,r)(z,t)),rho t). The map (y,r,z,t)→Theta_(y,r)(z,t) is jointly Borel measurable. For each y,r, Theta_(y,r) is an involution and preserves ell tensor m_n,T, in phase-first order. Every measure-preservation assertion includes measurability and equality of pushforward measures. All conclusions include n=0, T=0, zero reflection normals and rank-zero E; measurability, inverses, sigma finiteness and volume identities are proved internally from the six analytic assumptions. This is the finite prescribed endpoint/time change of variables used in the Appendix A.1 reversal argument. It does not assert pointwise time reversal of right-continuous paths at event times. Gibbs-weight balance, stationary averaging and invariant probability laws, Markov properties, hypocoercivity, implementation error, expected oracle costs, main sampling results and actual-input composition remain separate obligations.

\[\Theta^2=\mathrm{id},\qquad \Theta_\#(\ell\otimes m_{n,T})=\ell\otimes m_{n,T}.\]
Lean statement · actual_endpoint_time_reversal_laws

Let E be a finite-dimensional real inner-product space with its Borel sigma algebra, including dimension zero. Let V:E->R, alpha,beta>=0 and eta in R. Assume alpha>0, alpha<=beta, V is C2, alpha||v||^2<=D2V(x)[v,v]<=beta||v||^2 for every x,v in E, eta>0 and beta*eta<=1. For y,r in E put c=y-eta grad V(r), h_r(x)=grad V(x)-grad V(r), R(x,p)=(x,-p), Phi_(y,r,u)(x,p)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p), S_r(x,p)=(x,p-(2<p,h_r(x)>/||h_r(x)||^2)h_r(x)). Real division by zero is zero, so a zero normal gives the identity bounce. Let ell=volume_E tensor volume_E, with canonical Hilbert-space Lebesgue measure. For every integer n>=0 and horizon T>=0, let Delta_n(T) consist of real tuples 0<t_0<...<t_(n-1)<T. Equivalently, prepending 0 produces a strictly increasing tuple and every entry is less than T. Let Prefix_n(T) be this subtype and m_n,T the comap of Lebesgue measure on R^n under its inclusion. This is unnormalized simplex volume. For n=0 the tuple is empty and its zero-dimensional volume is one; for T=0 and n>0 the subtype is empty. Write q_0=0 and q_(j+1)=t_j. Starting at z_0=z, define z_(j+1)=S_r(Phi_(y,r,t_j-q_j)(z_j)) for 0<=j<n. Define records K_j=(q_j,z_j), each embedded in the live branch of (R_nonnegative x (E x E)) plus a cemetery symbol. For a general history of n+1 such records, the path reconstruction Psi at s in [0,T] starts from z and visits records in increasing index order: a live record (a,w) replaces the accumulator by Phi_(y,r,s-a)(w) exactly when a<=s; future records and cemetery records leave it unchanged. Here s-a is nonnegative subtraction. Define Gamma_(y,r,z,t)=Psi(K), the actual finite prescribed path; thus its value at an event is the post-bounce value. Let A_(y,r)(z,t)=Gamma_(y,r,z,t)(T). There exists rho:Prefix_n(T)->Prefix_n(T) with (rho t)_i=T-t_(n-1-i) for every i. It is Borel measurable, involutive, and preserves m_n,T. For all y,r,z,t, the terminal identity is A_(y,r)(z,t)=Phi_(y,r,T-q_n)(z_n). The map (y,r,z,t)->A_(y,r)(z,t) is jointly Borel measurable. For each y,r,t, z->A_(y,r)(z,t) preserves ell. The reversed endpoint satisfies A_(y,r)(R(A_(y,r)(z,t)),rho t)=R(z). Define Theta_(y,r)(z,t)=(R(A_(y,r)(z,t)),rho t). The map (y,r,z,t)->Theta_(y,r)(z,t) is jointly Borel measurable. For each y,r, Theta_(y,r) is an involution and preserves ell tensor m_n,T, in phase-first order. Every measure-preservation assertion includes measurability and equality of pushforward measures. All conclusions include n=0, T=0, zero reflection normals and rank-zero E; measurability, inverses, sigma finiteness and volume identities are proved internally from the six analytic assumptions. This is the finite prescribed endpoint/time change of variables used in the Appendix A.1 reversal argument. It does not assert pointwise time reversal of right-continuous paths at event times. Gibbs-weight balance, stationary averaging and invariant probability laws, Markov properties, hypocoercivity, implementation error, expected oracle costs, main sampling results and actual-input composition remain separate obligations.

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_endpoint_time_reversal_laws
    {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_endpoint_time_reversal_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_endpoint_time_reversal_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_endpoint_time_reversal_statement
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ) * ‖v‖ ^ 2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) : Prop := by
  classical
  exact
    let c : E → E → E := fun y xRef => y - η • gradient V xRef
    let Φ : E → E → ℝ → (E × E) → (E × E) := fun y xRef t z =>
      (c y xRef + Real.cos t • (z.1 - c y xRef) +
          (Real.sqrt η * Real.sin t) • z.2,
       (-Real.sin t / Real.sqrt η) • (z.1 - c y xRef) + Real.cos t • z.2)
    let S : E → (E × E) → (E × E) := fun xRef z =>
      (z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
        ‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
    let Rec := (ℝ≥0 × (E × E)) ⊕ Unit
    let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
    let Δ : (n : ℕ) → ℝ≥0 → Set (Fin n → ℝ) := fun n T =>
      {t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < (T : ℝ)}
    let Prefix : (n : ℕ) → ℝ≥0 → Type := fun n T => {t : Fin n → ℝ // t ∈ Δ n T}
    let m : (n : ℕ) → (T : ℝ≥0) → Measure (Prefix n T) := fun n T =>
      Measure.comap (fun t : Prefix n T => t.val) (volume : Measure (Fin n → ℝ))
    let zAt : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Fin (n + 1) → (E × E) := fun y xRef z₀ n T t =>
      Fin.induction z₀ (fun i z =>
        S xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc) z))
    let K : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Hist n := fun y xRef z₀ n T t j =>
      Sum.inl (Real.toNNReal ((Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) j), zAt y xRef z₀ n T t j)
    let Path : ℝ≥0 → Type _ := fun T => {s : ℝ≥0 // s ≤ T} → E × E
    let Ψ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Hist n → Path T :=
      fun y xRef z₀ n T h s =>
        Fin.foldl (n + 1) (fun z j => (h j).elim
          (fun a => if a.1 ≤ s.val then Φ y xRef ((s.val - a.1 : ℝ≥0) : ℝ) a.2 else z)
          (fun _ => z)) z₀
    let Γ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → Path T :=
      fun y xRef z₀ n T t => Ψ y xRef z₀ n T (K y xRef z₀ n T t)
    let R : (E × E) → (E × E) := fun z => (z.1, -z.2)
    let ell : Measure (E × E) := (volume : Measure E).prod (volume : Measure E)
    ∀ n : ℕ, ∀ T : ℝ≥0, ∃ rho : Prefix n T → Prefix n T,
      (∀ t : Prefix n T, ∀ i : Fin n, (rho t).val i = (T : ℝ) - t.val i.rev) ∧
      Measurable rho ∧ Function.Involutive rho ∧ MeasurePreserving rho (m n T) (m n T) ∧
      let A : E → E → (E × E) → Prefix n T → (E × E) :=
        fun y r z t => Γ y r z n T t ⟨T, le_rfl⟩
      let Theta : E → E → ((E × E) × Prefix n T) → ((E × E) × Prefix n T) :=
        fun y r q => (R (A y r q.1 q.2), rho q.2)
      (∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
        A y r z t = Φ y r ((T : ℝ) -
          (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) (Fin.last n))
          (zAt y r z n T t (Fin.last n))) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        A p.1.1.1 p.1.1.2 p.1.2 p.2) ∧
      (∀ y r : E, ∀ t : Prefix n T,
        MeasurePreserving (fun z => A y r z t) ell ell) ∧
      (∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
        A y r (R (A y r z t)) (rho t) = R z) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        Theta p.1.1.1 p.1.1.2 (p.1.2, p.2)) ∧
      (∀ y r : E, Function.Involutive (Theta y r)) ∧
      (∀ y r : E, MeasurePreserving (Theta y r) (ell.prod (m n T)) (ell.prod (m n T)))

Exact module and namespace context

Proof roadmap

  1. 1Reverse the ordered time simplex

    Set rho(t)_i=T-t_(n-1-i). Reversal reverses index order and subtraction reverses inequalities, so strict ordering is preserved. The original upper bound gives positivity, and the original positivity gives the new upper bound T. Applying the formula twice restores every coordinate. On R^n this map is a coordinate permutation composed with coordinatewise reflection and translation, each preserving Lebesgue measure. Its invariant measurable simplex therefore inherits preservation of the exact comap measure m. This includes the unique empty tuple.

  2. 2Cancel a finite reversed sequence

    For updates f_i and a map C satisfying f_i(C(f_i(x)))=C(x), process f_0 through f_(n-1), then apply C and process the updates in reverse order. Induction removes the outer matching pair and leaves C(x). A second finite induction identifies a fold with a prescribed sequence whenever its initial value and one-step recurrences agree. These algebraic statements will be applied to the actual flow and bounce.

  3. 3Express the endpoint as a finite word of gaps

    Append T and prepend 0 to define gaps g_0=t_0, g_j=t_j-t_(j-1), g_n=T-t_(n-1). Reversing the tuple reverses the n+1 gaps exactly. The recursive post-bounce states give the terminal map Phi_(g_n) S Phi_(g_(n-1)) ... S Phi_(g_0). Equivalently start from S(z) and fold f_i=Phi_(g_i) composed with S through i=0,...,n. The first pair of bounces cancels because S is involutive. For n=0 this is just Phi_T(z).

  4. 4Derive the inverse endpoint and its fiber volume

    Take C=S composed with R. The identities S^2=R^2=id, RS=SR and R Phi_u R=Phi_(-u), together with the inverse-flow law, imply f_i C f_i=C. Apply reversed-word cancellation and use the reversed-gap identity. The result is A_(rho t)(R A_t(z))=R(z). Separately, finite induction shows a composition of volume-preserving updates preserves volume; since S and each Phi_u preserve ell, so does A_t.

  5. 5Connect the finite word to the actual path at T

    The verified ordered-prefix theorem supplies measurability of Delta. The verified finite-count path theorem supplies joint measurability of Gamma and its last-interval formula. Evaluating the measurable function-valued path at T preserves measurability. For n>0 the last event is strictly before T; for n=0 its grid point is zero and T≥0. There is no later record than the final index. Thus the interval formula yields Gamma(T)=Phi_(T-q_n)(z_n), exactly the finite word above. This connection uses the actual live/cemetery history and the original six analytic assumptions.

  6. 6Assemble the jointly measurable preserving involution

    Reuse the actual phase-volume theorem for every flow, bounce and reversal identity; no such identity is an extra public premise. The terminal-data connection gives the measurable endpoint A and its fiber-volume and reversal laws. Hence Theta(z,t)=(R A_t(z),rho t) is jointly measurable and Theta^2(z,t)=(R R z,rho^2 t)=(z,t). The simplex inclusion pushes m to restricted ambient Lebesgue measure, establishing sigma finiteness. In time-first order, apply the measurable skew-product theorem to rho and the ell-preserving fibers z→R A_t(z); swap coordinates before and after to obtain preservation of ell tensor m in the stated phase-first order. This finishes the endpoint change of variables; weighting by Gibbs densities is a later edge.

Full assumptions and notation

All objects and hypotheses

  • Finite-dimensional real inner-product Borel E, including rank zero.
  • alpha,beta≥0; alpha>0; alpha≤beta; V is C2; alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for all x,v; eta>0; beta*eta≤1.
  • All n≥0, T≥0, y,r,z and strictly ordered event tuples; zero events and zero normals are included.
  • The exact unnormalized simplex comap m and phase-first product ell tensor m are fixed definitions. Measurability, sigma finiteness, inverses and volume preservation are proved dependencies or conclusions.

Mathematical proof

1. Reverse the ordered time simplex

Set rho(t)_i=T-t_(n-1-i). Reversal reverses index order and subtraction reverses inequalities, so strict ordering is preserved. The original upper bound gives positivity, and the original positivity gives the new upper bound T. Applying the formula twice restores every coordinate. On R^n this map is a coordinate permutation composed with coordinatewise reflection and translation, each preserving Lebesgue measure. Its invariant measurable simplex therefore inherits preservation of the exact comap measure m. This includes the unique empty tuple.

\[\rho(t)_i=T-t_{n-1-i},\quad \rho^2=\mathrm{id},\quad \rho_\#m_{n,T}=m_{n,T}.\]
Corresponding Lean step
private def delta (n : ℕ) (T : ℝ) : Set (Fin n → ℝ) :=
  {t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < T}
private def reverseTime {n : ℕ} (T : ℝ) (t : Fin n → ℝ) : Fin n → ℝ :=
  fun i => T - t i.rev

private theorem reverseTime_involutive (n : ℕ) (T : ℝ) :
    Function.Involutive (reverseTime (n := n) T) := by
  intro t; funext i
  simp [reverseTime]

private theorem reverseTime_mem {n : ℕ} {T : ℝ} {t : Fin n → ℝ}
    (ht : t ∈ delta n T) : reverseTime T t ∈ delta n T := by
  obtain ⟨hpos, hmono⟩ := Fin.strictMono_cons.mp ht.1
  refine ⟨Fin.strictMono_cons.mpr ⟨?_, ?_⟩, ?_⟩
  · intro i
    exact sub_pos.mpr (ht.2 i.rev)
  · intro i j hij
    exact sub_lt_sub_left (hmono (Fin.rev_lt_rev.mpr hij)) T
  · intro i
    exact sub_lt_self T (hpos i.rev)

private theorem reverseTime_measurable (n : ℕ) (T : ℝ) :
    Measurable (reverseTime (n := n) T) := by
  apply measurable_pi_lambda
  intro i
  exact measurable_const.sub (measurable_pi_apply i.rev)

private theorem reverseTime_volume (n : ℕ) (T : ℝ) :
    MeasurePreserving (reverseTime (n := n) T) volume volume := by
  have hp := volume_measurePreserving_piCongrLeft (fun _ : Fin n => ℝ) Fin.revPerm
  have heq : (fun t : Fin n → ℝ => fun i : Fin n => t i.rev) =
      MeasurableEquiv.piCongrLeft (fun _ : Fin n => ℝ) Fin.revPerm := by
    funext t i
    symm
    simpa only [Fin.revPerm_apply, Fin.rev_rev] using
      (MeasurableEquiv.piCongrLeft_apply_apply (β := fun _ : Fin n => ℝ) Fin.revPerm t i.rev)
  rw [← heq] at hp
  have hc : MeasurePreserving (fun t : Fin n → ℝ => fun i => T - t i) volume volume :=
    volume_preserving_pi (fun _ : Fin n => (volume : Measure ℝ).measurePreserving_sub_left T)
  exact hc.comp hp

private def rho (n : ℕ) (T : ℝ) (t : delta n T) : delta n T :=
  ⟨reverseTime T t.val, reverseTime_mem t.property⟩

private theorem rho_measurable (n : ℕ) (T : ℝ) : Measurable (rho n T) :=
  ((reverseTime_measurable n T).comp measurable_subtype_coe).subtype_mk

private theorem rho_involutive (n : ℕ) (T : ℝ) : Function.Involutive (rho n T) := by
  intro t; apply Subtype.ext
  exact reverseTime_involutive n T t.val

private theorem rho_volume (n : ℕ) (T : ℝ) (hs : MeasurableSet (delta n T)) :
    MeasurePreserving (rho n T) (Measure.comap Subtype.val volume)
      (Measure.comap Subtype.val volume) := by
  have he : reverseTime (n := n) T ⁻¹' delta n T = delta n T := by
    ext t
    constructor
    · intro ht
      have hh := reverseTime_mem ht
      simpa only [reverseTime_involutive n T t] using hh
    · exact reverseTime_mem
  have hr := (reverseTime_volume n T).restrict_preimage hs
  rw [he] at hr
  have hcoe := measurePreserving_subtype_coe (μa := (volume : Measure (Fin n → ℝ))) hs
  refine ⟨rho_measurable n T, ?_⟩
  apply (MeasurableEmbedding.subtype_coe hs).map_injective
  rw [Measure.map_map measurable_subtype_coe (rho_measurable n T)]
  exact (hr.comp hcoe).map_eq.trans hcoe.map_eq.symm



/-- Cancellation of a finite word against its reverse under a common reversing map. -/

Exact compiled region. Generic internal premises are supplied by verified actual maps in the final assembly.

2. Cancel a finite reversed sequence

For updates f_i and a map C satisfying f_i(C(f_i(x)))=C(x), process f_0 through f_(n-1), then apply C and process the updates in reverse order. Induction removes the outer matching pair and leaves C(x). A second finite induction identifies a fold with a prescribed sequence whenever its initial value and one-step recurrences agree. These algebraic statements will be applied to the actual flow and bounce.

\[f_i C f_i=C\ \Longrightarrow\ f_0\cdots f_{n-1}C f_{n-1}\cdots f_0=C.\]
Corresponding Lean step
private theorem reverse_fold_cancel {X : Type*} (C : X → X) (n : ℕ)
    (f : Fin n → X → X) (hf : ∀ i x, f i (C (f i x)) = C x) (x : X) :
    Fin.foldr n f (C (Fin.foldl n (fun z i => f i z) x)) = C x := by
  induction n generalizing x with
  | zero => simp
  | succ n ih =>
    rw [Fin.foldl_succ, Fin.foldr_succ]
    rw [ih (fun i => f i.succ) (fun i => hf i.succ)]
    exact hf 0 x

/-- Finite recursion is the corresponding left fold, without assuming an endpoint. -/
private theorem fold_of_sequence {X : Type*} (n : ℕ) (f : Fin n → X → X)
    (r : Fin (n + 1) → X) (x : X) (hzero : r 0 = x)
    (hstep : ∀ i : Fin n, r i.succ = f i (r i.castSucc)) :
    Fin.foldl n (fun z i => f i z) x = r (Fin.last n) := by
  induction n with
  | zero => simpa using hzero.symm
  | succ n ih =>
    rw [Fin.foldl_succ_last]
    have ht := ih (fun i => f i.castSucc) (fun i => r i.castSucc) hzero
      (fun i => hstep i.castSucc)
    rw [ht]
    exact (hstep (Fin.last n)).symm

Exact compiled region. Generic internal premises are supplied by verified actual maps in the final assembly.

3. Express the endpoint as a finite word of gaps

Append T and prepend 0 to define gaps g_0=t_0, g_j=t_j-t_(j-1), g_n=T-t_(n-1). Reversing the tuple reverses the n+1 gaps exactly. The recursive post-bounce states give the terminal map Phi_(g_n) S Phi_(g_(n-1)) ... S Phi_(g_0). Equivalently start from S(z) and fold f_i=Phi_(g_i) composed with S through i=0,...,n. The first pair of bounces cancels because S is involutive. For n=0 this is just Phi_T(z).

\[g_i(\rho t)=g_{n-i}(t),\qquad A_t=\Phi_{g_n}S\Phi_{g_{n-1}}\cdots S\Phi_{g_0}.\]
Corresponding Lean step
private def gaps {n : ℕ} (T : ℝ) (t : Fin n → ℝ) (i : Fin (n + 1)) : ℝ :=
  (Fin.snoc t T : Fin (n + 1) → ℝ) i - (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) i

private theorem gaps_reversed (n : ℕ) (T : ℝ) (t : Fin n → ℝ) (i : Fin (n + 1)) :
    gaps T (fun j => T - t j.rev) i = gaps T t i.rev := by
  have hl : (Fin.cons (0 : ℝ) (fun j : Fin n => T - t j.rev) : Fin (n + 1) → ℝ) i = T - (Fin.snoc t T : Fin (n + 1) → ℝ) i.rev := by
    induction i using Fin.cases with
    | zero => simp
    | succ j => simp [Fin.rev_succ]
  have hr : (Fin.snoc (fun j : Fin n => T - t j.rev) T : Fin (n + 1) → ℝ) i = T - (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) i.rev := by
    induction i using Fin.lastCases with
    | last => simp
    | cast j => simp [Fin.rev_castSucc]
  unfold gaps
  rw [hl, hr]
  ring

private def post {X : Type*} (Φ : ℝ → X → X) (S : X → X) (n : ℕ)
    (t : Fin n → ℝ) (z : X) : Fin (n + 1) → X :=
  Fin.induction z (fun i x => S (Φ (t i -
    (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) i.castSucc) x))

private def endpoint {X : Type*} (Φ : ℝ → X → X) (S : X → X) (n : ℕ)
    (T : ℝ) (t : Fin n → ℝ) (z : X) : X :=
  Φ (T - (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) (Fin.last n))
    (post Φ S n t z (Fin.last n))

private theorem endpoint_as_word {X : Type*} (Φ : ℝ → X → X) (S : X → X)
    (hS : Function.Involutive S) (n : ℕ) (T : ℝ) (t : Fin n → ℝ) (z : X) :
    endpoint Φ S n T t z =
      Fin.foldl (n + 1) (fun x i => Φ (gaps T t i) (S x)) (S z) := by
  have hSS (x : X) : S (S x) = x := hS x
  let r : Fin (n + 2) → X := Fin.snoc (fun i => S (post Φ S n t z i))
    (endpoint Φ S n T t z)
  have hzero : r 0 = S z := by
    change S (post Φ S n t z 0) = S z
    rfl
  have hstep (i : Fin (n + 1)) : r i.succ = Φ (gaps T t i) (S (r i.castSucc)) := by
    induction i using Fin.lastCases with
    | last =>
      simp only [r, Fin.succ_last, Fin.snoc_last, Fin.snoc_castSucc, endpoint, gaps, hSS]
    | cast j =>
      simp only [r, Fin.succ_castSucc, Fin.snoc_castSucc, post, Fin.induction_succ, gaps, hSS]
  have hf := fold_of_sequence (n + 1) (fun i x => Φ (gaps T t i) (S x)) r (S z) hzero hstep
  simpa only [r, Fin.snoc_last] using hf.symm

Exact compiled region. Generic internal premises are supplied by verified actual maps in the final assembly.

4. Derive the inverse endpoint and its fiber volume

Take C=S composed with R. The identities S^2=R^2=id, RS=SR and R Phi_u R=Phi_(-u), together with the inverse-flow law, imply f_i C f_i=C. Apply reversed-word cancellation and use the reversed-gap identity. The result is A_(rho t)(R A_t(z))=R(z). Separately, finite induction shows a composition of volume-preserving updates preserves volume; since S and each Phi_u preserve ell, so does A_t.

\[A_{\rho t}(R A_t(z))=Rz,\qquad (A_t)_\#\ell=\ell.\]
Corresponding Lean step
private theorem endpoint_reversed {X : Type*} (Φ : ℝ → X → X) (S R : X → X)
    (hS : Function.Involutive S) (hR : Function.Involutive R)
    (hRS : ∀ x, R (S x) = S (R x))
    (hInv : ∀ u x, Φ u (Φ (-u) x) = x)
    (hRev : ∀ u x, R (Φ u (R x)) = Φ (-u) x)
    (n : ℕ) (T : ℝ) (t : Fin n → ℝ) (z : X) :
    endpoint Φ S n T (fun i => T - t i.rev) (R (endpoint Φ S n T t z)) = R z := by
  have hSS (x : X) : S (S x) = x := hS x
  have hRR (x : X) : R (R x) = x := hR x
  have hcomm (u : ℝ) (x : X) : R (Φ u x) = Φ (-u) (R x) := by
    simpa only [hRR] using hRev u (R x)
  let C : X → X := fun x => S (R x)
  let f : Fin (n + 1) → X → X := fun i x => Φ (gaps T t i) (S x)
  have hf (i : Fin (n + 1)) (x : X) : f i (C (f i x)) = C x := by
    dsimp [f, C]
    rw [hSS, hcomm, hInv, hRS]
  rw [endpoint_as_word Φ S hS]
  simp_rw [gaps_reversed]
  change Fin.foldl (n + 1) (fun x i => f i.rev x) (C (endpoint Φ S n T t z)) = R z
  rw [Fin.foldl_rev, endpoint_as_word Φ S hS]
  exact (reverse_fold_cancel C (n + 1) f hf (S z)).trans (by dsimp [C]; rw [hRS, hSS])

private theorem preserving_fold {X : Type*} [MeasurableSpace X] (μ : Measure X)
    (n : ℕ) (f : Fin n → X → X) (hf : ∀ i, MeasurePreserving (f i) μ μ) :
    MeasurePreserving (fun x => Fin.foldl n (fun z i => f i z) x) μ μ := by
  induction n with
  | zero =>
    simp only [Fin.foldl_zero]
    exact ⟨measurable_id, Measure.map_id'⟩
  | succ n ih =>
    simpa only [Fin.foldl_succ_last, Function.comp_def] using
      (hf (Fin.last n)).comp (ih (fun i => f i.castSucc) (fun i => hf i.castSucc))

private theorem endpoint_volume {X : Type*} [MeasurableSpace X] (μ : Measure X)
    (Φ : ℝ → X → X) (S : X → X) (hS : Function.Involutive S)
    (hSM : MeasurePreserving S μ μ) (hΦ : ∀ u, MeasurePreserving (Φ u) μ μ)
    (n : ℕ) (T : ℝ) (t : Fin n → ℝ) : MeasurePreserving (endpoint Φ S n T t) μ μ := by
  have he : endpoint Φ S n T t =
      (fun x => Fin.foldl (n + 1) (fun z i => Φ (gaps T t i) (S z)) x) ∘ S := by
    funext z
    exact endpoint_as_word Φ S hS n T t z
  rw [he]
  exact (preserving_fold μ (n + 1) (fun i z => Φ (gaps T t i) (S z))
    (fun i => (hΦ _).comp hSM)).comp hSM


set_option maxHeartbeats 2400000

Exact compiled region. Generic internal premises are supplied by verified actual maps in the final assembly.

5. Connect the finite word to the actual path at T

The verified ordered-prefix theorem supplies measurability of Delta. The verified finite-count path theorem supplies joint measurability of Gamma and its last-interval formula. Evaluating the measurable function-valued path at T preserves measurability. For n>0 the last event is strictly before T; for n=0 its grid point is zero and T≥0. There is no later record than the final index. Thus the interval formula yields Gamma(T)=Phi_(T-q_n)(z_n), exactly the finite word above. This connection uses the actual live/cemetery history and the original six analytic assumptions.

\[A_{y,r}(z,t)=\Gamma_{y,r,z,t}(T)=\Phi_{y,r,T-q_n}(z_n).\]
Corresponding Lean step
private def endpoint_data_statement
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ) * ‖v‖ ^ 2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) : Prop := by
  classical
  exact
    let c : E → E → E := fun y xRef => y - η • gradient V xRef
    let Φ : E → E → ℝ → (E × E) → (E × E) := fun y xRef t z =>
      (c y xRef + Real.cos t • (z.1 - c y xRef) +
          (Real.sqrt η * Real.sin t) • z.2,
       (-Real.sin t / Real.sqrt η) • (z.1 - c y xRef) + Real.cos t • z.2)
    let S : E → (E × E) → (E × E) := fun xRef z =>
      (z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
        ‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
    let Rec := (ℝ≥0 × (E × E)) ⊕ Unit
    let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
    let Δ : (n : ℕ) → ℝ≥0 → Set (Fin n → ℝ) := fun n T =>
      {t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < (T : ℝ)}
    let Prefix : (n : ℕ) → ℝ≥0 → Type := fun n T => {t : Fin n → ℝ // t ∈ Δ n T}
    let m : (n : ℕ) → (T : ℝ≥0) → Measure (Prefix n T) := fun n T =>
      Measure.comap (fun t : Prefix n T => t.val) (volume : Measure (Fin n → ℝ))
    let zAt : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Fin (n + 1) → (E × E) := fun y xRef z₀ n T t =>
      Fin.induction z₀ (fun i z =>
        S xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc) z))
    let K : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Hist n := fun y xRef z₀ n T t j =>
      Sum.inl (Real.toNNReal ((Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) j), zAt y xRef z₀ n T t j)
    let Path : ℝ≥0 → Type _ := fun T => {s : ℝ≥0 // s ≤ T} → E × E
    let Ψ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Hist n → Path T :=
      fun y xRef z₀ n T h s =>
        Fin.foldl (n + 1) (fun z j => (h j).elim
          (fun a => if a.1 ≤ s.val then Φ y xRef ((s.val - a.1 : ℝ≥0) : ℝ) a.2 else z)
          (fun _ => z)) z₀
    let Γ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → Path T :=
      fun y xRef z₀ n T t => Ψ y xRef z₀ n T (K y xRef z₀ n T t)
    ∀ n : ℕ, ∀ T : ℝ≥0,
      MeasurableSet (Δ n T) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        Γ p.1.1.1 p.1.1.2 p.1.2 n T p.2) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        Γ p.1.1.1 p.1.1.2 p.1.2 n T p.2 ⟨T, le_rfl⟩) ∧
      (∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
        Γ y r z n T t ⟨T, le_rfl⟩ = Φ y r ((T : ℝ) -
          (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) (Fin.last n))
          (zAt y r z n T t (Fin.last n)))

private theorem endpoint_data
    {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) : endpoint_data_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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
  let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
  let Δ : (n : ℕ) → ℝ≥0 → Set (Fin n → ℝ) := fun n T =>
    {t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < (T : ℝ)}
  let Prefix : (n : ℕ) → ℝ≥0 → Type := fun n T => {t : Fin n → ℝ // t ∈ Δ n T}
  let m : (n : ℕ) → (T : ℝ≥0) → Measure (Prefix n T) := fun n T =>
    Measure.comap (fun t : Prefix n T => t.val) (volume : Measure (Fin n → ℝ))
  let zAt : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
      Prefix n T → Fin (n + 1) → (E × E) := fun y xRef z₀ n T t =>
    Fin.induction z₀ (fun i z =>
      S xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc) z))
  let K : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
      Prefix n T → Hist n := fun y xRef z₀ n T t j =>
    Sum.inl (Real.toNNReal ((Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) j), zAt y xRef z₀ n T t j)
  let Path : ℝ≥0 → Type _ := fun T => {s : ℝ≥0 // s ≤ T} → E × E
  let Ψ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Hist n → Path T :=
    fun y xRef z₀ n T h s =>
      Fin.foldl (n + 1) (fun z j => (h j).elim
        (fun a => if a.1 ≤ s.val then Φ y xRef ((s.val - a.1 : ℝ≥0) : ℝ) a.2 else z)
        (fun _ => z)) z₀
  let Γ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → Path T :=
    fun y xRef z₀ n T t => Ψ y xRef z₀ n T (K y xRef z₀ n T t)
  change
    ∀ n : ℕ, ∀ T : ℝ≥0,
      MeasurableSet (Δ n T) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        Γ p.1.1.1 p.1.1.2 p.1.2 n T p.2) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        Γ p.1.1.1 p.1.1.2 p.1.2 n T p.2 ⟨T, le_rfl⟩) ∧
      (∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
        Γ y r z n T t ⟨T, le_rfl⟩ = Φ y r ((T : ℝ) -
          (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) (Fin.last n))
          (zAt y r z n T t (Fin.last n)))
  obtain ⟨Z, hZM, hZarc, hZfallback, hZzero, hdata⟩ :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteCountPath.actual_finite_count_path_law
      hα hαβ hV hH hη hβη
  have hprefix := AutoSamplingTheory.ExampleCases.ProximalBPS.ActualOrderedPrefix.actual_ordered_prefix_law
    hα hαβ hV hH hη hβη
  intro n T
  have hGM : Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
      Γ p.1.1.1 p.1.1.2 p.1.2 n T p.2) := (hdata n T).2.1
  refine ⟨(hprefix n T).1, hGM, (measurable_pi_apply (⟨T, le_rfl⟩ : {s : ℝ≥0 // s ≤ T})).comp hGM, ?_⟩
  intro y r z t
  have hd := (hdata n T).2.2.2 y r z
  have hlast : (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ)
      (Fin.last n) ≤ (T : ℝ) := by
    induction n with
    | zero => simpa using T.coe_nonneg
    | succ n =>
      change t.val (Fin.last n) ≤ (T : ℝ)
      exact (t.property.2 (Fin.last n)).le
  exact hd.2.2.2.2.1 t ⟨T, le_rfl⟩ (Fin.last n) hlast
    (fun k hk => False.elim (not_lt_of_ge (Fin.le_last k) hk))

Exact compiled region. Generic internal premises are supplied by verified actual maps in the final assembly.

6. Assemble the jointly measurable preserving involution

Reuse the actual phase-volume theorem for every flow, bounce and reversal identity; no such identity is an extra public premise. The terminal-data connection gives the measurable endpoint A and its fiber-volume and reversal laws. Hence Theta(z,t)=(R A_t(z),rho t) is jointly measurable and Theta^2(z,t)=(R R z,rho^2 t)=(z,t). The simplex inclusion pushes m to restricted ambient Lebesgue measure, establishing sigma finiteness. In time-first order, apply the measurable skew-product theorem to rho and the ell-preserving fibers z→R A_t(z); swap coordinates before and after to obtain preservation of ell tensor m in the stated phase-first order. This finishes the endpoint change of variables; weighting by Gibbs densities is a later edge.

\[\Theta^2=\mathrm{id},\qquad \Theta_\#(\ell\otimes m_{n,T})=\ell\otimes m_{n,T}.\]
Corresponding Lean step
theorem actual_endpoint_time_reversal_laws
    {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_endpoint_time_reversal_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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
  let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
  let Δ : (n : ℕ) → ℝ≥0 → Set (Fin n → ℝ) := fun n T =>
    {t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < (T : ℝ)}
  let Prefix : (n : ℕ) → ℝ≥0 → Type := fun n T => {t : Fin n → ℝ // t ∈ Δ n T}
  let m : (n : ℕ) → (T : ℝ≥0) → Measure (Prefix n T) := fun n T =>
    Measure.comap (fun t : Prefix n T => t.val) (volume : Measure (Fin n → ℝ))
  let zAt : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
      Prefix n T → Fin (n + 1) → (E × E) := fun y xRef z₀ n T t =>
    Fin.induction z₀ (fun i z =>
      S xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc) z))
  let K : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
      Prefix n T → Hist n := fun y xRef z₀ n T t j =>
    Sum.inl (Real.toNNReal ((Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) j), zAt y xRef z₀ n T t j)
  let Path : ℝ≥0 → Type _ := fun T => {s : ℝ≥0 // s ≤ T} → E × E
  let Ψ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Hist n → Path T :=
    fun y xRef z₀ n T h s =>
      Fin.foldl (n + 1) (fun z j => (h j).elim
        (fun a => if a.1 ≤ s.val then Φ y xRef ((s.val - a.1 : ℝ≥0) : ℝ) a.2 else z)
        (fun _ => z)) z₀
  let Γ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → Path T :=
    fun y xRef z₀ n T t => Ψ y xRef z₀ n T (K y xRef z₀ n T t)
  let R : (E × E) → (E × E) := fun z => (z.1, -z.2)
  let ell : Measure (E × E) := (volume : Measure E).prod (volume : Measure E)
  change
    ∀ n : ℕ, ∀ T : ℝ≥0, ∃ rho : Prefix n T → Prefix n T,
      (∀ t : Prefix n T, ∀ i : Fin n, (rho t).val i = (T : ℝ) - t.val i.rev) ∧
      Measurable rho ∧ Function.Involutive rho ∧ MeasurePreserving rho (m n T) (m n T) ∧
      let A : E → E → (E × E) → Prefix n T → (E × E) :=
        fun y r z t => Γ y r z n T t ⟨T, le_rfl⟩
      let Theta : E → E → ((E × E) × Prefix n T) → ((E × E) × Prefix n T) :=
        fun y r q => (R (A y r q.1 q.2), rho q.2)
      (∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
        A y r z t = Φ y r ((T : ℝ) -
          (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) (Fin.last n))
          (zAt y r z n T t (Fin.last n))) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        A p.1.1.1 p.1.1.2 p.1.2 p.2) ∧
      (∀ y r : E, ∀ t : Prefix n T,
        MeasurePreserving (fun z => A y r z t) ell ell) ∧
      (∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
        A y r (R (A y r z t)) (rho t) = R z) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        Theta p.1.1.1 p.1.1.2 (p.1.2, p.2)) ∧
      (∀ y r : E, Function.Involutive (Theta y r)) ∧
      (∀ y r : E, MeasurePreserving (Theta y r) (ell.prod (m n T)) (ell.prod (m n T)))

  have hed := endpoint_data hα hαβ hV hH hη hβη
  obtain ⟨hΦM, hSM, hRateM, hΦP, hSP, hRP, hΦI, hSI, hRI, hRΦ, hRS, hRate, hInt⟩ :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseReversalVolume.actual_phase_reversal_volume_laws
      hα hαβ hV hH hη hβη
  intro n T
  let rho₀ : Prefix n T → Prefix n T := rho n (T : ℝ)
  have hrM : Measurable rho₀ := rho_measurable n (T : ℝ)
  have hrI : Function.Involutive rho₀ := rho_involutive n (T : ℝ)
  have hrP : MeasurePreserving rho₀ (m n T) (m n T) := rho_volume n (T : ℝ) (hed n T).1
  refine ⟨rho₀, (fun t i => rfl), hrM, hrI, hrP, ?_⟩
  let A : E → E → (E × E) → Prefix n T → (E × E) :=
    fun y r z t => Γ y r z n T t ⟨T, le_rfl⟩
  let Theta : E → E → ((E × E) × Prefix n T) → ((E × E) × Prefix n T) :=
    fun y r q => (R (A y r q.1 q.2), rho₀ q.2)
  change
      (∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
        A y r z t = Φ y r ((T : ℝ) -
          (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) (Fin.last n))
          (zAt y r z n T t (Fin.last n))) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        A p.1.1.1 p.1.1.2 p.1.2 p.2) ∧
      (∀ y r : E, ∀ t : Prefix n T,
        MeasurePreserving (fun z => A y r z t) ell ell) ∧
      (∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
        A y r (R (A y r z t)) (rho₀ t) = R z) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        Theta p.1.1.1 p.1.1.2 (p.1.2, p.2)) ∧
      (∀ y r : E, Function.Involutive (Theta y r)) ∧
      (∀ y r : E, MeasurePreserving (Theta y r) (ell.prod (m n T)) (ell.prod (m n T)))

  have hAm : Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
      A p.1.1.1 p.1.1.2 p.1.2 p.2) := (hed n T).2.2.1
  have hAid (y r : E) (z : E × E) (t : Prefix n T) :
      A y r z t = endpoint (Φ y r) (S r) n (T : ℝ) t.val z := (hed n T).2.2.2 y r z t
  have hAP (y r : E) (t : Prefix n T) : MeasurePreserving (fun z => A y r z t) ell ell := by
    have he : (fun z => A y r z t) = endpoint (Φ y r) (S r) n (T : ℝ) t.val := funext (fun z => hAid y r z t)
    rw [he]
    exact endpoint_volume ell (Φ y r) (S r) (hSI r) (hSP r) (hΦP y r) n (T : ℝ) t.val
  have hAI (y r : E) (z : E × E) (t : Prefix n T) :
      A y r (R (A y r z t)) (rho₀ t) = R z := by
    rw [hAid, hAid]
    exact endpoint_reversed (Φ y r) (S r) R (hSI r) hRI (hRS r)
      (fun u z => (hΦI y r u z).2) (hRΦ y r) n (T : ℝ) t.val z
  have hThetaM : Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
      Theta p.1.1.1 p.1.1.2 (p.1.2, p.2)) :=
    (hRP.measurable.comp hAm).prodMk (hrM.comp measurable_snd)
  refine ⟨(hed n T).2.2.2, hAm, hAP, hAI, hThetaM, ?_, ?_⟩
  · intro y r q
    apply Prod.ext
    · change R (A y r (R (A y r q.1 q.2)) (rho₀ q.2)) = q.1
      rw [hAI]
      exact hRI q.1
    · exact hrI q.2
  · intro y r
    have hs := (hed n T).1
    have hmσ : SigmaFinite ((m n T).map (fun t : Prefix n T => t.val)) := by
      change SigmaFinite ((Measure.comap (fun t : Prefix n T => t.val)
        (volume : Measure (Fin n → ℝ))).map (fun t : Prefix n T => t.val))
      rw [map_comap_subtype_coe hs]
      infer_instance
    letI : SigmaFinite (m n T) := SigmaFinite.of_map (m n T) measurable_subtype_coe.aemeasurable hmσ
    have hm : Measurable (fun q : (E × E) × Prefix n T => R (A y r q.1 q.2)) :=
      hRP.measurable.comp (hAm.comp
        (((measurable_const : Measurable (fun _ : (E × E) × Prefix n T => (y, r))).prodMk
          measurable_fst).prodMk measurable_snd))
    have hp := hrP.skew_product (g := fun t z => R (A y r z t)) (hm.comp measurable_swap)
      (Filter.Eventually.of_forall fun t => (hRP.comp (hAP y r t)).map_eq)
    have hout := (Measure.measurePreserving_swap (μ := m n T) (ν := ell)).comp
      (hp.comp (Measure.measurePreserving_swap (μ := ell) (ν := m n T)))
    exact hout

Exact compiled region. Generic internal premises are supplied by verified actual maps in the final assembly.

Lean verification

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

Lean proof · actual_endpoint_time_reversal_laws

Reverse the ordered time simplex; Cancel a finite reversed sequence; Express the endpoint as a finite word of gaps; Derive the inverse endpoint and its fiber volume; Connect the finite word to the actual path at T; Assemble the jointly measurable preserving involution

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_endpoint_time_reversal_laws
    {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_endpoint_time_reversal_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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
  let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
  let Δ : (n : ℕ) → ℝ≥0 → Set (Fin n → ℝ) := fun n T =>
    {t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < (T : ℝ)}
  let Prefix : (n : ℕ) → ℝ≥0 → Type := fun n T => {t : Fin n → ℝ // t ∈ Δ n T}
  let m : (n : ℕ) → (T : ℝ≥0) → Measure (Prefix n T) := fun n T =>
    Measure.comap (fun t : Prefix n T => t.val) (volume : Measure (Fin n → ℝ))
  let zAt : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
      Prefix n T → Fin (n + 1) → (E × E) := fun y xRef z₀ n T t =>
    Fin.induction z₀ (fun i z =>
      S xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc) z))
  let K : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
      Prefix n T → Hist n := fun y xRef z₀ n T t j =>
    Sum.inl (Real.toNNReal ((Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) j), zAt y xRef z₀ n T t j)
  let Path : ℝ≥0 → Type _ := fun T => {s : ℝ≥0 // s ≤ T} → E × E
  let Ψ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Hist n → Path T :=
    fun y xRef z₀ n T h s =>
      Fin.foldl (n + 1) (fun z j => (h j).elim
        (fun a => if a.1 ≤ s.val then Φ y xRef ((s.val - a.1 : ℝ≥0) : ℝ) a.2 else z)
        (fun _ => z)) z₀
  let Γ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → Path T :=
    fun y xRef z₀ n T t => Ψ y xRef z₀ n T (K y xRef z₀ n T t)
  let R : (E × E) → (E × E) := fun z => (z.1, -z.2)
  let ell : Measure (E × E) := (volume : Measure E).prod (volume : Measure E)
  change
    ∀ n : ℕ, ∀ T : ℝ≥0, ∃ rho : Prefix n T → Prefix n T,
      (∀ t : Prefix n T, ∀ i : Fin n, (rho t).val i = (T : ℝ) - t.val i.rev) ∧
      Measurable rho ∧ Function.Involutive rho ∧ MeasurePreserving rho (m n T) (m n T) ∧
      let A : E → E → (E × E) → Prefix n T → (E × E) :=
        fun y r z t => Γ y r z n T t ⟨T, le_rfl⟩
      let Theta : E → E → ((E × E) × Prefix n T) → ((E × E) × Prefix n T) :=
        fun y r q => (R (A y r q.1 q.2), rho q.2)
      (∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
        A y r z t = Φ y r ((T : ℝ) -
          (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) (Fin.last n))
          (zAt y r z n T t (Fin.last n))) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        A p.1.1.1 p.1.1.2 p.1.2 p.2) ∧
      (∀ y r : E, ∀ t : Prefix n T,
        MeasurePreserving (fun z => A y r z t) ell ell) ∧
      (∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
        A y r (R (A y r z t)) (rho t) = R z) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        Theta p.1.1.1 p.1.1.2 (p.1.2, p.2)) ∧
      (∀ y r : E, Function.Involutive (Theta y r)) ∧
      (∀ y r : E, MeasurePreserving (Theta y r) (ell.prod (m n T)) (ell.prod (m n T)))

  have hed := endpoint_data hα hαβ hV hH hη hβη
  obtain ⟨hΦM, hSM, hRateM, hΦP, hSP, hRP, hΦI, hSI, hRI, hRΦ, hRS, hRate, hInt⟩ :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseReversalVolume.actual_phase_reversal_volume_laws
      hα hαβ hV hH hη hβη
  intro n T
  let rho₀ : Prefix n T → Prefix n T := rho n (T : ℝ)
  have hrM : Measurable rho₀ := rho_measurable n (T : ℝ)
  have hrI : Function.Involutive rho₀ := rho_involutive n (T : ℝ)
  have hrP : MeasurePreserving rho₀ (m n T) (m n T) := rho_volume n (T : ℝ) (hed n T).1
  refine ⟨rho₀, (fun t i => rfl), hrM, hrI, hrP, ?_⟩
  let A : E → E → (E × E) → Prefix n T → (E × E) :=
    fun y r z t => Γ y r z n T t ⟨T, le_rfl⟩
  let Theta : E → E → ((E × E) × Prefix n T) → ((E × E) × Prefix n T) :=
    fun y r q => (R (A y r q.1 q.2), rho₀ q.2)
  change
      (∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
        A y r z t = Φ y r ((T : ℝ) -
          (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) (Fin.last n))
          (zAt y r z n T t (Fin.last n))) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        A p.1.1.1 p.1.1.2 p.1.2 p.2) ∧
      (∀ y r : E, ∀ t : Prefix n T,
        MeasurePreserving (fun z => A y r z t) ell ell) ∧
      (∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
        A y r (R (A y r z t)) (rho₀ t) = R z) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        Theta p.1.1.1 p.1.1.2 (p.1.2, p.2)) ∧
      (∀ y r : E, Function.Involutive (Theta y r)) ∧
      (∀ y r : E, MeasurePreserving (Theta y r) (ell.prod (m n T)) (ell.prod (m n T)))

  have hAm : Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
      A p.1.1.1 p.1.1.2 p.1.2 p.2) := (hed n T).2.2.1
  have hAid (y r : E) (z : E × E) (t : Prefix n T) :
      A y r z t = endpoint (Φ y r) (S r) n (T : ℝ) t.val z := (hed n T).2.2.2 y r z t
  have hAP (y r : E) (t : Prefix n T) : MeasurePreserving (fun z => A y r z t) ell ell := by
    have he : (fun z => A y r z t) = endpoint (Φ y r) (S r) n (T : ℝ) t.val := funext (fun z => hAid y r z t)
    rw [he]
    exact endpoint_volume ell (Φ y r) (S r) (hSI r) (hSP r) (hΦP y r) n (T : ℝ) t.val
  have hAI (y r : E) (z : E × E) (t : Prefix n T) :
      A y r (R (A y r z t)) (rho₀ t) = R z := by
    rw [hAid, hAid]
    exact endpoint_reversed (Φ y r) (S r) R (hSI r) hRI (hRS r)
      (fun u z => (hΦI y r u z).2) (hRΦ y r) n (T : ℝ) t.val z
  have hThetaM : Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
      Theta p.1.1.1 p.1.1.2 (p.1.2, p.2)) :=
    (hRP.measurable.comp hAm).prodMk (hrM.comp measurable_snd)
  refine ⟨(hed n T).2.2.2, hAm, hAP, hAI, hThetaM, ?_, ?_⟩
  · intro y r q
    apply Prod.ext
    · change R (A y r (R (A y r q.1 q.2)) (rho₀ q.2)) = q.1
      rw [hAI]
      exact hRI q.1
    · exact hrI q.2
  · intro y r
    have hs := (hed n T).1
    have hmσ : SigmaFinite ((m n T).map (fun t : Prefix n T => t.val)) := by
      change SigmaFinite ((Measure.comap (fun t : Prefix n T => t.val)
        (volume : Measure (Fin n → ℝ))).map (fun t : Prefix n T => t.val))
      rw [map_comap_subtype_coe hs]
      infer_instance
    letI : SigmaFinite (m n T) := SigmaFinite.of_map (m n T) measurable_subtype_coe.aemeasurable hmσ
    have hm : Measurable (fun q : (E × E) × Prefix n T => R (A y r q.1 q.2)) :=
      hRP.measurable.comp (hAm.comp
        (((measurable_const : Measurable (fun _ : (E × E) × Prefix n T => (y, r))).prodMk
          measurable_fst).prodMk measurable_snd))
    have hp := hrP.skew_product (g := fun t z => R (A y r z t)) (hm.comp measurable_swap)
      (Filter.Eventually.of_forall fun t => (hRP.comp (hAP y r t)).map_eq)
    have hout := (Measure.measurePreserving_swap (μ := m n T) (ν := ell)).comp
      (hp.comp (Measure.measurePreserving_swap (μ := ell) (ν := m n T)))
    exact hout

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualEndpointTimeReversal

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Endpoint/time substitution surrounding A8.Actual Gamma terminal evaluation and measurable preserving involution for exact simplex and phase volume.source-implicitExplicit ASTIS completion of finite-word cancellation, measurable maps and product-volume change of variables; no added premise.
Finite-dimensional Euclidean phase space.Finite-dimensional real Hilbert Borel space including rank zero.generalizationCoordinate-free volume and inner-product formulation.
Original sampler assumptions.All six original analytic assumptions retained.sameActual verified parents discharge all internal provider premises.
Weighted stationary identity and subsequent invariance.Finite endpoint/time volume substitution only.unresolvedGibbs balance, stationary averaging and full invariant probability law remain separate obligations.

No pointwise reversal of right-continuous path values at jumps; no Gibbs density balance, stationary initial averaging/invariance, Markovness, hypocoercivity, implementation error, expected costs, main results or composition.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • domains: Finite Hilbert/Borel carriers and subtype comap expose source Euclidean/simplex volume without normalization; all zero cases retained. — Primary3148-3155,3184-3198; rho_volume and final product proof.
  • objects: Source calls reversed-time complement linear; exact implementation is affine T minus reversed coordinates, with unit absolute Jacobian represented by elementary preserving maps. — Primary3195-3198; reverseTime_volume lines46-59.
  • scopes: Accepted scope is deterministic endpoint/time substitution underlying A8, not literal right-continuous jumpwise path reversal or full weighted A8 invariance argument. Publication and decoder preserve that boundary. — Primary2889-2912,3176-3227; exact endpoint inverse conclusion; publication excludes weighted-stationary-reversal.
  • assumptions: Joint measurability, sigma finiteness, inverse and preserving premises required by internal generic lemmas are proved from actual parent results and comap structure; they do not become public premises. — endpoint_data260-331; final actual93/96 discharge; SigmaFinite.of_map and skew_product399-533.

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
  • No pointwise reversal of right-continuous path values at jumps; no Gibbs density balance, stationary initial averaging/invariance, Markovness, hypocoercivity, implementation error, expected costs, main results or composition.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • MeasurePreserving.skew_product
  • MeasurePreserving.comp
  • Measure.measurePreserving_swap
  • MeasurableEquiv.piCongrLeft
  • map_comap_subtype_coe
  • measurePreserving_subtype_coe
  • SigmaFinite.of_map
  • Fin.foldl_rev
  • Fin.foldl_succ
  • Fin.foldr_succ
  • volume_preserving_pi
  • volume_measurePreserving_piCongrLeft
  • Measure.measurePreserving_sub_left

Mathematical sources

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 finite endpoint/time preserving involution
  • TODO — not closed by these contributions Gibbs-weighted sector reversal and stationary averaging