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

Actual PBPS finite physical-time interval coverage

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhysicalTimeCover.actual_fixed_reference_physical_time_cover · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be any finite-dimensional real inner-product space, including dimension zero, with its Borel measurable structure. Let V:E→ℝ be C². Let α,β be nonnegative reals and η a real number satisfying α>0, α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, η>0, and βη≤1. Fix any y,xRef∈E and initial phase z0=(x0,p0)∈E×E. Set c=y−η∇V(xRef). For z=(x,p), define the actual harmonic flow Φ_t(z)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p), reflection S(z)=(x,p−[2〈p,g(x)〉/‖g(x)‖²]g(x)), residual g(x)=∇V(x)−∇V(xRef), and rate λ(z)=√η max{0,〈p,g(x)〉}. The reflection uses total real division, hence is the identity when g(x)=0. Define Λ(z,t)=∫_0^t λ(Φ_s(z)) ds for finite t≥0 and τ(z,e)=inf{t≥0:Λ(z,t)≥e}, with inf empty=∞. Let P be the actual countable product of rate-one exponential Borel measures on Ω=ℝ^ℕ; let ε_k(sample)=max{sample_k,0} viewed as a nonnegative real. Define active records (T,z) and an absorbing stopped record carrying no phase. Initialize record0=(0,z0). At index k, a stopped record stays stopped; an active record (T,z) becomes stopped if τ(z,ε_k)=∞ and otherwise becomes (T+τ(z,ε_k), S(Φ_{τ(z,ε_k)}(z))). Its event time T_k is the finite time component if active and ∞ if stopped. Then for these fixed y,xRef,z0, for P-almost every sample, simultaneously: (i) for every finite nonnegative physical time t there exists exactly one n∈ℕ with T_n≤t<T_(n+1); (ii) for every such t and every index n satisfying those inequalities, there exists exactly one finite live record a=(s,z) such that record_n=inl(a), s≤t, and t−s<τ(z,ε_n), using nonnegative real subtraction and extended-valued comparison. In particular no stopped record supplies a phase, and when the next wait is infinite the last live record continues to cover every later finite physical time. Initialization index0 is retained and ε_n is source E_(n+1). Half-open intervals fix event-endpoint ownership; zero-length intervals are empty and strict positive waits are not an extra premise. This is the ASTIS interval/live-record/elapsed adapter needed by Appendix A.1's between-jump formula. It does not construct a global interpolated process, assert index(t=0)=0, or prove measurability, path regularity, full process uniqueness, Markov/invariance or costs.

\[P\text{-a.s.}:\quad\forall t\in[0,\infty),\quad\exists!n\in\mathbb N:\ T_n\le t<T_{n+1};\quad\operatorname{record}_n=(s,z),\quad s\le t,\quad t-s<\tau(z,\varepsilon_n).\]
Lean statement · actual_fixed_reference_physical_time_cover

