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

Actual PBPS finite stopped postjump recursion

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, arXiv:2609.06905v1, Algorithm1 and AppendixA.1 equation(A.2), Ex4–8. ASTIS supplies the explicit measurable finite/stopped representation and deterministic zero-threshold extension. Ex9 iid/SLLN nonaccumulation and the full Proposition3.1 process remain later consumers.

arXiv2609.06905v1 · arXiv2609.06905v1 AppendixA.1 equation(A.2), Ex4-8, Algorithm1/Proposition3.1; deterministic finite skeleton feeding future iid/SLLN nonaccumulation. · faithful paraphrase

Complete source statement (Samplinglib restatement)

Let E be a finite-dimensional real inner-product Borel space, including rank zero. Let V:E→ℝ be C², let α,β≥0 satisfy 0<α≤β and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v, and let η>0 with βη≤1. Fix arbitrary y,xRef∈E, z₀=(x₀,p₀)∈E×E and an arbitrary sequence e_n≥0. Define c=y−η∇V(xRef); Φ_t(x,p)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p); S(x,p)=(x,p−(2⟨p,∇V(x)−∇V(xRef)⟩/‖∇V(x)−∇V(xRef)‖²)(∇V(x)−∇V(xRef))), using total real division, so a zero normal gives the identity; λ(x,p)=√η max(0,⟨p,∇V(x)−∇V(xRef)⟩); H(x,p)=(η⁻¹‖x−c‖²+‖p‖²)/2; C(z)=√η β√(2H(z))(√(2ηH(z))+‖c−xRef‖); Λ_z(t)=∫₀ᵗλ(Φ_s z)ds for t≥0; and τ_z(e)=inf{t≥0:Λ_z(t)≥e}∈[0,∞], with inf∅=∞. Records are the disjoint union of finite active pairs (T,z) and a phase-free stopped symbol †. Define next_e(†)=†; for an active (T,z), put next_e(T,z)=† if τ_z(e)=∞, otherwise next_e(T,z)=(T+τ_z(e),S(Φ_(τ_z(e))z)). Define r₀=(0,z₀), r_(n+1)=next_(e_n)(r_n), and T_n as the finite time coordinate when r_n is active and ∞ when it is stopped. Then: (1) the initial record is exactly (0,z₀); (2) the successor identity holds, and an active record stops at the next index iff its actual clock is infinite, otherwise it has exactly the displayed active successor; (3) next is jointly Borel in y,xRef,e,r; (4) for each n, r_n is jointly Borel in y,xRef,z₀ and the whole threshold sequence; (5) T_n is jointly Borel in the same inputs; (6) T₀=0 and T_n is nondecreasing; (7) a stopped record at n remains stopped at every n+k; (8) if r_n=(T,z), then H(z)=H(z₀), and for every t≥0 with t<τ_z(e_n), H(Φ_tz)=H(z₀) and 0≤λ(Φ_tz)≤C(z₀); (9) C₀=C(z₀)≥0, C₀>0 implies T_n+max(e_n/C₀,0)≤T_(n+1) for every n, including stopped records, while C₀=0 and an active record with e_n>0 imply that the next record is stopped; (10) for an active r_n=(T,z), e_n=0 gives r_(n+1)=(T,S(z)), while e_n>0 and a finite active successor (T′,z′) imply T<T′. All statements concern the actual finite indexed recursion with fixed y,xRef. No iid realization, almost-sure nonaccumulation, single physical-time phase in the presence of zero thresholds, all-time process, Markov law, invariance, terminal sampler or cost theorem is asserted.

  • E is a finite-dimensional real inner-product space with its compatible norm and Borel measurable structure; rank zero is allowed. Products and the threshold sequence space carry product measurable structures; the record space carries the native disjoint-union structure.
  • V:E→ℝ is C² on all E. Nonnegative α,β satisfy 0<α≤β, and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v∈E.
  • η>0 and βη≤1. These and the preceding potential conditions are the six original analytic callers. The actual flow, bounce, clock, measurable record maps, conserved energy, cap and increment are produced within the proof, never supplied as callers.
  • y,xRef∈E and initial phase z₀∈E×E are arbitrary. The threshold sequence e:ℕ→[0,∞) is arbitrary, including zeros. It is not assumed to have any probability law; e_n corresponds to source E_(n+1).
  • An active record is (T,z) with finite T≥0 and phase z. A stopped record has no phase and extended event time ∞. The literal next map tests whether the actual first clock is ∞ before evaluating its finite waiting value, flow or bounce.
  • The cap C₀ is the displayed actual formula evaluated at the original z₀. The positive-cap and zero-cap branches have their own implication guards. Strict time growth requires a positive threshold and a finite active successor. Arbitrary zero thresholds may repeat an event time with different postjump phases.

Actual harmonic flow

\[c=y-\eta\nabla V(x_{\rm ref}),\quad\Phi_t(x,p)=\bigl(c+\cos t(x-c)+\sqrt\eta\sin t\,p,-\tfrac{\sin t}{\sqrt\eta}(x-c)+\cos t\,p\bigr).\]

Actual zero-safe reflection and rate

\[h(x)=\nabla V(x)-\nabla V(x_{\rm ref}),\quad S(x,p)=\bigl(x,p-\tfrac{2\langle p,h(x)\rangle}{\|h(x)\|^2}h(x)\bigr),\quad\lambda(x,p)=\sqrt\eta\max\{0,\langle p,h(x)\rangle\}.\]

Actual energy, cap and clock

\[H(z)=\tfrac12(\eta^{-1}\|x-c\|^2+\|p\|^2),\quad C(z)=\sqrt\eta\,\beta\sqrt{2H(z)}\bigl(\sqrt{2\eta H(z)}+\|c-x_{\rm ref}\|\bigr),\quad\Lambda_z(t)=\int_0^t\lambda(\Phi_s z)ds,\quad\tau_z(e)=\inf\{t\ge0:\Lambda_z(t)\ge e\}.\]

Finite active and stopped records

\[\operatorname{next}_e(\dagger)=\dagger,\quad\operatorname{next}_e(T,z)=\begin{cases}\dagger&\tau_z(e)=\infty,\\(T+\tau_z(e),S\Phi_{\tau_z(e)}z)&\tau_z(e)<\infty;\end{cases}\quad r_0=(0,z_0),\quad r_{n+1}=\operatorname{next}_{e_n}(r_n),\quad T_n=\begin{cases}T&r_n=(T,z),\\\infty&r_n=\dagger.\end{cases}\]

Original-energy waiting increment

\[H(z_n)=H(z_0),\quad0\le\lambda(\Phi_tz_n)\le C_0=C(z_0),\quad T_{n+1}\ge T_n+e_n/C_0\ (C_0>0).\]

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 stopped postjump recursion

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursion · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product Borel space, including rank zero. Let V:E→ℝ be C², let α,β≥0 satisfy 0<α≤β and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v, and let η>0 with βη≤1. Fix arbitrary y,xRef∈E, z₀=(x₀,p₀)∈E×E and an arbitrary sequence e_n≥0. Define c=y−η∇V(xRef); Φ_t(x,p)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p); S(x,p)=(x,p−(2⟨p,∇V(x)−∇V(xRef)⟩/‖∇V(x)−∇V(xRef)‖²)(∇V(x)−∇V(xRef))), using total real division, so a zero normal gives the identity; λ(x,p)=√η max(0,⟨p,∇V(x)−∇V(xRef)⟩); H(x,p)=(η⁻¹‖x−c‖²+‖p‖²)/2; C(z)=√η β√(2H(z))(√(2ηH(z))+‖c−xRef‖); Λ_z(t)=∫₀ᵗλ(Φ_s z)ds for t≥0; and τ_z(e)=inf{t≥0:Λ_z(t)≥e}∈[0,∞], with inf∅=∞. Records are the disjoint union of finite active pairs (T,z) and a phase-free stopped symbol †. Define next_e(†)=†; for an active (T,z), put next_e(T,z)=† if τ_z(e)=∞, otherwise next_e(T,z)=(T+τ_z(e),S(Φ_(τ_z(e))z)). Define r₀=(0,z₀), r_(n+1)=next_(e_n)(r_n), and T_n as the finite time coordinate when r_n is active and ∞ when it is stopped. Then: (1) the initial record is exactly (0,z₀); (2) the successor identity holds, and an active record stops at the next index iff its actual clock is infinite, otherwise it has exactly the displayed active successor; (3) next is jointly Borel in y,xRef,e,r; (4) for each n, r_n is jointly Borel in y,xRef,z₀ and the whole threshold sequence; (5) T_n is jointly Borel in the same inputs; (6) T₀=0 and T_n is nondecreasing; (7) a stopped record at n remains stopped at every n+k; (8) if r_n=(T,z), then H(z)=H(z₀), and for every t≥0 with t<τ_z(e_n), H(Φ_tz)=H(z₀) and 0≤λ(Φ_tz)≤C(z₀); (9) C₀=C(z₀)≥0, C₀>0 implies T_n+max(e_n/C₀,0)≤T_(n+1) for every n, including stopped records, while C₀=0 and an active record with e_n>0 imply that the next record is stopped; (10) for an active r_n=(T,z), e_n=0 gives r_(n+1)=(T,S(z)), while e_n>0 and a finite active successor (T′,z′) imply T<T′. All statements concern the actual finite indexed recursion with fixed y,xRef. No iid realization, almost-sure nonaccumulation, single physical-time phase in the presence of zero thresholds, all-time process, Markov law, invariance, terminal sampler or cost theorem is asserted.