Let E be any finite-dimensional real inner-product space, including dimension zero, with its Borel measurable structure. Let V:E→ℝ be C². Let α,β be nonnegative reals and η a real number satisfying α>0, α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, η>0, and βη≤1. Fix any y,xRef∈E and initial phase z0=(x0,p0)∈E×E. Set c=y−η∇V(xRef). For z=(x,p), define the actual harmonic flow Φ_t(z)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p), reflection S(z)=(x,p−[2〈p,g(x)〉/‖g(x)‖²]g(x)), residual g(x)=∇V(x)−∇V(xRef), and rate λ(z)=√η max{0,〈p,g(x)〉}. The reflection uses total real division, hence is the identity when g(x)=0. Define Λ(z,t)=∫_0^t λ(Φ_s(z)) ds for finite t≥0 and τ(z,e)=inf{t≥0:Λ(z,t)≥e}, with inf empty=∞. Let P be the actual countable product of rate-one exponential Borel measures on Ω=ℝ^ℕ; let ε_k(sample)=max{sample_k,0} viewed as a nonnegative real. Define active records (T,z) and an absorbing stopped record carrying no phase. Initialize record0=(0,z0). At index k, a stopped record stays stopped; an active record (T,z) becomes stopped if τ(z,ε_k)=∞ and otherwise becomes (T+τ(z,ε_k), S(Φ_{τ(z,ε_k)}(z))). Its event time T_k is the finite time component if active and ∞ if stopped. Then for these fixed y,xRef,z0, for P-almost every sample, simultaneously: (i) for every finite nonnegative physical time t there exists exactly one n∈ℕ with T_n≤t<T_(n+1); (ii) for every such t and every index n satisfying those inequalities, there exists exactly one finite live record a=(s,z) such that record_n=inl(a), s≤t, and t−s<τ(z,ε_n), using nonnegative real subtraction and extended-valued comparison. In particular no stopped record supplies a phase, and when the next wait is infinite the last live record continues to cover every later finite physical time. Initialization index0 is retained and ε_n is source E_(n+1). Half-open intervals fix event-endpoint ownership; zero-length intervals are empty and strict positive waits are not an extra premise. This is the ASTIS interval/live-record/elapsed adapter needed by Appendix A.1's between-jump formula. It does not construct a global interpolated process, assert index(t=0)=0, or prove measurability, path regularity, full process uniqueness, Markov/invariance or costs.

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_physical_time_cover
    {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_physical_time_cover_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_fixed_reference_physical_time_cover_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_physical_time_cover_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 P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
    let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun sample k => Real.toNNReal (sample k)
    let c : E → E → E := fun y xRef => y - η • gradient V xRef
    let Φ : E → E → ℝ → (E × E) → (E × E) := fun y xRef t z =>
      (c y xRef + Real.cos t • (z.1 - c y xRef) +
          (Real.sqrt η * Real.sin t) • z.2,
       (-Real.sin t / Real.sqrt η) • (z.1 - c y xRef) + Real.cos t • z.2)
    let S : E → (E × E) → (E × E) := fun xRef z =>
      (z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
        ‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
    let rate : E → (E × E) → ℝ := fun xRef z =>
      Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V xRef))
    let Λ : E → E → (E × E) → ℝ≥0 → ℝ := fun y xRef z t =>
      ∫ s in (0 : ℝ)..(t : ℝ), rate xRef (Φ y xRef s z)
    let τ : E → E → (E × E) → ℝ≥0 → WithTop ℝ≥0 := fun y xRef z e =>
      MeasureTheory.hittingAfter
        (fun t : ℝ≥0 => fun a : (E × E) × (E × E) × ℝ≥0 =>
          Λ a.1.1 a.1.2 a.2.1 t - (a.2.2 : ℝ))
        (Set.Ici (0 : ℝ)) 0 ((y, xRef), z, e)
    let next : E → E → ℝ≥0 → ((ℝ≥0 × (E × E)) ⊕ Unit) →
        ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef e r =>
      match r with
      | Sum.inr _ => Sum.inr ()
      | Sum.inl a =>
        if τ y xRef a.2 e = ⊤ then Sum.inr () else
          Sum.inl (a.1 + (τ y xRef a.2 e).untopD 0,
            S xRef (Φ y xRef (((τ y xRef a.2 e).untopD 0 : ℝ≥0) : ℝ) a.2))
    let record : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ →
        ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef z₀ e n =>
      Nat.rec (Sum.inl (0, z₀)) (fun k r => next y xRef (e k) r) n
    let 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, ∀ᵐ sample ∂P,
      (∀ t : ℝ≥0, ∃! n : ℕ,
        eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) ∧
        (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1)) ∧
      (∀ t : ℝ≥0, ∀ n : ℕ,
        eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) →
        (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) →
        ∃! a : ℝ≥0 × (E × E),
          record y xRef z₀ (ε sample) n = Sum.inl a ∧ a.1 ≤ t ∧
          ((t - a.1 : ℝ≥0) : WithTop ℝ≥0) < τ y xRef a.2 (ε sample n))


set_option maxHeartbeats 800000 in

Exact module and namespace context

Proof roadmap

  1. 1Fix the actual source objects and finite-time target

    Keep the literal source flow, reflection, hazard, first hitting time and guarded finite-record recurrence. Use the canonical Exp1 product and total NNReal thresholds. The two conclusions concern the actual half-open clock interval and the actual stored live record with finite elapsed time.

  2. 2Reuse initialized monotone actual clocks on the common AE event

    The exact finite-recursion parent supplies initialization, monotonicity and guarded next-record updates. The actual nonaccumulation parent supplies finite-horizon escape on one AE event for each fixed parameter triple. No certificate is supplied as a new public assumption.

  3. 3Select the predecessor of the first clock crossing

    For each finite t choose the least k with t<T_k. Initialization gives k>0. Let n=k−1. Minimality gives T_n≤t, and n+1=k gives t<T_(n+1).

  4. 4Prove that the half-open interval index is unique

    If two indices m,n satisfy their half-open inequalities, m>n would imply T_(n+1)≤T_m≤t, contradicting t<T_(n+1). The opposite inequality is symmetric. Empty zero-length intervals cause no overlap, so no extra strict-wait premise is needed.

  5. 5Exclude stopped records at finite covering times

    A stopped record has eventTime=∞. Its lower interval inequality ∞≤t contradicts finiteness of t. Thus every covering record must be active.

  6. 6Recover the actual live record and its stored time

    For an active record a the exact eventTime eliminator gives T_n=a.time. The lower interval inequality gives a.time≤t. The record supplied in the conclusion is this actual record, not a chosen external state.

  7. 7Keep the last live arc when the next wait is infinite

    If the actual next waiting time is infinity, every finite NNReal elapsed offset is strictly less than it. Stopping the next jump does not erase the currently live state or invent a phase at infinity.

  8. 8Bound the elapsed offset for a finite next wait

    Write the actual finite wait as q. The existing guarded recurrence gives record_(n+1)=(a.time+q, bounce(flow(q,a.state))) and hence T_(n+1)=a.time+q. Therefore t<T_(n+1) and a.time≤t imply t−a.time<q. Subtraction is nonnegative and never evaluates an infinite elapsed duration.

  9. 9Prove uniqueness of the actual live record

    The record recursion is a function. Two live records at the same index have equal Sum.inl values, so injectivity gives equal time/state pairs. Assemble the interval and live-record conclusions on the common AE event.

Full assumptions and notation

All objects and hypotheses

  • E is finite-dimensional real inner-product with its Borel measurable structure; no positive-dimension restriction. V is C² and α,β≥0.
  • The six exact source conditions are α>0; α≤β; V∈C²; for all x,v, α‖v‖²≤D²V(x)[v,v]≤β‖v‖²; η>0; βη≤1. No third or higher derivative condition.
  • y,xRef,z0 are arbitrary deterministic parameters. P and ε are literal canonical definitions. No probability, iid, positivity, divergence, cap, energy, waiting-time or recurrence certificate is a public premise.
  • Threshold positivity and faithful clamp/raw equality hold simultaneously only almost surely. The all-finite-horizon conclusion is pathwise on the common good-input event for each fixed parameter triple; no uncountable intersection over triples is assumed.
  • Stopped records have eventTime=∞ and carry no phase. Every selected record is live with finite stored time and finite nonnegative elapsed offset. The next wait may be infinite; zero-length intervals are empty. No positive-wait, index, recurrence, nonaccumulation, measurable-selector or path certificate is a public premise.

Mathematical proof

1. Fix the actual source objects and finite-time target

Keep the literal source flow, reflection, hazard, first hitting time and guarded finite-record recurrence. Use the canonical Exp1 product and total NNReal thresholds. The two conclusions concern the actual half-open clock interval and the actual stored live record with finite elapsed time.