\[c=y-\eta\nabla V(x_{\rm ref}),\quad\Phi_t(x,p)=\bigl(c+\cos t(x-c)+\sqrt\eta\sin t\,p,-\tfrac{\sin t}{\sqrt\eta}(x-c)+\cos t\,p\bigr).\quad h(x)=\nabla V(x)-\nabla V(x_{\rm ref}),\quad S(x,p)=\bigl(x,p-\tfrac{2\langle p,h(x)\rangle}{\|h(x)\|^2}h(x)\bigr),\quad\lambda(x,p)=\sqrt\eta\max\{0,\langle p,h(x)\rangle\}.\quad H(z)=\tfrac12(\eta^{-1}\|x-c\|^2+\|p\|^2),\quad C(z)=\sqrt\eta\,\beta\sqrt{2H(z)}\bigl(\sqrt{2\eta H(z)}+\|c-x_{\rm ref}\|\bigr),\quad\Lambda_z(t)=\int_0^t\lambda(\Phi_s z)ds,\quad\tau_z(e)=\inf\{t\ge0:\Lambda_z(t)\ge e\}.\quad \operatorname{next}_e(\dagger)=\dagger,\quad\operatorname{next}_e(T,z)=\begin{cases}\dagger&\tau_z(e)=\infty,\\(T+\tau_z(e),S\Phi_{\tau_z(e)}z)&\tau_z(e)<\infty;\end{cases}\quad r_0=(0,z_0),\quad r_{n+1}=\operatorname{next}_{e_n}(r_n),\quad T_n=\begin{cases}T&r_n=(T,z),\\\infty&r_n=\dagger.\end{cases}\quad H(z_n)=H(z_0),\quad0\le\lambda(\Phi_tz_n)\le C_0=C(z_0),\quad T_{n+1}\ge T_n+e_n/C_0\ (C_0>0).\]
Lean statement · actual_fixed_reference_finite_jump_recursion