\[T_n=\operatorname{time}(\operatorname{record}_n),\quad T_n=\infty\text{ if stopped};\quad T_n\le t<T_{n+1}.\]
Corresponding Lean step
  classical
  let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
  let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun sample k => Real.toNNReal (sample k)
  let c : E → E → E := fun y xRef => y - η • gradient V xRef
  let Φ : E → E → ℝ → (E × E) → (E × E) := fun y xRef t z =>
    (c y xRef + Real.cos t • (z.1 - c y xRef) +
        (Real.sqrt η * Real.sin t) • z.2,
     (-Real.sin t / Real.sqrt η) • (z.1 - c y xRef) + Real.cos t • z.2)
  let S : E → (E × E) → (E × E) := fun xRef z =>
    (z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
      ‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
  let rate : E → (E × E) → ℝ := fun xRef z =>
    Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V xRef))
  let Λ : E → E → (E × E) → ℝ≥0 → ℝ := fun y xRef z t =>
    ∫ s in (0 : ℝ)..(t : ℝ), rate xRef (Φ y xRef s z)
  let τ : E → E → (E × E) → ℝ≥0 → WithTop ℝ≥0 := fun y xRef z e =>
    MeasureTheory.hittingAfter
      (fun t : ℝ≥0 => fun a : (E × E) × (E × E) × ℝ≥0 =>
        Λ a.1.1 a.1.2 a.2.1 t - (a.2.2 : ℝ))
      (Set.Ici (0 : ℝ)) 0 ((y, xRef), z, e)
  let next : E → E → ℝ≥0 → ((ℝ≥0 × (E × E)) ⊕ Unit) →
      ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef e r =>
    match r with
    | Sum.inr _ => Sum.inr ()
    | Sum.inl a =>
      if τ y xRef a.2 e = ⊤ then Sum.inr () else
        Sum.inl (a.1 + (τ y xRef a.2 e).untopD 0,
          S xRef (Φ y xRef (((τ y xRef a.2 e).untopD 0 : ℝ≥0) : ℝ) a.2))
  let record : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ →
      ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef z₀ e n =>
    Nat.rec (Sum.inl (0, z₀)) (fun k r => next y xRef (e k) r) n
  let 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, ∀ᵐ sample ∂P,
    (∀ t : ℝ≥0, ∃! n : ℕ,
      eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) ∧
      (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1)) ∧
    (∀ t : ℝ≥0, ∀ n : ℕ,
      eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) →
      (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) →
      ∃! a : ℝ≥0 × (E × E),
        record y xRef z₀ (ε sample) n = Sum.inl a ∧ a.1 ≤ t ∧
        ((t - a.1 : ℝ≥0) : WithTop ℝ≥0) < τ y xRef a.2 (ε sample n))

Exact contiguous compiled proof region; preceding local definitions and facts remain in scope.

2. Reuse initialized monotone actual clocks on the common AE event

The exact finite-recursion parent supplies initialization, monotonicity and guarded next-record updates. The actual nonaccumulation parent supplies finite-horizon escape on one AE event for each fixed parameter triple. No certificate is supplied as a new public assumption.

\[T_0=0,\quad T_n\le T_{n+1},\quad\forall t<\infty,\quad T_n>t\text{ eventually}.\]
Corresponding Lean step
  -- Exact deterministic initialization/monotonicity and guarded live-record updates.
  rcases ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursion
      hα hαβ hV hH hη hβη with
    ⟨_, hstep, _, _, _, htime, _, _, _, _⟩
  have hinput := ActualNonaccumulation.actual_fixed_reference_event_time_nonaccumulation
    hα hαβ hV hH hη hβη
  intro y xRef z₀
  filter_upwards [hinput y xRef z₀] with sample hgood
  have hzero : eventTime y xRef z₀ (ε sample) 0 = 0 :=
    (htime y xRef z₀ (ε sample)).1
  have hmono : Monotone (eventTime y xRef z₀ (ε sample)) :=
    (htime y xRef z₀ (ε sample)).2
  constructor

Exact contiguous compiled proof region; preceding local definitions and facts remain in scope.

3. Select the predecessor of the first clock crossing

For each finite t choose the least k with t<T_k. Initialization gives k>0. Let n=k−1. Minimality gives T_n≤t, and n+1=k gives t<T_(n+1).

\[k=\min\{j:t<T_j\}>0,\quad n=k-1,\quad T_n\le t<T_{n+1}.\]
Corresponding Lean step
  · -- The first clock strictly above t has an initialized finite predecessor.
    intro t
    obtain ⟨N, hN⟩ := eventually_atTop.mp (hgood.1 t)
    have hex : ∃ k : ℕ, (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) k :=
      ⟨N, hN N le_rfl⟩
    let k : ℕ := Nat.find hex
    have hk : (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) k :=
      Nat.find_spec hex
    have hkpos : 0 < k := by
      by_contra h
      have hk0 : k = 0 := Nat.eq_zero_of_not_pos h
      rw [hk0, hzero] at hk
      exact (not_lt_of_ge (show (0 : WithTop ℝ≥0) ≤ t from bot_le)) hk
    let n : ℕ := k - 1
    have hsucc : n + 1 = k := by dsimp [n]; omega
    have hlow : eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) := by
      apply le_of_not_gt
      exact Nat.find_min hex (by change k - 1 < k; omega)
    have hupp : (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) := by
      simpa only [hsucc] using hk
    refine ⟨n, ⟨hlow, hupp⟩, ?_⟩

Exact contiguous compiled proof region; preceding local definitions and facts remain in scope.

4. Prove that the half-open interval index is unique

If two indices m,n satisfy their half-open inequalities, m>n would imply T_(n+1)≤T_m≤t, contradicting t<T_(n+1). The opposite inequality is symmetric. Empty zero-length intervals cause no overlap, so no extra strict-wait premise is needed.

\[m>n\Longrightarrow t<T_{n+1}\le T_m\le t,\quad\text{a contradiction}.\]
Corresponding Lean step
    -- Monotonicity makes distinct half-open event intervals disjoint.
    intro m hm
    apply le_antisymm
    · by_contra h
      have hnm : n + 1 ≤ m := by omega
      exact (not_lt_of_ge ((hmono hnm).trans hm.1)) hupp
    · by_contra h
      have hmn : m + 1 ≤ n := by omega
      exact (not_lt_of_ge ((hmono hmn).trans hlow)) hm.2

Exact contiguous compiled proof region; preceding local definitions and facts remain in scope.

5. Exclude stopped records at finite covering times

A stopped record has eventTime=∞. Its lower interval inequality ∞≤t contradicts finiteness of t. Thus every covering record must be active.

\[T_n\le t<\infty\Longrightarrow\operatorname{record}_n\ne\mathrm{stopped}.\]
Corresponding Lean step
  · -- A clock below finite t cannot be a stopped record.
    intro t n hlow hupp
    cases hr : record y xRef z₀ (ε sample) n with
    | inr u =>
      have hevent : eventTime y xRef z₀ (ε sample) n = ⊤ := by
        change (record y xRef z₀ (ε sample) n).elim _ _ = ⊤
        rw [hr]
        rfl
      rw [hevent] at hlow
      exact False.elim ((not_le_of_gt (WithTop.coe_lt_top t)) hlow)

Exact contiguous compiled proof region; preceding local definitions and facts remain in scope.

6. Recover the actual live record and its stored time

For an active record a the exact eventTime eliminator gives T_n=a.time. The lower interval inequality gives a.time≤t. The record supplied in the conclusion is this actual record, not a chosen external state.

\[\operatorname{record}_n=\mathrm{inl}(a)\Longrightarrow T_n=a.time\le t.\]
Corresponding Lean step
    | inl a =>
      have haClock : eventTime y xRef z₀ (ε sample) n = (a.1 : WithTop ℝ≥0) := by
        change (record y xRef z₀ (ε sample) n).elim _ _ = _
        rw [hr]
        rfl
      have hat : a.1 ≤ t := WithTop.coe_le_coe.mp (by
        rw [← haClock]
        exact hlow)
      refine ⟨a, ⟨rfl, hat, ?_⟩, ?_⟩