Let E be a finite-dimensional real inner-product Borel space, including rank zero. Let V:E→ℝ be C², let α,β≥0 satisfy 0<α≤β and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v, and let η>0 with βη≤1. Fix arbitrary y,xRef∈E, z₀=(x₀,p₀)∈E×E and an arbitrary sequence e_n≥0. Define c=y−η∇V(xRef); Φ_t(x,p)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p); S(x,p)=(x,p−(2⟨p,∇V(x)−∇V(xRef)⟩/‖∇V(x)−∇V(xRef)‖²)(∇V(x)−∇V(xRef))), using total real division, so a zero normal gives the identity; λ(x,p)=√η max(0,⟨p,∇V(x)−∇V(xRef)⟩); H(x,p)=(η⁻¹‖x−c‖²+‖p‖²)/2; C(z)=√η β√(2H(z))(√(2ηH(z))+‖c−xRef‖); Λ_z(t)=∫₀ᵗλ(Φ_s z)ds for t≥0; and τ_z(e)=inf{t≥0:Λ_z(t)≥e}∈[0,∞], with inf∅=∞. Records are the disjoint union of finite active pairs (T,z) and a phase-free stopped symbol †. Define next_e(†)=†; for an active (T,z), put next_e(T,z)=† if τ_z(e)=∞, otherwise next_e(T,z)=(T+τ_z(e),S(Φ_(τ_z(e))z)). Define r₀=(0,z₀), r_(n+1)=next_(e_n)(r_n), and T_n as the finite time coordinate when r_n is active and ∞ when it is stopped. Then: (1) the initial record is exactly (0,z₀); (2) the successor identity holds, and an active record stops at the next index iff its actual clock is infinite, otherwise it has exactly the displayed active successor; (3) next is jointly Borel in y,xRef,e,r; (4) for each n, r_n is jointly Borel in y,xRef,z₀ and the whole threshold sequence; (5) T_n is jointly Borel in the same inputs; (6) T₀=0 and T_n is nondecreasing; (7) a stopped record at n remains stopped at every n+k; (8) if r_n=(T,z), then H(z)=H(z₀), and for every t≥0 with t<τ_z(e_n), H(Φ_tz)=H(z₀) and 0≤λ(Φ_tz)≤C(z₀); (9) C₀=C(z₀)≥0, C₀>0 implies T_n+max(e_n/C₀,0)≤T_(n+1) for every n, including stopped records, while C₀=0 and an active record with e_n>0 imply that the next record is stopped; (10) for an active r_n=(T,z), e_n=0 gives r_(n+1)=(T,S(z)), while e_n>0 and a finite active successor (T′,z′) imply T<T′. All statements concern the actual finite indexed recursion with fixed y,xRef. No iid realization, almost-sure nonaccumulation, single physical-time phase in the presence of zero thresholds, all-time process, Markov law, invariance, terminal sampler or cost theorem is asserted.

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_fixed_reference_finite_jump_recursion
    {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_fixed_reference_finite_jump_recursion_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_fixed_reference_finite_jump_recursion_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_fixed_reference_finite_jump_recursion_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 H : E → E → (E × E) → ℝ := fun y xRef z =>
      (η⁻¹ * ‖z.1 - c y xRef‖ ^ 2 + ‖z.2‖ ^ 2) / 2
    let C : E → E → (E × E) → ℝ := fun y xRef z =>
      Real.sqrt η * (β : ℝ) * Real.sqrt (2 * H y xRef z) *
        (Real.sqrt (2 * η * H y xRef z) + ‖c y xRef - 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 eventTime : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ → WithTop ℝ≥0 :=
      fun y xRef z₀ e n => (record y xRef z₀ e n).elim
        (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
    (∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0,
      record y xRef z₀ e 0 = Sum.inl (0, z₀)) ∧
    (∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n : ℕ,
      record y xRef z₀ e (n + 1) = next y xRef (e n) (record y xRef z₀ e n) ∧
      (∀ a : ℝ≥0 × (E × E), record y xRef z₀ e n = Sum.inl a →
        (record y xRef z₀ e (n + 1) = Sum.inr () ↔ τ y xRef a.2 (e n) = ⊤) ∧
        (τ y xRef a.2 (e n) ≠ ⊤ → record y xRef z₀ e (n + 1) =
          Sum.inl (a.1 + (τ y xRef a.2 (e n)).untopD 0,
            S xRef (Φ y xRef (((τ y xRef a.2 (e n)).untopD 0 : ℝ≥0) : ℝ) a.2))))) ∧
    Measurable (fun a : (E × E) × ℝ≥0 × ((ℝ≥0 × (E × E)) ⊕ Unit) =>
      next a.1.1 a.1.2 a.2.1 a.2.2) ∧
    (∀ n : ℕ, Measurable (fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
      record a.1.1 a.1.2 a.2.1 a.2.2 n)) ∧
    (∀ n : ℕ, Measurable (fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
      eventTime a.1.1 a.1.2 a.2.1 a.2.2 n)) ∧
    (∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0,
      eventTime y xRef z₀ e 0 = 0 ∧ Monotone (eventTime y xRef z₀ e)) ∧
    (∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n k : ℕ,
      record y xRef z₀ e n = Sum.inr () →
        record y xRef z₀ e (n + k) = Sum.inr ()) ∧
    (∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n : ℕ,
      ∀ a : ℝ≥0 × (E × E), record y xRef z₀ e n = Sum.inl a →
        H y xRef a.2 = H y xRef z₀ ∧
        ∀ t : ℝ≥0, (t : WithTop ℝ≥0) < τ y xRef a.2 (e n) →
          H y xRef (Φ y xRef (t : ℝ) a.2) = H y xRef z₀ ∧
          0 ≤ rate xRef (Φ y xRef (t : ℝ) a.2) ∧
          rate xRef (Φ y xRef (t : ℝ) a.2) ≤ C y xRef z₀) ∧
    (∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0,
      0 ≤ C y xRef z₀ ∧
      (0 < C y xRef z₀ → ∀ n : ℕ,
        eventTime y xRef z₀ e n +
          (Real.toNNReal ((e n : ℝ) / C y xRef z₀) : WithTop ℝ≥0) ≤
        eventTime y xRef z₀ e (n + 1)) ∧
      (C y xRef z₀ = 0 → ∀ n : ℕ, ∀ a : ℝ≥0 × (E × E),
        record y xRef z₀ e n = Sum.inl a → 0 < e n →
          record y xRef z₀ e (n + 1) = Sum.inr ())) ∧
    (∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n : ℕ,
      ∀ a : ℝ≥0 × (E × E), record y xRef z₀ e n = Sum.inl a →
        (e n = 0 → record y xRef z₀ e (n + 1) = Sum.inl (a.1, S xRef a.2)) ∧
        (∀ b : ℝ≥0 × (E × E), 0 < e n →
          record y xRef z₀ e (n + 1) = Sum.inl b → a.1 < b.1))

set_option maxHeartbeats 1600000 in

Exact module and namespace context

Proof roadmap

  1. 1Reuse actual flow, bounce and first-clock laws

    Invoke the compiled laws of the literal harmonic flow, zero-safe bounce/rate and integrated-hazard clock under the same six original analytic callers. Extract joint measurability, flow and bounce energy preservation, nonnegative actual rate, same-energy-layer cap, positive/zero threshold clocks and extended waiting lower bound. No abstract transition or cap certificate is assumed.

  2. 2Identify the literal finite and stopped recursion branches

    The initial and successor identities unfold Nat.rec. If the current record is active, split on whether its actual first clock is infinite. The infinite branch is exactly stopped; the other branch contains the finite waiting value and the actual flow followed by bounce.

  3. 3Prove joint Borel measurability of one actual successor

    On active inputs, compose the jointly Borel clock with the parameter/phase/threshold projections. The finite-value extraction is Borel; the equality-to-infinity guard is Borel. Compose the actual jointly Borel flow and bounce for the finite branch, then use measurable conditional and disjoint-union maps. A measurable product-over-sum equivalence includes the stopped constant branch.

  4. 4Prove joint Borel finite record and event-time maps

    Induct on the finite index. The initial map injects (0,z₀); each successor composes the Borel next map with the previous record and the measurable n-th coordinate of the threshold sequence. The event-time map is the disjoint union of the finite time projection followed by extended-time inclusion and the constant ∞ map.

  5. 5Carry the original energy through every active finite index

    Induct on the index, generalizing the candidate active record. At zero the phase is z₀. A stopped predecessor or infinite clock cannot produce an active successor. A finite active successor is SΦ_q(z); flow preservation and bounce preservation give H(SΦ_q(z))=H(z)=H(z₀).

  6. 6Prove nondecreasing event times and stopped absorption

    At every successor, stopped records remain stopped and have time ∞. An active record either stops, increasing its extended time to ∞, or adds a nonnegative finite wait. Successor monotonicity gives monotonicity on ℕ. A separate induction on k proves that stopping at n persists at n+k.

  7. 7Use the original energy for every outgoing arc and cap

    For an active phase z, combine its inherited H(z)=H(z₀) with H(Φ_tz)=H(z). The actual rate is nonnegative, and the already proved same-energy-layer bound gives λ(Φ_tz)≤C(z₀). Since C depends on phase only through H, it also gives C(z)=C(z₀). The displayed arc conclusion keeps its source t<τ guard.

  8. 8Derive the uniform extended waiting increment

    For C₀>0, the actual clock bound at the current active phase gives τ_z(e_n)≥e_n/C(z). Replace C(z) by the proved C₀, then add the existing finite event time. An infinite next clock gives the extended inequality automatically. Already stopped records have ∞ on both sides, so the inequality remains valid for every n.

  9. 9Handle zero original cap with a positive threshold

    For an active phase, its proved cap equals C₀. If C₀=0 and e_n>0, the actual one-clock zero-cap law says τ_z(e_n)=∞; the exact active stopping equivalence then makes the successor stopped. This conclusion makes no finite-clock assumption.

  10. 10Keep zero thresholds and strict positive finite growth distinct

    For e_n=0, the exact clock is zero and Φ_0 is the identity, yielding (T,Sz) at the same event time. For a positive threshold with an active successor, the clock must be finite; its strict positivity gives a strictly positive finite waiting value, hence T<T′. Collect the ten conclusion groups. Repeated zero-threshold times do not define a single physical-time phase or prove nonaccumulation.

Full assumptions and notation

All objects and hypotheses

  • E is a finite-dimensional real inner-product space with its compatible norm and Borel measurable structure; rank zero is allowed. Products and the threshold sequence space carry product measurable structures; the record space carries the native disjoint-union structure.
  • V:E→ℝ is C² on all E. Nonnegative α,β satisfy 0<α≤β, and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v∈E.
  • η>0 and βη≤1. These and the preceding potential conditions are the six original analytic callers. The actual flow, bounce, clock, measurable record maps, conserved energy, cap and increment are produced within the proof, never supplied as callers.
  • y,xRef∈E and initial phase z₀∈E×E are arbitrary. The threshold sequence e:ℕ→[0,∞) is arbitrary, including zeros. It is not assumed to have any probability law; e_n corresponds to source E_(n+1).
  • An active record is (T,z) with finite T≥0 and phase z. A stopped record has no phase and extended event time ∞. The literal next map tests whether the actual first clock is ∞ before evaluating its finite waiting value, flow or bounce.
  • The cap C₀ is the displayed actual formula evaluated at the original z₀. The positive-cap and zero-cap branches have their own implication guards. Strict time growth requires a positive threshold and a finite active successor. Arbitrary zero thresholds may repeat an event time with different postjump phases.

Mathematical proof

1. Reuse actual flow, bounce and first-clock laws

Invoke the compiled laws of the literal harmonic flow, zero-safe bounce/rate and integrated-hazard clock under the same six original analytic callers. Extract joint measurability, flow and bounce energy preservation, nonnegative actual rate, same-energy-layer cap, positive/zero threshold clocks and extended waiting lower bound. No abstract transition or cap certificate is assumed.

\[H(\Phi_tz)=H(z),\ H(Sz)=H(z),\ \lambda(z)\ge0,\ \tau_z(0)=0,\ e>0\Rightarrow\tau_z(e)>0.\]
Corresponding Lean step
  have hf := ActualHarmonicFlow.actual_harmonic_flow_laws hα hαβ hV hH hη hβη
  have hb := ActualBounceRate.actual_bounce_rate_energy_laws hα hαβ hV hH hη hβη
  have hk := ActualHazardClock.actual_integrated_hazard_clock_laws hα hαβ hV hH hη hβη
  have hΦmeas : Measurable (fun a : (E × E) × ℝ × (E × E) =>
      Φ a.1.1 a.1.2 a.2.1 a.2.2) := hf.2.1
  have hΦzero (y xRef : E) (z : E × E) : Φ y xRef 0 z = z := hf.2.2.1 y xRef z
  have hΦH (y xRef : E) (t : ℝ) (z : E × E) :
      H y xRef (Φ y xRef t z) = H y xRef z := hf.2.2.2.2.2.2.2.1 y xRef t z
  have hSmeas : Measurable (fun a : E × (E × E) => S a.1 a.2) := hb.1
  have hSH (y xRef : E) (z : E × E) : H y xRef (S xRef z) = H y xRef z :=
    hb.2.2.2.2.2.2.1 y xRef z
  have hrate0 (xRef : E) (z : E × E) : 0 ≤ rate xRef z :=
    (hb.2.2.2.2.2.2.2.1 xRef z).1
  have hratecap (y xRef : E) (z₀ z : E × E) (hz : H y xRef z = H y xRef z₀) :
      rate xRef z ≤ C y xRef z₀ :=
    ((hb.2.2.2.2.2.2.2.2.2 y xRef z₀).2 z hz).2.2
  have hτpositive (y xRef : E) (z : E × E) (e : ℝ≥0) :
      0 < e → (0 : WithTop ℝ≥0) < τ y xRef z e :=
    (hk.2.2.2.2.2.1 y xRef z e).2.2.1
  have hτzero (y xRef : E) (z : E × E) : τ y xRef z 0 = 0 :=
    (hk.2.2.2.2.2.1 y xRef z 0).2.2.2
  have hτmeas : Measurable (fun a : (E × E) × (E × E) × ℝ≥0 =>
      τ a.1.1 a.1.2 a.2.1 a.2.2) := hk.2.2.2.2.2.2.1
  have hC0 (y xRef : E) (z : E × E) : 0 ≤ C y xRef z :=
    (hk.2.2.2.2.2.2.2.2.1 y xRef z).1
  have hwait (y xRef : E) (z : E × E) (e : ℝ≥0) :
      (0 < C y xRef z →
        (Real.toNNReal ((e : ℝ) / C y xRef z) : WithTop ℝ≥0) ≤ τ y xRef z e) ∧
      (C y xRef z = 0 → 0 < e → τ y xRef z e = ⊤) :=
    hk.2.2.2.2.2.2.2.2.2 y xRef z e
  have hfiniteval (q : ℝ≥0) : (q : WithTop ℝ≥0).untopD 0 = q := rfl
  have hzeroval : (0 : WithTop ℝ≥0).untopD 0 = 0 := rfl

Exact contiguous compiled public BODY. The eleven literal definitions and preceding facts remain in scope. All stochastic nonaccumulation and global-process consumers remain separate.

2. Identify the literal finite and stopped recursion branches

The initial and successor identities unfold Nat.rec. If the current record is active, split on whether its actual first clock is infinite. The infinite branch is exactly stopped; the other branch contains the finite waiting value and the actual flow followed by bounce.

\[r_0=(0,z_0),\quad r_{n+1}=\operatorname{next}_{e_n}(r_n),\quad r_n=(T,z)\Rightarrow(r_{n+1}=\dagger\iff\tau_z(e_n)=\infty).\]
Corresponding Lean step
  have hrec0 (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) :
      record y xRef z₀ e 0 = Sum.inl (0, z₀) := rfl
  have hrecstep (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ) :
      record y xRef z₀ e (n + 1) = next y xRef (e n) (record y xRef z₀ e n) := rfl
  have hbranches (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ)
      (a : ℝ≥0 × (E × E)) (ha : record y xRef z₀ e n = Sum.inl a) :
      (record y xRef z₀ e (n + 1) = Sum.inr () ↔ τ y xRef a.2 (e n) = ⊤) ∧
      (τ y xRef a.2 (e n) ≠ ⊤ → record y xRef z₀ e (n + 1) =
        Sum.inl (a.1 + (τ y xRef a.2 (e n)).untopD 0,
          S xRef (Φ y xRef (((τ y xRef a.2 (e n)).untopD 0 : ℝ≥0) : ℝ) a.2))) := by
    rw [hrecstep, ha]
    dsimp only [next]
    split_ifs with ht <;> simp [ht]

Exact contiguous compiled public BODY. The eleven literal definitions and preceding facts remain in scope. All stochastic nonaccumulation and global-process consumers remain separate.

3. Prove joint Borel measurability of one actual successor

On active inputs, compose the jointly Borel clock with the parameter/phase/threshold projections. The finite-value extraction is Borel; the equality-to-infinity guard is Borel. Compose the actual jointly Borel flow and bounce for the finite branch, then use measurable conditional and disjoint-union maps. A measurable product-over-sum equivalence includes the stopped constant branch.

\[(y,x_{\rm ref},e,r)\longmapsto\operatorname{next}_e(r)\text{ is Borel}.\]
Corresponding Lean step
  have hnextmeas : Measurable
      (fun a : (E × E) × ℝ≥0 × ((ℝ≥0 × (E × E)) ⊕ Unit) =>
        next a.1.1 a.1.2 a.2.1 a.2.2) := by
    let g : ((E × E) × ℝ≥0) × (ℝ≥0 × (E × E)) →
        ((ℝ≥0 × (E × E)) ⊕ Unit) := fun a =>
      if τ a.1.1.1 a.1.1.2 a.2.2 a.1.2 = ⊤ then Sum.inr () else
        Sum.inl (a.2.1 + (τ a.1.1.1 a.1.1.2 a.2.2 a.1.2).untopD 0,
          S a.1.1.2 (Φ a.1.1.1 a.1.1.2
            (((τ a.1.1.1 a.1.1.2 a.2.2 a.1.2).untopD 0 : ℝ≥0) : ℝ) a.2.2))
    have hparams : Measurable
        (fun a : ((E × E) × ℝ≥0) × (ℝ≥0 × (E × E)) =>
          (a.1.1, a.2.2, a.1.2)) :=
      measurable_fst.fst.prodMk (measurable_snd.snd.prodMk measurable_fst.snd)
    have ht0 := hτmeas.comp hparams
    have ht : Measurable (fun a : ((E × E) × ℝ≥0) × (ℝ≥0 × (E × E)) =>
        τ a.1.1.1 a.1.1.2 a.2.2 a.1.2) := ht0
    have hq := ht.untopD (0 : ℝ≥0)
    have hp := hΦmeas.comp (measurable_fst.fst.prodMk
      ((measurable_coe_nnreal_real.comp hq).prodMk measurable_snd.snd))
    have hs := hSmeas.comp (measurable_fst.fst.snd.prodMk hp)
    have hg : Measurable g := measurable_const.ite
      (measurableSet_eq_fun ht measurable_const)
      (measurable_inl.comp ((measurable_snd.fst.add hq).prodMk hs))
    have hsum := hg.sumElim
      (show Measurable (fun _ : ((E × E) × ℝ≥0) × Unit =>
        (Sum.inr () : (ℝ≥0 × (E × E)) ⊕ Unit)) from measurable_const)
    have hm := hsum.comp ((MeasurableEquiv.prodSumDistrib
      ((E × E) × ℝ≥0) (ℝ≥0 × (E × E)) Unit).measurable.comp
      ((measurable_fst.prodMk measurable_snd.fst).prodMk measurable_snd.snd))
    convert hm using 1
    funext a
    rcases a with ⟨⟨y, xRef⟩, e, r⟩
    cases r <;> rfl

Exact contiguous compiled public BODY. The eleven literal definitions and preceding facts remain in scope. All stochastic nonaccumulation and global-process consumers remain separate.

4. Prove joint Borel finite record and event-time maps

Induct on the finite index. The initial map injects (0,z₀); each successor composes the Borel next map with the previous record and the measurable n-th coordinate of the threshold sequence. The event-time map is the disjoint union of the finite time projection followed by extended-time inclusion and the constant ∞ map.

\[(y,x_{\rm ref},z_0,e)\longmapsto r_n\text{ and }T_n\text{ are Borel for every }n.\]
Corresponding Lean step
  have hrecordmeas (n : ℕ) : Measurable
      (fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
        record a.1.1 a.1.2 a.2.1 a.2.2 n) := by
    induction n with
    | zero => exact measurable_inl.comp (measurable_const.prodMk measurable_snd.fst)
    | succ n ih =>
      exact hnextmeas.comp (measurable_fst.prodMk
        (((measurable_pi_apply n).comp measurable_snd.snd).prodMk ih))
  have htimemeas (n : ℕ) : Measurable
      (fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
        eventTime a.1.1 a.1.2 a.2.1 a.2.2 n) :=
    ((WithTop.measurable_coe.comp measurable_fst).sumElim measurable_const).comp
      (hrecordmeas n)

Exact contiguous compiled public BODY. The eleven literal definitions and preceding facts remain in scope. All stochastic nonaccumulation and global-process consumers remain separate.

5. Carry the original energy through every active finite index

Induct on the index, generalizing the candidate active record. At zero the phase is z₀. A stopped predecessor or infinite clock cannot produce an active successor. A finite active successor is SΦ_q(z); flow preservation and bounce preservation give H(SΦ_q(z))=H(z)=H(z₀).

\[r_n=(T,z)\Longrightarrow H(z)=H(z_0),\quad H(S\Phi_qz)=H(\Phi_qz)=H(z).\]
Corresponding Lean step
  have henergy (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ)
      (a : ℝ≥0 × (E × E)) (ha : record y xRef z₀ e n = Sum.inl a) :
      H y xRef a.2 = H y xRef z₀ := by
    induction n generalizing a with
    | zero =>
      have heq : (0, z₀) = a := Sum.inl.inj ha
      subst a
      rfl
    | succ n ih =>
      rw [hrecstep] at ha
      cases hr : record y xRef z₀ e n with
      | inr u => simp [hr, next] at ha
      | inl b =>
        rw [hr] at ha
        dsimp only [next] at ha
        by_cases ht : τ y xRef b.2 (e n) = ⊤
        · simp only [if_pos ht] at ha
          cases ha
        · rw [if_neg ht] at ha
          have heq := Sum.inl.inj ha
          rw [← heq]
          exact (hSH y xRef _).trans ((hΦH y xRef _ _).trans (ih b hr))

Exact contiguous compiled public BODY. The eleven literal definitions and preceding facts remain in scope. All stochastic nonaccumulation and global-process consumers remain separate.

6. Prove nondecreasing event times and stopped absorption

At every successor, stopped records remain stopped and have time ∞. An active record either stops, increasing its extended time to ∞, or adds a nonnegative finite wait. Successor monotonicity gives monotonicity on ℕ. A separate induction on k proves that stopping at n persists at n+k.

\[T_0=0,\quad T_n\le T_{n+1},\quad r_n=\dagger\Rightarrow r_{n+k}=\dagger.\]
Corresponding Lean step
  have hmono (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) :
      Monotone (eventTime y xRef z₀ e) := by
    apply monotone_nat_of_le_succ
    intro n
    dsimp only [eventTime]
    rw [hrecstep]
    cases hr : record y xRef z₀ e n with
    | inr u => simp [next]
    | inl a =>
      dsimp only [next]
      split_ifs with ht
      · exact le_top
      · exact WithTop.coe_le_coe.mpr (le_add_of_nonneg_right zero_le)
  have hstopped (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n k : ℕ)
      (hn : record y xRef z₀ e n = Sum.inr ()) :
      record y xRef z₀ e (n + k) = Sum.inr () := by
    induction k with
    | zero => simpa using hn
    | succ k ih => simpa only [Nat.add_succ, hrecstep, ih, next]

Exact contiguous compiled public BODY. The eleven literal definitions and preceding facts remain in scope. All stochastic nonaccumulation and global-process consumers remain separate.

7. Use the original energy for every outgoing arc and cap

For an active phase z, combine its inherited H(z)=H(z₀) with H(Φ_tz)=H(z). The actual rate is nonnegative, and the already proved same-energy-layer bound gives λ(Φ_tz)≤C(z₀). Since C depends on phase only through H, it also gives C(z)=C(z₀). The displayed arc conclusion keeps its source t<τ guard.

\[H(\Phi_tz)=H(z_0),\quad0\le\lambda(\Phi_tz)\le C(z_0),\quad C(z)=C(z_0).\]
Corresponding Lean step
  have harcs (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ)
      (a : ℝ≥0 × (E × E)) (ha : record y xRef z₀ e n = Sum.inl a) :
      H y xRef a.2 = H y xRef z₀ ∧
      ∀ t : ℝ≥0, (t : WithTop ℝ≥0) < τ y xRef a.2 (e n) →
        H y xRef (Φ y xRef (t : ℝ) a.2) = H y xRef z₀ ∧
        0 ≤ rate xRef (Φ y xRef (t : ℝ) a.2) ∧
        rate xRef (Φ y xRef (t : ℝ) a.2) ≤ C y xRef z₀ := by
    have hEa := henergy y xRef z₀ e n a ha
    refine ⟨hEa, fun t _ => ?_⟩
    have hEt := (hΦH y xRef t a.2).trans hEa
    exact ⟨hEt, hrate0 xRef _, hratecap y xRef z₀ _ hEt⟩
  have hcap_eq (y xRef : E) (z₀ z : E × E) (hz : H y xRef z = H y xRef z₀) :
      C y xRef z = C y xRef z₀ := by simp only [C, hz]

Exact contiguous compiled public BODY. The eleven literal definitions and preceding facts remain in scope. All stochastic nonaccumulation and global-process consumers remain separate.

8. Derive the uniform extended waiting increment

For C₀>0, the actual clock bound at the current active phase gives τ_z(e_n)≥e_n/C(z). Replace C(z) by the proved C₀, then add the existing finite event time. An infinite next clock gives the extended inequality automatically. Already stopped records have ∞ on both sides, so the inequality remains valid for every n.

\[C_0>0\Longrightarrow T_n+\max\{e_n/C_0,0\}\le T_{n+1}.\]
Corresponding Lean step
  have hincrement (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0)
      (hC : 0 < C y xRef z₀) (n : ℕ) :
      eventTime y xRef z₀ e n +
        (Real.toNNReal ((e n : ℝ) / C y xRef z₀) : WithTop ℝ≥0) ≤
      eventTime y xRef z₀ e (n + 1) := by
    cases hr : record y xRef z₀ e n with
    | inr u =>
      dsimp only [eventTime]
      rw [hrecstep, hr]
      change (⊤ : WithTop ℝ≥0) + _ ≤ ⊤
      exact le_top
    | inl a =>
      have hCa := hcap_eq y xRef z₀ a.2 (henergy y xRef z₀ e n a hr)
      have hw := (hwait y xRef a.2 (e n)).1 (by simpa only [hCa] using hC)
      rw [hCa] at hw
      dsimp only [eventTime]
      rw [hrecstep, hr]
      dsimp only [next]
      split_ifs with ht
      · exact le_top
      · have hq : (((τ y xRef a.2 (e n)).untopD 0 : ℝ≥0) : WithTop ℝ≥0) =
            τ y xRef a.2 (e n) := by
          induction hτ : τ y xRef a.2 (e n) using WithTop.recTopCoe with
          | top => exact False.elim (ht hτ)
          | coe q => exact congrArg (fun q : ℝ≥0 => (q : WithTop ℝ≥0)) (hfiniteval q)
        change (a.1 : WithTop ℝ≥0) + _ ≤
          ((a.1 + (τ y xRef a.2 (e n)).untopD 0 : ℝ≥0) : WithTop ℝ≥0)
        rw [WithTop.coe_add, hq]
        exact add_le_add le_rfl hw

Exact contiguous compiled public BODY. The eleven literal definitions and preceding facts remain in scope. All stochastic nonaccumulation and global-process consumers remain separate.

9. Handle zero original cap with a positive threshold

For an active phase, its proved cap equals C₀. If C₀=0 and e_n>0, the actual one-clock zero-cap law says τ_z(e_n)=∞; the exact active stopping equivalence then makes the successor stopped. This conclusion makes no finite-clock assumption.

\[C_0=0,\ r_n=(T,z),\ e_n>0\Longrightarrow\tau_z(e_n)=\infty\Longrightarrow r_{n+1}=\dagger.\]
Corresponding Lean step
  have hzerocap (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0)
      (hC : C y xRef z₀ = 0) (n : ℕ) (a : ℝ≥0 × (E × E))
      (ha : record y xRef z₀ e n = Sum.inl a) (he : 0 < e n) :
      record y xRef z₀ e (n + 1) = Sum.inr () := by
    apply (hbranches y xRef z₀ e n a ha).1.mpr
    apply (hwait y xRef a.2 (e n)).2 _ he
    exact (hcap_eq y xRef z₀ a.2 (henergy y xRef z₀ e n a ha)).trans hC

Exact contiguous compiled public BODY. The eleven literal definitions and preceding facts remain in scope. All stochastic nonaccumulation and global-process consumers remain separate.

10. Keep zero thresholds and strict positive finite growth distinct

For e_n=0, the exact clock is zero and Φ_0 is the identity, yielding (T,Sz) at the same event time. For a positive threshold with an active successor, the clock must be finite; its strict positivity gives a strictly positive finite waiting value, hence T<T′. Collect the ten conclusion groups. Repeated zero-threshold times do not define a single physical-time phase or prove nonaccumulation.

\[e_n=0\Rightarrow r_{n+1}=(T,Sz),\qquad e_n>0,\ r_{n+1}=(T^{\prime},z^{\prime})\Rightarrow T<T^{\prime}.\]
Corresponding Lean step
  have hzeroevent (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ)
      (a : ℝ≥0 × (E × E)) (ha : record y xRef z₀ e n = Sum.inl a)
      (he : e n = 0) :
      record y xRef z₀ e (n + 1) = Sum.inl (a.1, S xRef a.2) := by
    rw [hrecstep, ha]
    simp only [next, he, hτzero, WithTop.zero_ne_top, ↓reduceIte,
      hzeroval, add_zero, NNReal.coe_zero, hΦzero]
  have hstrictevent (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ)
      (a : ℝ≥0 × (E × E)) (ha : record y xRef z₀ e n = Sum.inl a)
      (b : ℝ≥0 × (E × E)) (he : 0 < e n)
      (hb : record y xRef z₀ e (n + 1) = Sum.inl b) : a.1 < b.1 := by
    have ht : τ y xRef a.2 (e n) ≠ ⊤ := by
      intro ht
      have hs := (hbranches y xRef z₀ e n a ha).1.mpr ht
      rw [hb] at hs
      cases hs
    have hq : 0 < (τ y xRef a.2 (e n)).untopD 0 := by
      have hp := hτpositive y xRef a.2 (e n) he
      induction hτ : τ y xRef a.2 (e n) using WithTop.recTopCoe with
      | top => exact False.elim (ht hτ)
      | coe q => simpa only [hτ, hfiniteval, ← WithTop.coe_zero,
          WithTop.coe_lt_coe] using hp
    have hupdate := (hbranches y xRef z₀ e n a ha).2 ht
    rw [hb] at hupdate
    have heq := Sum.inl.inj hupdate
    have hbtime := congrArg Prod.fst heq
    rw [hbtime]
    exact lt_add_of_pos_right _ hq
  exact ⟨hrec0, fun y xRef z₀ e n =>
    ⟨hrecstep y xRef z₀ e n, hbranches y xRef z₀ e n⟩,
    hnextmeas, hrecordmeas, htimemeas,
    fun y xRef z₀ e => ⟨rfl, hmono y xRef z₀ e⟩, hstopped, harcs,
    fun y xRef z₀ e => ⟨hC0 y xRef z₀, hincrement y xRef z₀ e,
      hzerocap y xRef z₀ e⟩,
    fun y xRef z₀ e n a ha => ⟨hzeroevent y xRef z₀ e n a ha,
      hstrictevent y xRef z₀ e n a ha⟩⟩

Exact contiguous compiled public BODY. The eleven literal definitions and preceding facts remain in scope. All stochastic nonaccumulation and global-process consumers remain separate.

Lean verification

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

Lean proof · actual_fixed_reference_finite_jump_recursion

Reuse actual flow, bounce and first-clock laws; Identify the literal finite and stopped recursion branches; Prove joint Borel measurability of one actual successor; Prove joint Borel finite record and event-time maps; Carry the original energy through every active finite index; Prove nondecreasing event times and stopped absorption; Use the original energy for every outgoing arc and cap; Derive the uniform extended waiting increment; Handle zero original cap with a positive threshold; Keep zero thresholds and strict positive finite growth distinct

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_fixed_reference_finite_jump_recursion
    {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_fixed_reference_finite_jump_recursion_statement hα hαβ hV hH hη hβη := by
  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 H : E → E → (E × E) → ℝ := fun y xRef z =>
    (η⁻¹ * ‖z.1 - c y xRef‖ ^ 2 + ‖z.2‖ ^ 2) / 2
  let C : E → E → (E × E) → ℝ := fun y xRef z =>
    Real.sqrt η * (β : ℝ) * Real.sqrt (2 * H y xRef z) *
      (Real.sqrt (2 * η * H y xRef z) + ‖c y xRef - 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 eventTime : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ → WithTop ℝ≥0 :=
    fun y xRef z₀ e n => (record y xRef z₀ e n).elim
      (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
  change
  (∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0,
    record y xRef z₀ e 0 = Sum.inl (0, z₀)) ∧
  (∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n : ℕ,
    record y xRef z₀ e (n + 1) = next y xRef (e n) (record y xRef z₀ e n) ∧
    (∀ a : ℝ≥0 × (E × E), record y xRef z₀ e n = Sum.inl a →
      (record y xRef z₀ e (n + 1) = Sum.inr () ↔ τ y xRef a.2 (e n) = ⊤) ∧
      (τ y xRef a.2 (e n) ≠ ⊤ → record y xRef z₀ e (n + 1) =
        Sum.inl (a.1 + (τ y xRef a.2 (e n)).untopD 0,
          S xRef (Φ y xRef (((τ y xRef a.2 (e n)).untopD 0 : ℝ≥0) : ℝ) a.2))))) ∧
  Measurable (fun a : (E × E) × ℝ≥0 × ((ℝ≥0 × (E × E)) ⊕ Unit) =>
    next a.1.1 a.1.2 a.2.1 a.2.2) ∧
  (∀ n : ℕ, Measurable (fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
    record a.1.1 a.1.2 a.2.1 a.2.2 n)) ∧
  (∀ n : ℕ, Measurable (fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
    eventTime a.1.1 a.1.2 a.2.1 a.2.2 n)) ∧
  (∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0,
    eventTime y xRef z₀ e 0 = 0 ∧ Monotone (eventTime y xRef z₀ e)) ∧
  (∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n k : ℕ,
    record y xRef z₀ e n = Sum.inr () →
      record y xRef z₀ e (n + k) = Sum.inr ()) ∧
  (∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n : ℕ,
    ∀ a : ℝ≥0 × (E × E), record y xRef z₀ e n = Sum.inl a →
      H y xRef a.2 = H y xRef z₀ ∧
      ∀ t : ℝ≥0, (t : WithTop ℝ≥0) < τ y xRef a.2 (e n) →
        H y xRef (Φ y xRef (t : ℝ) a.2) = H y xRef z₀ ∧
        0 ≤ rate xRef (Φ y xRef (t : ℝ) a.2) ∧
        rate xRef (Φ y xRef (t : ℝ) a.2) ≤ C y xRef z₀) ∧
  (∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0,
    0 ≤ C y xRef z₀ ∧
    (0 < C y xRef z₀ → ∀ n : ℕ,
      eventTime y xRef z₀ e n +
        (Real.toNNReal ((e n : ℝ) / C y xRef z₀) : WithTop ℝ≥0) ≤
      eventTime y xRef z₀ e (n + 1)) ∧
    (C y xRef z₀ = 0 → ∀ n : ℕ, ∀ a : ℝ≥0 × (E × E),
      record y xRef z₀ e n = Sum.inl a → 0 < e n →
        record y xRef z₀ e (n + 1) = Sum.inr ())) ∧
  (∀ y xRef : E, ∀ z₀ : E × E, ∀ e : ℕ → ℝ≥0, ∀ n : ℕ,
    ∀ a : ℝ≥0 × (E × E), record y xRef z₀ e n = Sum.inl a →
      (e n = 0 → record y xRef z₀ e (n + 1) = Sum.inl (a.1, S xRef a.2)) ∧
      (∀ b : ℝ≥0 × (E × E), 0 < e n →
        record y xRef z₀ e (n + 1) = Sum.inl b → a.1 < b.1))

  have hf := ActualHarmonicFlow.actual_harmonic_flow_laws hα hαβ hV hH hη hβη
  have hb := ActualBounceRate.actual_bounce_rate_energy_laws hα hαβ hV hH hη hβη
  have hk := ActualHazardClock.actual_integrated_hazard_clock_laws hα hαβ hV hH hη hβη
  have hΦmeas : Measurable (fun a : (E × E) × ℝ × (E × E) =>
      Φ a.1.1 a.1.2 a.2.1 a.2.2) := hf.2.1
  have hΦzero (y xRef : E) (z : E × E) : Φ y xRef 0 z = z := hf.2.2.1 y xRef z
  have hΦH (y xRef : E) (t : ℝ) (z : E × E) :
      H y xRef (Φ y xRef t z) = H y xRef z := hf.2.2.2.2.2.2.2.1 y xRef t z
  have hSmeas : Measurable (fun a : E × (E × E) => S a.1 a.2) := hb.1
  have hSH (y xRef : E) (z : E × E) : H y xRef (S xRef z) = H y xRef z :=
    hb.2.2.2.2.2.2.1 y xRef z
  have hrate0 (xRef : E) (z : E × E) : 0 ≤ rate xRef z :=
    (hb.2.2.2.2.2.2.2.1 xRef z).1
  have hratecap (y xRef : E) (z₀ z : E × E) (hz : H y xRef z = H y xRef z₀) :
      rate xRef z ≤ C y xRef z₀ :=
    ((hb.2.2.2.2.2.2.2.2.2 y xRef z₀).2 z hz).2.2
  have hτpositive (y xRef : E) (z : E × E) (e : ℝ≥0) :
      0 < e → (0 : WithTop ℝ≥0) < τ y xRef z e :=
    (hk.2.2.2.2.2.1 y xRef z e).2.2.1
  have hτzero (y xRef : E) (z : E × E) : τ y xRef z 0 = 0 :=
    (hk.2.2.2.2.2.1 y xRef z 0).2.2.2
  have hτmeas : Measurable (fun a : (E × E) × (E × E) × ℝ≥0 =>
      τ a.1.1 a.1.2 a.2.1 a.2.2) := hk.2.2.2.2.2.2.1
  have hC0 (y xRef : E) (z : E × E) : 0 ≤ C y xRef z :=
    (hk.2.2.2.2.2.2.2.2.1 y xRef z).1
  have hwait (y xRef : E) (z : E × E) (e : ℝ≥0) :
      (0 < C y xRef z →
        (Real.toNNReal ((e : ℝ) / C y xRef z) : WithTop ℝ≥0) ≤ τ y xRef z e) ∧
      (C y xRef z = 0 → 0 < e → τ y xRef z e = ⊤) :=
    hk.2.2.2.2.2.2.2.2.2 y xRef z e
  have hfiniteval (q : ℝ≥0) : (q : WithTop ℝ≥0).untopD 0 = q := rfl
  have hzeroval : (0 : WithTop ℝ≥0).untopD 0 = 0 := rfl
  have hrec0 (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) :
      record y xRef z₀ e 0 = Sum.inl (0, z₀) := rfl
  have hrecstep (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ) :
      record y xRef z₀ e (n + 1) = next y xRef (e n) (record y xRef z₀ e n) := rfl
  have hbranches (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ)
      (a : ℝ≥0 × (E × E)) (ha : record y xRef z₀ e n = Sum.inl a) :
      (record y xRef z₀ e (n + 1) = Sum.inr () ↔ τ y xRef a.2 (e n) = ⊤) ∧
      (τ y xRef a.2 (e n) ≠ ⊤ → record y xRef z₀ e (n + 1) =
        Sum.inl (a.1 + (τ y xRef a.2 (e n)).untopD 0,
          S xRef (Φ y xRef (((τ y xRef a.2 (e n)).untopD 0 : ℝ≥0) : ℝ) a.2))) := by
    rw [hrecstep, ha]
    dsimp only [next]
    split_ifs with ht <;> simp [ht]
  have hnextmeas : Measurable
      (fun a : (E × E) × ℝ≥0 × ((ℝ≥0 × (E × E)) ⊕ Unit) =>
        next a.1.1 a.1.2 a.2.1 a.2.2) := by
    let g : ((E × E) × ℝ≥0) × (ℝ≥0 × (E × E)) →
        ((ℝ≥0 × (E × E)) ⊕ Unit) := fun a =>
      if τ a.1.1.1 a.1.1.2 a.2.2 a.1.2 = ⊤ then Sum.inr () else
        Sum.inl (a.2.1 + (τ a.1.1.1 a.1.1.2 a.2.2 a.1.2).untopD 0,
          S a.1.1.2 (Φ a.1.1.1 a.1.1.2
            (((τ a.1.1.1 a.1.1.2 a.2.2 a.1.2).untopD 0 : ℝ≥0) : ℝ) a.2.2))
    have hparams : Measurable
        (fun a : ((E × E) × ℝ≥0) × (ℝ≥0 × (E × E)) =>
          (a.1.1, a.2.2, a.1.2)) :=
      measurable_fst.fst.prodMk (measurable_snd.snd.prodMk measurable_fst.snd)
    have ht0 := hτmeas.comp hparams
    have ht : Measurable (fun a : ((E × E) × ℝ≥0) × (ℝ≥0 × (E × E)) =>
        τ a.1.1.1 a.1.1.2 a.2.2 a.1.2) := ht0
    have hq := ht.untopD (0 : ℝ≥0)
    have hp := hΦmeas.comp (measurable_fst.fst.prodMk
      ((measurable_coe_nnreal_real.comp hq).prodMk measurable_snd.snd))
    have hs := hSmeas.comp (measurable_fst.fst.snd.prodMk hp)
    have hg : Measurable g := measurable_const.ite
      (measurableSet_eq_fun ht measurable_const)
      (measurable_inl.comp ((measurable_snd.fst.add hq).prodMk hs))
    have hsum := hg.sumElim
      (show Measurable (fun _ : ((E × E) × ℝ≥0) × Unit =>
        (Sum.inr () : (ℝ≥0 × (E × E)) ⊕ Unit)) from measurable_const)
    have hm := hsum.comp ((MeasurableEquiv.prodSumDistrib
      ((E × E) × ℝ≥0) (ℝ≥0 × (E × E)) Unit).measurable.comp
      ((measurable_fst.prodMk measurable_snd.fst).prodMk measurable_snd.snd))
    convert hm using 1
    funext a
    rcases a with ⟨⟨y, xRef⟩, e, r⟩
    cases r <;> rfl
  have hrecordmeas (n : ℕ) : Measurable
      (fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
        record a.1.1 a.1.2 a.2.1 a.2.2 n) := by
    induction n with
    | zero => exact measurable_inl.comp (measurable_const.prodMk measurable_snd.fst)
    | succ n ih =>
      exact hnextmeas.comp (measurable_fst.prodMk
        (((measurable_pi_apply n).comp measurable_snd.snd).prodMk ih))
  have htimemeas (n : ℕ) : Measurable
      (fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
        eventTime a.1.1 a.1.2 a.2.1 a.2.2 n) :=
    ((WithTop.measurable_coe.comp measurable_fst).sumElim measurable_const).comp
      (hrecordmeas n)
  have henergy (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ)
      (a : ℝ≥0 × (E × E)) (ha : record y xRef z₀ e n = Sum.inl a) :
      H y xRef a.2 = H y xRef z₀ := by
    induction n generalizing a with
    | zero =>
      have heq : (0, z₀) = a := Sum.inl.inj ha
      subst a
      rfl
    | succ n ih =>
      rw [hrecstep] at ha
      cases hr : record y xRef z₀ e n with
      | inr u => simp [hr, next] at ha
      | inl b =>
        rw [hr] at ha
        dsimp only [next] at ha
        by_cases ht : τ y xRef b.2 (e n) = ⊤
        · simp only [if_pos ht] at ha
          cases ha
        · rw [if_neg ht] at ha
          have heq := Sum.inl.inj ha
          rw [← heq]
          exact (hSH y xRef _).trans ((hΦH y xRef _ _).trans (ih b hr))
  have hmono (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) :
      Monotone (eventTime y xRef z₀ e) := by
    apply monotone_nat_of_le_succ
    intro n
    dsimp only [eventTime]
    rw [hrecstep]
    cases hr : record y xRef z₀ e n with
    | inr u => simp [next]
    | inl a =>
      dsimp only [next]
      split_ifs with ht
      · exact le_top
      · exact WithTop.coe_le_coe.mpr (le_add_of_nonneg_right zero_le)
  have hstopped (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n k : ℕ)
      (hn : record y xRef z₀ e n = Sum.inr ()) :
      record y xRef z₀ e (n + k) = Sum.inr () := by
    induction k with
    | zero => simpa using hn
    | succ k ih => simpa only [Nat.add_succ, hrecstep, ih, next]
  have harcs (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ)
      (a : ℝ≥0 × (E × E)) (ha : record y xRef z₀ e n = Sum.inl a) :
      H y xRef a.2 = H y xRef z₀ ∧
      ∀ t : ℝ≥0, (t : WithTop ℝ≥0) < τ y xRef a.2 (e n) →
        H y xRef (Φ y xRef (t : ℝ) a.2) = H y xRef z₀ ∧
        0 ≤ rate xRef (Φ y xRef (t : ℝ) a.2) ∧
        rate xRef (Φ y xRef (t : ℝ) a.2) ≤ C y xRef z₀ := by
    have hEa := henergy y xRef z₀ e n a ha
    refine ⟨hEa, fun t _ => ?_⟩
    have hEt := (hΦH y xRef t a.2).trans hEa
    exact ⟨hEt, hrate0 xRef _, hratecap y xRef z₀ _ hEt⟩
  have hcap_eq (y xRef : E) (z₀ z : E × E) (hz : H y xRef z = H y xRef z₀) :
      C y xRef z = C y xRef z₀ := by simp only [C, hz]
  have hincrement (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0)
      (hC : 0 < C y xRef z₀) (n : ℕ) :
      eventTime y xRef z₀ e n +
        (Real.toNNReal ((e n : ℝ) / C y xRef z₀) : WithTop ℝ≥0) ≤
      eventTime y xRef z₀ e (n + 1) := by
    cases hr : record y xRef z₀ e n with
    | inr u =>
      dsimp only [eventTime]
      rw [hrecstep, hr]
      change (⊤ : WithTop ℝ≥0) + _ ≤ ⊤
      exact le_top
    | inl a =>
      have hCa := hcap_eq y xRef z₀ a.2 (henergy y xRef z₀ e n a hr)
      have hw := (hwait y xRef a.2 (e n)).1 (by simpa only [hCa] using hC)
      rw [hCa] at hw
      dsimp only [eventTime]
      rw [hrecstep, hr]
      dsimp only [next]
      split_ifs with ht
      · exact le_top
      · have hq : (((τ y xRef a.2 (e n)).untopD 0 : ℝ≥0) : WithTop ℝ≥0) =
            τ y xRef a.2 (e n) := by
          induction hτ : τ y xRef a.2 (e n) using WithTop.recTopCoe with
          | top => exact False.elim (ht hτ)
          | coe q => exact congrArg (fun q : ℝ≥0 => (q : WithTop ℝ≥0)) (hfiniteval q)
        change (a.1 : WithTop ℝ≥0) + _ ≤
          ((a.1 + (τ y xRef a.2 (e n)).untopD 0 : ℝ≥0) : WithTop ℝ≥0)
        rw [WithTop.coe_add, hq]
        exact add_le_add le_rfl hw
  have hzerocap (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0)
      (hC : C y xRef z₀ = 0) (n : ℕ) (a : ℝ≥0 × (E × E))
      (ha : record y xRef z₀ e n = Sum.inl a) (he : 0 < e n) :
      record y xRef z₀ e (n + 1) = Sum.inr () := by
    apply (hbranches y xRef z₀ e n a ha).1.mpr
    apply (hwait y xRef a.2 (e n)).2 _ he
    exact (hcap_eq y xRef z₀ a.2 (henergy y xRef z₀ e n a ha)).trans hC
  have hzeroevent (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ)
      (a : ℝ≥0 × (E × E)) (ha : record y xRef z₀ e n = Sum.inl a)
      (he : e n = 0) :
      record y xRef z₀ e (n + 1) = Sum.inl (a.1, S xRef a.2) := by
    rw [hrecstep, ha]
    simp only [next, he, hτzero, WithTop.zero_ne_top, ↓reduceIte,
      hzeroval, add_zero, NNReal.coe_zero, hΦzero]
  have hstrictevent (y xRef : E) (z₀ : E × E) (e : ℕ → ℝ≥0) (n : ℕ)
      (a : ℝ≥0 × (E × E)) (ha : record y xRef z₀ e n = Sum.inl a)
      (b : ℝ≥0 × (E × E)) (he : 0 < e n)
      (hb : record y xRef z₀ e (n + 1) = Sum.inl b) : a.1 < b.1 := by
    have ht : τ y xRef a.2 (e n) ≠ ⊤ := by
      intro ht
      have hs := (hbranches y xRef z₀ e n a ha).1.mpr ht
      rw [hb] at hs
      cases hs
    have hq : 0 < (τ y xRef a.2 (e n)).untopD 0 := by
      have hp := hτpositive y xRef a.2 (e n) he
      induction hτ : τ y xRef a.2 (e n) using WithTop.recTopCoe with
      | top => exact False.elim (ht hτ)
      | coe q => simpa only [hτ, hfiniteval, ← WithTop.coe_zero,
          WithTop.coe_lt_coe] using hp
    have hupdate := (hbranches y xRef z₀ e n a ha).2 ht
    rw [hb] at hupdate
    have heq := Sum.inl.inj hupdate
    have hbtime := congrArg Prod.fst heq
    rw [hbtime]
    exact lt_add_of_pos_right _ hq
  exact ⟨hrec0, fun y xRef z₀ e n =>
    ⟨hrecstep y xRef z₀ e n, hbranches y xRef z₀ e n⟩,
    hnextmeas, hrecordmeas, htimemeas,
    fun y xRef z₀ e => ⟨rfl, hmono y xRef z₀ e⟩, hstopped, harcs,
    fun y xRef z₀ e => ⟨hC0 y xRef z₀, hincrement y xRef z₀ e,
      hzerocap y xRef z₀ e⟩,
    fun y xRef z₀ e n a ha => ⟨hzeroevent y xRef z₀ e n a ha,
      hstrictevent y xRef z₀ e n a ha⟩⟩

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteJumpRecursion

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
The original C² strongly convex/smooth potential and η>0, βη≤1.E is a finite-dimensional real inner-product space with its compatible norm and Borel measurable structure; rank zero is allowed. Products and the threshold sequence space carry product measurable structures; the record space carries the native disjoint-union structure. V:E→ℝ is C² on all E. Nonnegative α,β satisfy 0<α≤β, and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v∈E. η>0 and βη≤1. These and the preceding potential conditions are the six original analytic callers. The actual flow, bounce, clock, measurable record maps, conserved energy, cap and increment are produced within the proof, never supplied as callers.sameThe six original analytic callers are unchanged; Borel finite-Hilbert typing includes rank zero.
AppendixA1(A2) recursive actual jump times/phases and Ex8 original-energy uniform waiting increment.Let E be a finite-dimensional real inner-product Borel space, including rank zero. Let V:E→ℝ be C², let α,β≥0 satisfy 0<α≤β and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v, and let η>0 with βη≤1. Fix arbitrary y,xRef∈E, z₀=(x₀,p₀)∈E×E and an arbitrary sequence e_n≥0. Define c=y−η∇V(xRef); Φ_t(x,p)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p); S(x,p)=(x,p−(2⟨p,∇V(x)−∇V(xRef)⟩/‖∇V(x)−∇V(xRef)‖²)(∇V(x)−∇V(xRef))), using total real division, so a zero normal gives the identity; λ(x,p)=√η max(0,⟨p,∇V(x)−∇V(xRef)⟩); H(x,p)=(η⁻¹‖x−c‖²+‖p‖²)/2; C(z)=√η β√(2H(z))(√(2ηH(z))+‖c−xRef‖); Λ_z(t)=∫₀ᵗλ(Φ_s z)ds for t≥0; and τ_z(e)=inf{t≥0:Λ_z(t)≥e}∈[0,∞], with inf∅=∞. Records are the disjoint union of finite active pairs (T,z) and a phase-free stopped symbol †. Define next_e(†)=†; for an active (T,z), put next_e(T,z)=† if τ_z(e)=∞, otherwise next_e(T,z)=(T+τ_z(e),S(Φ_(τ_z(e))z)). Define r₀=(0,z₀), r_(n+1)=next_(e_n)(r_n), and T_n as the finite time coordinate when r_n is active and ∞ when it is stopped. Then: (1) the initial record is exactly (0,z₀); (2) the successor identity holds, and an active record stops at the next index iff its actual clock is infinite, otherwise it has exactly the displayed active successor; (3) next is jointly Borel in y,xRef,e,r; (4) for each n, r_n is jointly Borel in y,xRef,z₀ and the whole threshold sequence; (5) T_n is jointly Borel in the same inputs; (6) T₀=0 and T_n is nondecreasing; (7) a stopped record at n remains stopped at every n+k; (8) if r_n=(T,z), then H(z)=H(z₀), and for every t≥0 with t<τ_z(e_n), H(Φ_tz)=H(z₀) and 0≤λ(Φ_tz)≤C(z₀); (9) C₀=C(z₀)≥0, C₀>0 implies T_n+max(e_n/C₀,0)≤T_(n+1) for every n, including stopped records, while C₀=0 and an active record with e_n>0 imply that the next record is stopped; (10) for an active r_n=(T,z), e_n=0 gives r_(n+1)=(T,S(z)), while e_n>0 and a finite active successor (T′,z′) imply T<T′. All statements concern the actual finite indexed recursion with fixed y,xRef. No iid realization, almost-sure nonaccumulation, single physical-time phase in the presence of zero thresholds, all-time process, Markov law, invariance, terminal sampler or cost theorem is asserted.source-implicitNative finite-active/stopped records implement the finite deterministic skeleton. Borel maps, original-energy induction and actual cap equality are proved internally. Arbitrary zero thresholds extend the source positive almost-sure thresholds and retain their separate same-time behavior.
iid exponential sequence, SLLN/nonaccumulation, all-time PDMP, Markov/invariance, actual terminal sampler, errors and expected costs.Only actual fixed-reference finite stopped recursion with joint Borel/energy/cap/wait laws. No iid exponential product realization, SLLN/nonaccumulation, all-time process/cadlag/Markov/invariance, Algorithm1 returned position kernel, hypocoercivity/main/error/expected costs/actual-input composition, full Exposition/PURIFIED/main/live/whole-paper/Goal credit. Arbitrary zero thresholds may repeat times; no physical-time phase at infinity is assigned. Focused compilation is local evidence. Independent whole-proof/source/decoder review, serialized aggregate and reader delivery remain separate.unresolvedThese require additional stochastic construction and source arguments. Finite recursion alone is not the complete algorithm or paper theorem.

Only actual fixed-reference finite stopped recursion with joint Borel/energy/cap/wait laws. No iid exponential product realization, SLLN/nonaccumulation, all-time process/cadlag/Markov/invariance, Algorithm1 returned position kernel, hypocoercivity/main/error/expected costs/actual-input composition, full Exposition/PURIFIED/main/live/whole-paper/Goal credit. Arbitrary zero thresholds may repeat times; no physical-time phase at infinity is assigned. Focused compilation is local evidence. Independent whole-proof/source/decoder review, serialized aggregate and reader delivery remain separate.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • objects: phase-free-finite-stopped-representation: Stop the source recursion at an empty hit set and do not define a phase at∞. A Sum.inr Unit stopped tag is absorbing and its event time is∞; the finite successor is guarded before untopD0/Φ/S. — L47–60,136–149,229–237,319–324. This is a faithful finite representation plus inert post-stop indexing, not an invented phase fallback.
  • quantifiers: declared-deterministic-zero-threshold-extension: E_(n+1) are independent Exp(1), strictly positive a.s. in the future stochastic construction. Arbitrary e(n)≥0 is supplied as deterministic data; zero gives a same-time indexed bounce. — The attribution explicitly names the ASTIS extension and reserves iid/nonaccumulation. L99–101,374–401 preserve the independently frozen zero-time limitation. No source repair is being accepted.
  • domains: coordinate-free-Euclidean-Borel-formulation: Finite-dimensional Euclidean R^d, with no source-added higher regularity or rank-positive condition. Finite-dimensional real inner-product Borel E, including rank zero. — L17–18,104–106 and the five typing instances. The argument is coordinate invariant and all zero-dimensional cases remain defined.
  • conclusion: Borel-recursion-and-extended-wait-bookkeeping: Source A.2 is stated by recursion and Ex8 is stated for finite waits. The actual successor/record/time maps are jointly Borel, and the increment extends to stopped∞ indices in the standard extended order. — L238–283 and338–366; finite hit measurability is derived by the consumed concrete clock theorem. Extended∞ inequalities add no finite-wait or process premise.

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
  • Only actual fixed-reference finite stopped recursion with joint Borel/energy/cap/wait laws. No iid exponential product realization, SLLN/nonaccumulation, all-time process/cadlag/Markov/invariance, Algorithm1 returned position kernel, hypocoercivity/main/error/expected costs/actual-input composition, full Exposition/PURIFIED/main/live/whole-paper/Goal credit. Arbitrary zero thresholds may repeat times; no physical-time phase at infinity is assigned. Focused compilation is local evidence. Independent whole-proof/source/decoder review, serialized aggregate and reader delivery remain separate.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • measurableSet_eq_fun
  • Measurable.ite
  • Measurable.sumElim
  • MeasurableEquiv.prodSumDistrib
  • WithTop.measurable_untopD
  • WithTop.measurable_coe
  • measurable_pi_apply
  • monotone_nat_of_le_succ
  • WithTop.coe_add
  • WithTop.coe_le_coe
  • WithTop.coe_lt_coe
  • WithTop.recTopCoe

Mathematical sources

  • arXiv2609.06905v1 AppendixA.1 equation(A.2), Ex4-8, Algorithm1/Proposition3.1; deterministic finite skeleton feeding future iid/SLLN nonaccumulation. — Only actual fixed-reference finite stopped recursion with joint Borel/energy/cap/wait laws. No iid exponential product realization, SLLN/nonaccumulation, all-time process/cadlag/Markov/invariance, Algorithm1 returned position kernel, hypocoercivity/main/error/expected costs/actual-input composition, full Exposition/PURIFIED/main/live/whole-paper/Goal credit. Arbitrary zero thresholds may repeat times; no physical-time phase at infinity is assigned. Focused compilation is local evidence. Independent whole-proof/source/decoder review, serialized aggregate and reader delivery remain separate.

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 jointly Borel finite stopped recursion and original-energy uniform increment
  • TODO — not closed by these contributions iid nonaccumulation/global process and full paper/cost/composition