Exact contiguous compiled proof region; preceding local definitions and facts remain in scope.

7. Keep the last live arc when the next wait is infinite

If the actual next waiting time is infinity, every finite NNReal elapsed offset is strictly less than it. Stopping the next jump does not erase the currently live state or invent a phase at infinity.

\[\tau(a.state,\varepsilon_n)=\infty\Longrightarrow t-a.time<\infty=\tau(a.state,\varepsilon_n).\]
Corresponding Lean step
      · -- Infinite wait keeps the last live arc available at every finite offset.
        by_cases hwtop : τ y xRef a.2 (ε sample n) = ⊤
        · simp only [hwtop, WithTop.coe_lt_top]

Exact contiguous compiled proof region; preceding local definitions and facts remain in scope.

8. Bound the elapsed offset for a finite next wait

Write the actual finite wait as q. The existing guarded recurrence gives record_(n+1)=(a.time+q, bounce(flow(q,a.state))) and hence T_(n+1)=a.time+q. Therefore t<T_(n+1) and a.time≤t imply t−a.time<q. Subtraction is nonnegative and never evaluates an infinite elapsed duration.

\[T_{n+1}=a.time+q,\quad a.time\le t<T_{n+1}\Longrightarrow 0\le t-a.time<q.\]
Corresponding Lean step
        -- Finite wait: the actual next clock is a.time plus that same wait.
        · let q : ℝ≥0 := (τ y xRef a.2 (ε sample n)).untop hwtop
          have hq : (q : WithTop ℝ≥0) = τ y xRef a.2 (ε sample n) :=
            WithTop.coe_untop _ _
          have hn : record y xRef z₀ (ε sample) (n + 1) =
              Sum.inl (a.1 + (τ y xRef a.2 (ε sample n)).untopD 0,
                S xRef (Φ y xRef (((τ y xRef a.2 (ε sample n)).untopD 0 : ℝ≥0) : ℝ) a.2)) :=
            ((hstep y xRef z₀ (ε sample) n).2 a hr).2 hwtop
          rw [← hq] at hn ⊢
          have hnTime : eventTime y xRef z₀ (ε sample) (n + 1) =
              ((a.1 + q : ℝ≥0) : WithTop ℝ≥0) := by
            change (record y xRef z₀ (ε sample) (n + 1)).elim _ _ = _
            rw [hn]
            rfl
          have hsmall : t < a.1 + q := WithTop.coe_lt_coe.mp (by
            simpa only [hnTime] using hupp)
          exact WithTop.coe_lt_coe.mpr ((tsub_lt_iff_right hat).mpr (by
            simpa only [add_comm] using hsmall))

Exact contiguous compiled proof region; preceding local definitions and facts remain in scope.

9. Prove uniqueness of the actual live record

The record recursion is a function. Two live records at the same index have equal Sum.inl values, so injectivity gives equal time/state pairs. Assemble the interval and live-record conclusions on the common AE event.

\[\mathrm{inl}(a)=\operatorname{record}_n=\mathrm{inl}(b)\Longrightarrow a=b.\]
Corresponding Lean step
      · -- The stored record is a function; injectivity gives uniqueness.
        intro b hb
        exact Sum.inl.inj hb.1.symm

Exact contiguous compiled proof region; preceding local definitions and facts remain in scope.

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_physical_time_cover

Fix the actual source objects and finite-time target; Reuse initialized monotone actual clocks on the common AE event; Select the predecessor of the first clock crossing; Prove that the half-open interval index is unique; Exclude stopped records at finite covering times; Recover the actual live record and its stored time; Keep the last live arc when the next wait is infinite; Bound the elapsed offset for a finite next wait; Prove uniqueness of the actual live record

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_physical_time_cover
    {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_physical_time_cover_statement hα hαβ hV hH hη hβη := by
  classical
  let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
  let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun sample k => Real.toNNReal (sample k)
  let c : E → E → E := fun y xRef => y - η • gradient V xRef
  let Φ : E → E → ℝ → (E × E) → (E × E) := fun y xRef t z =>
    (c y xRef + Real.cos t • (z.1 - c y xRef) +
        (Real.sqrt η * Real.sin t) • z.2,
     (-Real.sin t / Real.sqrt η) • (z.1 - c y xRef) + Real.cos t • z.2)
  let S : E → (E × E) → (E × E) := fun xRef z =>
    (z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
      ‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
  let rate : E → (E × E) → ℝ := fun xRef z =>
    Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V xRef))
  let Λ : E → E → (E × E) → ℝ≥0 → ℝ := fun y xRef z t =>
    ∫ s in (0 : ℝ)..(t : ℝ), rate xRef (Φ y xRef s z)
  let τ : E → E → (E × E) → ℝ≥0 → WithTop ℝ≥0 := fun y xRef z e =>
    MeasureTheory.hittingAfter
      (fun t : ℝ≥0 => fun a : (E × E) × (E × E) × ℝ≥0 =>
        Λ a.1.1 a.1.2 a.2.1 t - (a.2.2 : ℝ))
      (Set.Ici (0 : ℝ)) 0 ((y, xRef), z, e)
  let next : E → E → ℝ≥0 → ((ℝ≥0 × (E × E)) ⊕ Unit) →
      ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef e r =>
    match r with
    | Sum.inr _ => Sum.inr ()
    | Sum.inl a =>
      if τ y xRef a.2 e = ⊤ then Sum.inr () else
        Sum.inl (a.1 + (τ y xRef a.2 e).untopD 0,
          S xRef (Φ y xRef (((τ y xRef a.2 e).untopD 0 : ℝ≥0) : ℝ) a.2))
  let record : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ →
      ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef z₀ e n =>
    Nat.rec (Sum.inl (0, z₀)) (fun k r => next y xRef (e k) r) n
  let 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, ∀ᵐ sample ∂P,
    (∀ t : ℝ≥0, ∃! n : ℕ,
      eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) ∧
      (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1)) ∧
    (∀ t : ℝ≥0, ∀ n : ℕ,
      eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) →
      (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) →
      ∃! a : ℝ≥0 × (E × E),
        record y xRef z₀ (ε sample) n = Sum.inl a ∧ a.1 ≤ t ∧
        ((t - a.1 : ℝ≥0) : WithTop ℝ≥0) < τ y xRef a.2 (ε sample n))
  -- Exact deterministic initialization/monotonicity and guarded live-record updates.
  rcases ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursion
      hα hαβ hV hH hη hβη with
    ⟨_, hstep, _, _, _, htime, _, _, _, _⟩
  have hinput := ActualNonaccumulation.actual_fixed_reference_event_time_nonaccumulation
    hα hαβ hV hH hη hβη
  intro y xRef z₀
  filter_upwards [hinput y xRef z₀] with sample hgood
  have hzero : eventTime y xRef z₀ (ε sample) 0 = 0 :=
    (htime y xRef z₀ (ε sample)).1
  have hmono : Monotone (eventTime y xRef z₀ (ε sample)) :=
    (htime y xRef z₀ (ε sample)).2
  constructor
  · -- The first clock strictly above t has an initialized finite predecessor.
    intro t
    obtain ⟨N, hN⟩ := eventually_atTop.mp (hgood.1 t)
    have hex : ∃ k : ℕ, (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) k :=
      ⟨N, hN N le_rfl⟩
    let k : ℕ := Nat.find hex
    have hk : (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) k :=
      Nat.find_spec hex
    have hkpos : 0 < k := by
      by_contra h
      have hk0 : k = 0 := Nat.eq_zero_of_not_pos h
      rw [hk0, hzero] at hk
      exact (not_lt_of_ge (show (0 : WithTop ℝ≥0) ≤ t from bot_le)) hk
    let n : ℕ := k - 1
    have hsucc : n + 1 = k := by dsimp [n]; omega
    have hlow : eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) := by
      apply le_of_not_gt
      exact Nat.find_min hex (by change k - 1 < k; omega)
    have hupp : (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) := by
      simpa only [hsucc] using hk
    refine ⟨n, ⟨hlow, hupp⟩, ?_⟩
    -- Monotonicity makes distinct half-open event intervals disjoint.
    intro m hm
    apply le_antisymm
    · by_contra h
      have hnm : n + 1 ≤ m := by omega
      exact (not_lt_of_ge ((hmono hnm).trans hm.1)) hupp
    · by_contra h
      have hmn : m + 1 ≤ n := by omega
      exact (not_lt_of_ge ((hmono hmn).trans hlow)) hm.2
  · -- A clock below finite t cannot be a stopped record.
    intro t n hlow hupp
    cases hr : record y xRef z₀ (ε sample) n with
    | inr u =>
      have hevent : eventTime y xRef z₀ (ε sample) n = ⊤ := by
        change (record y xRef z₀ (ε sample) n).elim _ _ = ⊤
        rw [hr]
        rfl
      rw [hevent] at hlow
      exact False.elim ((not_le_of_gt (WithTop.coe_lt_top t)) hlow)
    | inl a =>
      have haClock : eventTime y xRef z₀ (ε sample) n = (a.1 : WithTop ℝ≥0) := by
        change (record y xRef z₀ (ε sample) n).elim _ _ = _
        rw [hr]
        rfl
      have hat : a.1 ≤ t := WithTop.coe_le_coe.mp (by
        rw [← haClock]
        exact hlow)
      refine ⟨a, ⟨rfl, hat, ?_⟩, ?_⟩
      · -- Infinite wait keeps the last live arc available at every finite offset.
        by_cases hwtop : τ y xRef a.2 (ε sample n) = ⊤
        · simp only [hwtop, WithTop.coe_lt_top]
        -- Finite wait: the actual next clock is a.time plus that same wait.
        · let q : ℝ≥0 := (τ y xRef a.2 (ε sample n)).untop hwtop
          have hq : (q : WithTop ℝ≥0) = τ y xRef a.2 (ε sample n) :=
            WithTop.coe_untop _ _
          have hn : record y xRef z₀ (ε sample) (n + 1) =
              Sum.inl (a.1 + (τ y xRef a.2 (ε sample n)).untopD 0,
                S xRef (Φ y xRef (((τ y xRef a.2 (ε sample n)).untopD 0 : ℝ≥0) : ℝ) a.2)) :=
            ((hstep y xRef z₀ (ε sample) n).2 a hr).2 hwtop
          rw [← hq] at hn ⊢
          have hnTime : eventTime y xRef z₀ (ε sample) (n + 1) =
              ((a.1 + q : ℝ≥0) : WithTop ℝ≥0) := by
            change (record y xRef z₀ (ε sample) (n + 1)).elim _ _ = _
            rw [hn]
            rfl
          have hsmall : t < a.1 + q := WithTop.coe_lt_coe.mp (by
            simpa only [hnTime] using hupp)
          exact WithTop.coe_lt_coe.mpr ((tsub_lt_iff_right hat).mpr (by
            simpa only [add_comm] using hsmall))
      · -- The stored record is a function; injectivity gives uniqueness.
        intro b hb
        exact Sum.inl.inj hb.1.symm

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhysicalTimeCover

Exact module and namespace context

Scope and omitted-condition boundaries
  • Only actual interval/live-record/elapsed coverage on a common AE actual-input event per fixed deterministic parameter triple. No measurable index or interpolated process, explicit index0 initialization, global path uniqueness/regularity, Markov/invariance/kernel/hypocoercivity/main/errors/cost/composition. Stopped next jump leaves last live arc; no phase at infinity. No full-paper/Goal, stabilized, merged, purified or live credit.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • Nat.find
  • Nat.find_spec
  • Nat.find_min
  • Nat.eq_zero_of_not_pos
  • Filter.eventually_atTop
  • WithTop.coe_lt_top
  • WithTop.coe_le_coe
  • WithTop.coe_lt_coe
  • WithTop.coe_untop
  • tsub_lt_iff_right
  • Sum.inl.inj

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.