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

Actual PBPS jointly measurable physical-time phase

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, arXiv2609.06905v1 Appendix A.1 (A.2), A1.E2 and the between-jump paragraph A1.SS1.p2.2, with nonaccumulation p3.7. The joint measurable physical-time representative and initialization adapter is an ASTIS completion of an implicit construction step, not a quotation or the full Proposition3.1.

arXiv2609.06905v1 · Chen-Chewi-Lu-Zhang arXiv2609.06905v1 Algorithm1 and AppendixA1 A.2/A1.E2/A1.SS1.p2.2 between-jump prescription; original six analytic conditions; actual source implicit measurable realization adapter. · faithful paraphrase

Complete source statement (Samplinglib restatement)

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. Allow arbitrary parameters 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. There exists a total phase map Z:E×E×(E×E)×[0,∞)×Ω→E×E jointly Borel measurable in all displayed parameters, finite physical time t and sample, while V,α,β,η remain fixed. For every parameter triple, every sample, every finite t and any actual covering index n with T_n≤t<T_(n+1), if record_n=inl(a) with a=(s,z), then Z(y,xRef,z0,t,sample)=Φ_(t−s)(z), where subtraction is the NNReal nonnegative subtraction. If no such actual covering index exists, Z(y,xRef,z0,t,sample)=z0. This uncovered value is an explicitly chosen ASTIS total representative convention, not a source state supplied on exceptional inputs. Furthermore, for each fixed deterministic y,xRef,z0, for P-almost every sample simultaneously: for every finite nonnegative t there exist n and an actual finite live record a=(s,z) with T_n≤t<T_(n+1), record_n=inl(a), s≤t, t−s<τ(z,ε_n) and Z(y,xRef,z0,t,sample)=Φ_(t−s)(z); and Z(y,xRef,z0,0,sample)=z0. A stopped record never provides the source phase. An infinite next wait retains the last live harmonic arc for all later finite t and does not trigger the uncovered fallback. The AE event may depend on the fixed parameter triple; no uniform event over all parameters is asserted. Joint measurability permits later measurable parameter evaluation, but per-parameter AE agreement cannot be substituted at arbitrary parameters correlated with sample without a separate law/independence/conditional-kernel argument. This is an ASTIS source-implicit measurable realization of Appendix A.1's actual between-jump prescription, not the full process/Markov/invariance/main sampler/error/query-cost/composition theorem. No positive dimension, energy, cap, selector, nonexplosion, positive support, measurable flow or higher regularity certificate is a new premise.

  • E is any finite-dimensional real inner-product space with its Borel measurable structure, including dimension zero. V is real-valued and C²; α,β are nonnegative reals.
  • Exactly six analytic source hypotheses: α>0; α≤β; V∈C²; for all x,v, α‖v‖²≤D²V(x)[v,v]≤β‖v‖²; η>0; βη≤1. No third or higher derivative bound.
  • Standing E,V,α,β,η are fixed. y,xRef,z0,t,sample are arguments of one jointly Borel map. P and ε are literal canonical definitions; measurability, positive support, recurrence, cover and nonaccumulation are produced dependencies.
  • The deterministic covered-arc characterization and uncovered fallback hold for every sample. Actual all-time agreement and initialization hold on one AE sample event for each fixed parameter triple. No uniform AE event over uncountably many parameter triples and no arbitrary correlated random-parameter law are inferred.
  • A stopped record has no phase and infinite event time; every covering interval has a live finite record. The last infinite-wait live arc remains covered. The initial-phase fallback is an explicitly labelled ASTIS measurable extension only on the uncovered complement; zero-time exceptional bounces need not have source index0 at t0.

Actual source objects 1

\[c=y-\eta\nabla V(x_{\rm ref}),\quad g(x)=\nabla V(x)-\nabla V(x_{\rm ref}),\quad\lambda(x,p)=\sqrt\eta\max\{0,\langle p,g(x)\rangle\}.\]

Actual source objects 2

\[\Phi_t(x,p)=\left(c+\cos t(x-c)+\sqrt\eta\sin t\,p,\ -\frac{\sin t}{\sqrt\eta}(x-c)+\cos t\,p\right),\quad S(x,p)=\left(x,p-\frac{2\langle p,g(x)\rangle}{\|g(x)\|^2}g(x)\right).\]

Actual source objects 3

\[\Lambda(z,t)=\int_0^t\lambda(\Phi_s z)\,ds,\quad\tau(z,e)=\inf\{t\ge0:\Lambda(z,t)\ge e\},\quad\inf\varnothing=\infty.\]

Actual source objects 4

\[D_n=\{T_n\le t<T_{n+1}\},\quad Z=\Phi_{t-a.time}(a.phase)\text{ on }D_n,\quad Z=z_0\text{ on }(\bigcup_nD_n)^c.\]

Actual source objects 5

\[Z\text{ jointly Borel in }(y,x_{\rm ref},z_0,t,\omega);\quad\forall(y,x_{\rm ref},z_0),\ P\text{-a.s. }[\forall t<\infty,\ Z_t=\Phi_{t-T_n}(z_n)],\quad Z_0=z_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 jointly measurable physical-time phase

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhysicalTimeMeasurability.actual_physical_time_measurable_phase · 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. Allow arbitrary parameters 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. There exists a total phase map Z:E×E×(E×E)×[0,∞)×Ω→E×E jointly Borel measurable in all displayed parameters, finite physical time t and sample, while V,α,β,η remain fixed. For every parameter triple, every sample, every finite t and any actual covering index n with T_n≤t<T_(n+1), if record_n=inl(a) with a=(s,z), then Z(y,xRef,z0,t,sample)=Φ_(t−s)(z), where subtraction is the NNReal nonnegative subtraction. If no such actual covering index exists, Z(y,xRef,z0,t,sample)=z0. This uncovered value is an explicitly chosen ASTIS total representative convention, not a source state supplied on exceptional inputs. Furthermore, for each fixed deterministic y,xRef,z0, for P-almost every sample simultaneously: for every finite nonnegative t there exist n and an actual finite live record a=(s,z) with T_n≤t<T_(n+1), record_n=inl(a), s≤t, t−s<τ(z,ε_n) and Z(y,xRef,z0,t,sample)=Φ_(t−s)(z); and Z(y,xRef,z0,0,sample)=z0. A stopped record never provides the source phase. An infinite next wait retains the last live harmonic arc for all later finite t and does not trigger the uncovered fallback. The AE event may depend on the fixed parameter triple; no uniform event over all parameters is asserted. Joint measurability permits later measurable parameter evaluation, but per-parameter AE agreement cannot be substituted at arbitrary parameters correlated with sample without a separate law/independence/conditional-kernel argument. This is an ASTIS source-implicit measurable realization of Appendix A.1's actual between-jump prescription, not the full process/Markov/invariance/main sampler/error/query-cost/composition theorem. No positive dimension, energy, cap, selector, nonexplosion, positive support, measurable flow or higher regularity certificate is a new premise.

\[Z\text{ jointly Borel in }(y,x_{\rm ref},z_0,t,\omega);\quad\forall(y,x_{\rm ref},z_0),\ P\text{-a.s. }[\forall t<\infty,\ Z_t=\Phi_{t-T_n}(z_n)],\quad Z_0=z_0.\]
Lean statement · actual_physical_time_measurable_phase

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. Allow arbitrary parameters 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. There exists a total phase map Z:E×E×(E×E)×[0,∞)×Ω→E×E jointly Borel measurable in all displayed parameters, finite physical time t and sample, while V,α,β,η remain fixed. For every parameter triple, every sample, every finite t and any actual covering index n with T_n≤t<T_(n+1), if record_n=inl(a) with a=(s,z), then Z(y,xRef,z0,t,sample)=Φ_(t−s)(z), where subtraction is the NNReal nonnegative subtraction. If no such actual covering index exists, Z(y,xRef,z0,t,sample)=z0. This uncovered value is an explicitly chosen ASTIS total representative convention, not a source state supplied on exceptional inputs. Furthermore, for each fixed deterministic y,xRef,z0, for P-almost every sample simultaneously: for every finite nonnegative t there exist n and an actual finite live record a=(s,z) with T_n≤t<T_(n+1), record_n=inl(a), s≤t, t−s<τ(z,ε_n) and Z(y,xRef,z0,t,sample)=Φ_(t−s)(z); and Z(y,xRef,z0,0,sample)=z0. A stopped record never provides the source phase. An infinite next wait retains the last live harmonic arc for all later finite t and does not trigger the uncovered fallback. The AE event may depend on the fixed parameter triple; no uniform event over all parameters is asserted. Joint measurability permits later measurable parameter evaluation, but per-parameter AE agreement cannot be substituted at arbitrary parameters correlated with sample without a separate law/independence/conditional-kernel argument. This is an ASTIS source-implicit measurable realization of Appendix A.1's actual between-jump prescription, not the full process/Markov/invariance/main sampler/error/query-cost/composition theorem. No positive dimension, energy, cap, selector, nonexplosion, positive support, measurable flow or higher regularity certificate is a new premise.

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_physical_time_measurable_phase
    {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_physical_time_measurable_phase_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_physical_time_measurable_phase_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_physical_time_measurable_phase_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 _ => ⊤)
    ∃ Z : E → E → (E × E) → ℝ≥0 → (ℕ → ℝ) → (E × E),
      Measurable (fun a : ((E × E) × (E × E)) × ℝ≥0 × (ℕ → ℝ) =>
        Z a.1.1.1 a.1.1.2 a.1.2 a.2.1 a.2.2) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ sample : ℕ → ℝ, ∀ t : ℝ≥0,
        ∀ n : ℕ, ∀ a : ℝ≥0 × (E × E),
          eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) →
          (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) →
          record y xRef z₀ (ε sample) n = Sum.inl a →
          Z y xRef z₀ t sample = Φ y xRef ((t - a.1 : ℝ≥0) : ℝ) a.2) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ sample : ℕ → ℝ, ∀ t : ℝ≥0,
        (¬ ∃ n : ℕ, eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) ∧
          (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1)) →
          Z y xRef z₀ t sample = z₀) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ᵐ sample ∂P,
        (∀ t : ℝ≥0, ∃ n : ℕ, ∃ a : ℝ≥0 × (E × E),
          eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) ∧
          (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) ∧
          record y xRef z₀ (ε sample) n = Sum.inl a ∧ a.1 ≤ t ∧
          ((t - a.1 : ℝ≥0) : WithTop ℝ≥0) < τ y xRef a.2 (ε sample n) ∧
          Z y xRef z₀ t sample = Φ y xRef ((t - a.1 : ℝ≥0) : ℝ) a.2) ∧
        Z y xRef z₀ 0 sample = z₀)


set_option maxHeartbeats 1600000 in

Exact module and namespace context

Proof roadmap

  1. 1Retain actual source objects

    Use the canonical Exp1 sample, actual NNReal thresholds, harmonic flow, reflection, integrated hazard, hitting time and guarded stopped recurrence. No witness or measurable clock is supplied as an extra assumption.

  2. 2Pull back the measurable actual records and clocks

    The verified finite-record theorem supplies joint measurability of every finite stopped record and clock. Coordinate clamping is measurable, so composition gives joint measurable maps in parameters, physical time and the real-sequence sample. The verified harmonic-flow theorem supplies joint measurable harmonic flow and Phi0=id.

  3. 3Build disjoint measurable half-open intervals

    Order comparison makes each D_n measurable for all inputs. Actual clock monotonicity implies that if n<m, then t<T_(n+1)≤T_m≤t would contradict simultaneous membership. Nonaccumulation is not used to prove this deterministic measurability or disjointness.

  4. 4Make the finite harmonic branch measurable

    The auxiliary Sum projection is total with a dummy zero branch only to define a Borel branch everywhere. A selected D_n cannot have a stopped nth record because its left clock is at most finite t. Thus the dummy never supplies the source phase. NNReal elapsed subtraction and the exact harmonic formula give joint Borel branch maps.

  5. 5Glue countably many branches and the explicit complement

    Use Option naturals: some n indexes D_n, none indexes the measurable uncovered complement. The none value is the initial phase coordinate z0. All sets are disjoint, so their values agree on overlaps. Pinned Mathlib countable measurable piecewise assembly proves existence of a total Borel realization.

  6. 6Realize one joint phase map and its actual covered arcs

    Curry the proved measurable f into Z. On every actual covering interval, piecewise agreement selects the nth branch. Rewriting the actual live-record equality removes the dummy Sum branch and gives the exact finite elapsed harmonic interpolation. This deterministic characterization holds for all samples.

  7. 7Certify the uncovered representative convention

    If no interval covers a pair, it lies in the none set. Piecewise agreement gives Z=z0 there. This is a declared ASTIS exceptional extension and is not used for a last live arc with an infinite next wait.

  8. 8Obtain actual interpolation simultaneously at every finite time

    For each fixed parameter triple use the verified interval-cover theorem on its common AE sample event, together with the canonical positive-input support. At every finite t, the verified interval-cover theorem supplies the actual covering index and live record, its stored time≤t and elapsed below the next wait. The deterministic characterization gives actual Z agreement on that same event.

  9. 9Derive source initialization from actual positive input

    The initial record is (0,z0). Actual epsilon0 is strictly positive AE by the proved canonical input law. If record1 is stopped its clock is infinity; otherwise the actual finite recursion strict increment gives T1>0. Hence interval0 contains physical0. The covered formula and Phi0=id yield Z0=z0, without asserting initialization for every exceptional real sequence.

Full assumptions and notation

All objects and hypotheses

  • E is any finite-dimensional real inner-product space with its Borel measurable structure, including dimension zero. V is real-valued and C²; α,β are nonnegative reals.
  • Exactly six analytic source hypotheses: α>0; α≤β; V∈C²; for all x,v, α‖v‖²≤D²V(x)[v,v]≤β‖v‖²; η>0; βη≤1. No third or higher derivative bound.
  • Standing E,V,α,β,η are fixed. y,xRef,z0,t,sample are arguments of one jointly Borel map. P and ε are literal canonical definitions; measurability, positive support, recurrence, cover and nonaccumulation are produced dependencies.
  • The deterministic covered-arc characterization and uncovered fallback hold for every sample. Actual all-time agreement and initialization hold on one AE sample event for each fixed parameter triple. No uniform AE event over uncountably many parameter triples and no arbitrary correlated random-parameter law are inferred.
  • A stopped record has no phase and infinite event time; every covering interval has a live finite record. The last infinite-wait live arc remains covered. The initial-phase fallback is an explicitly labelled ASTIS measurable extension only on the uncovered complement; zero-time exceptional bounces need not have source index0 at t0.

Mathematical proof

1. Retain actual source objects

Use the canonical Exp1 sample, actual NNReal thresholds, harmonic flow, reflection, integrated hazard, hitting time and guarded stopped recurrence. No witness or measurable clock is supplied as an extra assumption.

\[\varepsilon_n(\omega)=\max\{\omega_n,0\},\quad\operatorname{record}_0=(0,z_0),\quad T_n=\infty\text{ only if stopped}.\]
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 _ => ⊤)

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

2. Pull back the measurable actual records and clocks

The verified finite-record theorem supplies joint measurability of every finite stopped record and clock. Coordinate clamping is measurable, so composition gives joint measurable maps in parameters, physical time and the real-sequence sample. The verified harmonic-flow theorem supplies joint measurable harmonic flow and Phi0=id.

\[(y,x_{\rm ref},z_0,t,\omega)\mapsto \operatorname{record}_n(y,x_{\rm ref},z_0,\varepsilon(\omega)),\ T_n\quad\text{are Borel}.\]
Corresponding Lean step
  have h76 := ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursion
    hα hαβ hV hH hη hβη
  rcases h76 with ⟨hinit, _, _, hrecordM, htimeM, hmono, _, _, _, hstrict⟩
  have hflow := ActualHarmonicFlow.actual_harmonic_flow_laws hα hαβ hV hH hη hβη
  have hΦM : Measurable (fun a : (E × E) × ℝ × (E × E) =>
      Φ a.1.1 a.1.2 a.2.1 a.2.2) := hflow.2.1
  have hΦ0 : ∀ y xRef : E, ∀ z : E × E, Φ y xRef 0 z = z := hflow.2.2.1
  have hεM : Measurable ε := measurable_pi_lambda _ fun n =>
    measurable_real_toNNReal.comp (measurable_pi_apply n)
  let A := ((E × E) × (E × E)) × ℝ≥0 × (ℕ → ℝ)
  let args : A → (E × E) × (E × E) × (ℕ → ℝ≥0) :=
    fun a => (a.1.1, a.1.2, ε a.2.2)
  have hargs : Measurable args := measurable_fst.fst.prodMk
    (measurable_fst.snd.prodMk (hεM.comp measurable_snd.snd))
  have hrM (n : ℕ) : Measurable (fun a : A =>
      record a.1.1.1 a.1.1.2 a.1.2 (ε a.2.2) n) := (hrecordM n).comp hargs
  have hTM (n : ℕ) : Measurable (fun a : A =>
      eventTime a.1.1.1 a.1.1.2 a.1.2 (ε a.2.2) n) := (htimeM n).comp hargs
  have htM : Measurable (fun a : A => (a.2.1 : WithTop ℝ≥0)) :=
    WithTop.measurable_coe.comp measurable_snd.fst

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

3. Build disjoint measurable half-open intervals

Order comparison makes each D_n measurable for all inputs. Actual clock monotonicity implies that if n<m, then t<T_(n+1)≤T_m≤t would contradict simultaneous membership. Nonaccumulation is not used to prove this deterministic measurability or disjointness.

\[D_n=\{T_n\le t<T_{n+1}\},\quad D_n\cap D_m=\varnothing\ (n\ne m).\]
Corresponding Lean step
  let D : ℕ → Set A := fun n => {a |
    eventTime a.1.1.1 a.1.1.2 a.1.2 (ε a.2.2) n ≤ (a.2.1 : WithTop ℝ≥0) ∧
    (a.2.1 : WithTop ℝ≥0) < eventTime a.1.1.1 a.1.1.2 a.1.2 (ε a.2.2) (n + 1)}
  have hDM (n : ℕ) : MeasurableSet (D n) :=
    (measurableSet_le (hTM n) htM).inter (measurableSet_lt htM (hTM (n + 1)))
  have hdisj (n m : ℕ) (a : A) (hn : a ∈ D n) (hm : a ∈ D m) : n = m := by
    have hmon : Monotone (eventTime a.1.1.1 a.1.1.2 a.1.2 (ε a.2.2)) :=
      (hmono a.1.1.1 a.1.1.2 a.1.2 (ε a.2.2)).2
    rcases lt_trichotomy n m with hlt | heq | hgt
    · exact False.elim ((not_lt_of_ge hm.1) (hn.2.trans_le (hmon (Nat.succ_le_of_lt hlt))))
    · exact heq
    · exact False.elim ((not_lt_of_ge hn.1) (hm.2.trans_le (hmon (Nat.succ_le_of_lt hgt))))

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

4. Make the finite harmonic branch measurable

The auxiliary Sum projection is total with a dummy zero branch only to define a Borel branch everywhere. A selected D_n cannot have a stopped nth record because its left clock is at most finite t. Thus the dummy never supplies the source phase. NNReal elapsed subtraction and the exact harmonic formula give joint Borel branch maps.

\[g_n=\Phi_{t-L_n.time}(L_n.phase),\quad\operatorname{record}_n=\mathrm{inl}(a)\Longrightarrow L_n=a.\]
Corresponding Lean step
  -- This total auxiliary projection is used only on D_n, where the record is live.
  -- Its zero branch never supplies a source phase for a stopped record.
  let L : ℕ → A → ℝ≥0 × (E × E) := fun n a =>
    (record a.1.1.1 a.1.1.2 a.1.2 (ε a.2.2) n).elim id (fun _ => (0, (0, 0)))
  have hLM (n : ℕ) : Measurable (L n) :=
    (measurable_id.sumElim measurable_const).comp (hrM n)
  let branch : ℕ → A → E × E := fun n a =>
    Φ a.1.1.1 a.1.1.2 ((a.2.1 - (L n a).1 : ℝ≥0) : ℝ) (L n a).2
  have hbM (n : ℕ) : Measurable (branch n) :=
    hΦM.comp (measurable_fst.fst.prodMk
      ((measurable_coe_nnreal_real.comp (measurable_snd.fst.sub (hLM n).fst)).prodMk
        (hLM n).snd))

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

5. Glue countably many branches and the explicit complement

Use Option naturals: some n indexes D_n, none indexes the measurable uncovered complement. The none value is the initial phase coordinate z0. All sets are disjoint, so their values agree on overlaps. Pinned Mathlib countable measurable piecewise assembly proves existence of a total Borel realization.

\[D_{\mathrm{none}}=(\bigcup_nD_n)^c,\quad g_{\mathrm{none}}=z_0,\quad\exists f\text{ Borel},\ f|_{D_i}=g_i.\]
Corresponding Lean step
  let sets : Option ℕ → Set A
    | none => (⋃ n, D n)ᶜ
    | some n => D n
  let values : Option ℕ → A → E × E
    | none => fun a => a.1.2
    | some n => branch n
  have hsM (i : Option ℕ) : MeasurableSet (sets i) := by
    cases i with
    | none => exact (MeasurableSet.iUnion hDM).compl
    | some n => exact hDM n
  have hvM (i : Option ℕ) : Measurable (values i) := by
    cases i with
    | none => exact measurable_fst.snd
    | some n => exact hbM n
  have hcompat : Pairwise (fun i j => Set.EqOn (values i) (values j) (sets i ∩ sets j)) := by
    intro i j hij a ha
    cases i with
    | none =>
      cases j with
      | none => exact False.elim (hij rfl)
      | some m => exact False.elim (ha.1 (Set.mem_iUnion.mpr ⟨m, ha.2⟩))
    | some n =>
      cases j with
      | none => exact False.elim (ha.2 (Set.mem_iUnion.mpr ⟨n, ha.1⟩))
      | some m => exact False.elim (hij (congrArg some (hdisj n m a ha.1 ha.2)))

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

6. Realize one joint phase map and its actual covered arcs

Curry the proved measurable f into Z. On every actual covering interval, piecewise agreement selects the nth branch. Rewriting the actual live-record equality removes the dummy Sum branch and gives the exact finite elapsed harmonic interpolation. This deterministic characterization holds for all samples.

\[Z(y,x_{\rm ref},z_0,t,\omega)=f(((y,x_{\rm ref}),z_0),t,\omega)=\Phi_{t-a.time}(a.phase)\quad\text{on }D_n.\]
Corresponding Lean step
  obtain ⟨f, hfM, hf⟩ := exists_measurable_piecewise sets hsM values hvM hcompat
  let Z : E → E → (E × E) → ℝ≥0 → (ℕ → ℝ) → (E × E) :=
    fun y xRef z₀ t sample => f (((y, xRef), z₀), t, sample)
  have hZ (y xRef : E) (z₀ : E × E) (sample : ℕ → ℝ) (t : ℝ≥0)
      (n : ℕ) (a : ℝ≥0 × (E × E))
      (hl : eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0))
      (hu : (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1))
      (hr : record y xRef z₀ (ε sample) n = Sum.inl a) :
      Z y xRef z₀ t sample = Φ y xRef ((t - a.1 : ℝ≥0) : ℝ) a.2 := by
    have heq := hf (some n) (show (((y, xRef), z₀), t, sample) ∈ sets (some n) from ⟨hl, hu⟩)
    change f (((y, xRef), z₀), t, sample) = _
    rw [heq]
    dsimp [values, branch, L]
    rw [hr]
    rfl

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

7. Certify the uncovered representative convention

If no interval covers a pair, it lies in the none set. Piecewise agreement gives Z=z0 there. This is a declared ASTIS exceptional extension and is not used for a last live arc with an infinite next wait.

\[(\nexists n:T_n\le t<T_{n+1})\Longrightarrow Z(y,x_{\rm ref},z_0,t,\omega)=z_0.\]
Corresponding Lean step
  refine ⟨Z, hfM, hZ, ?_, ?_⟩
  · intro y xRef z₀ sample t hn
    exact hf none (show (((y, xRef), z₀), t, sample) ∈ sets none from by
      intro hx
      obtain ⟨n, hnD⟩ := Set.mem_iUnion.mp hx
      exact hn ⟨n, hnD⟩)

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

8. Obtain actual interpolation simultaneously at every finite time

For each fixed parameter triple use the verified interval-cover theorem on its common AE sample event, together with the canonical positive-input support. At every finite t, the verified interval-cover theorem supplies the actual covering index and live record, its stored time≤t and elapsed below the next wait. The deterministic characterization gives actual Z agreement on that same event.

\[\forall(y,x_{\rm ref},z_0),\quad P\text{-a.s. }\forall t<\infty,\quad\exists n,a:\ T_n\le t<T_{n+1},\quad t-a.time<\tau(a.phase,\varepsilon_n),\quad Z_t=\Phi_{t-a.time}(a.phase).\]
Corresponding Lean step
  · intro y xRef z₀
    have hc := ActualPhysicalTimeCover.actual_fixed_reference_physical_time_cover
      hα hαβ hV hH hη hβη y xRef z₀
    have hp := AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.2.2.2.1
    filter_upwards [hc, hp] with sample hcover hpositive
    constructor
    · intro t
      obtain ⟨n, hn, huniq⟩ := hcover.1 t
      obtain ⟨a, ha, hau⟩ := hcover.2 t n hn.1 hn.2
      exact ⟨n, a, hn.1, hn.2, ha.1, ha.2.1, ha.2.2,
        hZ y xRef z₀ sample t n a hn.1 hn.2 ha.1⟩

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

9. Derive source initialization from actual positive input

The initial record is (0,z0). Actual epsilon0 is strictly positive AE by the proved canonical input law. If record1 is stopped its clock is infinity; otherwise the actual finite recursion strict increment gives T1>0. Hence interval0 contains physical0. The covered formula and Phi0=id yield Z0=z0, without asserting initialization for every exceptional real sequence.

\[\varepsilon_0>0\Longrightarrow 0=T_0<T_1\le\infty,\quad Z_0=\Phi_0(z_0)=z_0\quad P\text{-a.s.}.\]
Corresponding Lean step
    · have hi0 : record y xRef z₀ (ε sample) 0 = Sum.inl (0, z₀) :=
        hinit y xRef z₀ (ε sample)
      have hT0 : eventTime y xRef z₀ (ε sample) 0 = 0 :=
        (hmono y xRef z₀ (ε sample)).1
      have hepos : 0 < ε sample 0 := Real.toNNReal_pos.mpr (hpositive 0).1
      have hfirst : (0 : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) 1 := by
        cases hr1 : record y xRef z₀ (ε sample) 1 with
        | inr u =>
          change (0 : WithTop ℝ≥0) <
            (record y xRef z₀ (ε sample) 1).elim (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
          rw [hr1]
          exact WithTop.coe_lt_top (0 : ℝ≥0)
        | inl b =>
          have hbpos : 0 < b.1 :=
            (hstrict y xRef z₀ (ε sample) 0 (0, z₀) hi0).2 b hepos hr1
          change (0 : WithTop ℝ≥0) <
            (record y xRef z₀ (ε sample) 1).elim (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
          rw [hr1]
          exact WithTop.coe_lt_coe.mpr hbpos
      have heq := hZ y xRef z₀ sample 0 0 (0, z₀)
        (by rw [hT0]; rfl) hfirst hi0
      simpa only [tsub_zero, NNReal.coe_zero, hΦ0] using heq

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_physical_time_measurable_phase

Retain actual source objects; Pull back the measurable actual records and clocks; Build disjoint measurable half-open intervals; Make the finite harmonic branch measurable; Glue countably many branches and the explicit complement; Realize one joint phase map and its actual covered arcs; Certify the uncovered representative convention; Obtain actual interpolation simultaneously at every finite time; Derive source initialization from actual positive input

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_physical_time_measurable_phase
    {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_physical_time_measurable_phase_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 _ => ⊤)
  have h76 := ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursion
    hα hαβ hV hH hη hβη
  rcases h76 with ⟨hinit, _, _, hrecordM, htimeM, hmono, _, _, _, hstrict⟩
  have hflow := ActualHarmonicFlow.actual_harmonic_flow_laws hα hαβ hV hH hη hβη
  have hΦM : Measurable (fun a : (E × E) × ℝ × (E × E) =>
      Φ a.1.1 a.1.2 a.2.1 a.2.2) := hflow.2.1
  have hΦ0 : ∀ y xRef : E, ∀ z : E × E, Φ y xRef 0 z = z := hflow.2.2.1
  have hεM : Measurable ε := measurable_pi_lambda _ fun n =>
    measurable_real_toNNReal.comp (measurable_pi_apply n)
  let A := ((E × E) × (E × E)) × ℝ≥0 × (ℕ → ℝ)
  let args : A → (E × E) × (E × E) × (ℕ → ℝ≥0) :=
    fun a => (a.1.1, a.1.2, ε a.2.2)
  have hargs : Measurable args := measurable_fst.fst.prodMk
    (measurable_fst.snd.prodMk (hεM.comp measurable_snd.snd))
  have hrM (n : ℕ) : Measurable (fun a : A =>
      record a.1.1.1 a.1.1.2 a.1.2 (ε a.2.2) n) := (hrecordM n).comp hargs
  have hTM (n : ℕ) : Measurable (fun a : A =>
      eventTime a.1.1.1 a.1.1.2 a.1.2 (ε a.2.2) n) := (htimeM n).comp hargs
  have htM : Measurable (fun a : A => (a.2.1 : WithTop ℝ≥0)) :=
    WithTop.measurable_coe.comp measurable_snd.fst
  let D : ℕ → Set A := fun n => {a |
    eventTime a.1.1.1 a.1.1.2 a.1.2 (ε a.2.2) n ≤ (a.2.1 : WithTop ℝ≥0) ∧
    (a.2.1 : WithTop ℝ≥0) < eventTime a.1.1.1 a.1.1.2 a.1.2 (ε a.2.2) (n + 1)}
  have hDM (n : ℕ) : MeasurableSet (D n) :=
    (measurableSet_le (hTM n) htM).inter (measurableSet_lt htM (hTM (n + 1)))
  have hdisj (n m : ℕ) (a : A) (hn : a ∈ D n) (hm : a ∈ D m) : n = m := by
    have hmon : Monotone (eventTime a.1.1.1 a.1.1.2 a.1.2 (ε a.2.2)) :=
      (hmono a.1.1.1 a.1.1.2 a.1.2 (ε a.2.2)).2
    rcases lt_trichotomy n m with hlt | heq | hgt
    · exact False.elim ((not_lt_of_ge hm.1) (hn.2.trans_le (hmon (Nat.succ_le_of_lt hlt))))
    · exact heq
    · exact False.elim ((not_lt_of_ge hn.1) (hm.2.trans_le (hmon (Nat.succ_le_of_lt hgt))))
  -- This total auxiliary projection is used only on D_n, where the record is live.
  -- Its zero branch never supplies a source phase for a stopped record.
  let L : ℕ → A → ℝ≥0 × (E × E) := fun n a =>
    (record a.1.1.1 a.1.1.2 a.1.2 (ε a.2.2) n).elim id (fun _ => (0, (0, 0)))
  have hLM (n : ℕ) : Measurable (L n) :=
    (measurable_id.sumElim measurable_const).comp (hrM n)
  let branch : ℕ → A → E × E := fun n a =>
    Φ a.1.1.1 a.1.1.2 ((a.2.1 - (L n a).1 : ℝ≥0) : ℝ) (L n a).2
  have hbM (n : ℕ) : Measurable (branch n) :=
    hΦM.comp (measurable_fst.fst.prodMk
      ((measurable_coe_nnreal_real.comp (measurable_snd.fst.sub (hLM n).fst)).prodMk
        (hLM n).snd))
  let sets : Option ℕ → Set A
    | none => (⋃ n, D n)ᶜ
    | some n => D n
  let values : Option ℕ → A → E × E
    | none => fun a => a.1.2
    | some n => branch n
  have hsM (i : Option ℕ) : MeasurableSet (sets i) := by
    cases i with
    | none => exact (MeasurableSet.iUnion hDM).compl
    | some n => exact hDM n
  have hvM (i : Option ℕ) : Measurable (values i) := by
    cases i with
    | none => exact measurable_fst.snd
    | some n => exact hbM n
  have hcompat : Pairwise (fun i j => Set.EqOn (values i) (values j) (sets i ∩ sets j)) := by
    intro i j hij a ha
    cases i with
    | none =>
      cases j with
      | none => exact False.elim (hij rfl)
      | some m => exact False.elim (ha.1 (Set.mem_iUnion.mpr ⟨m, ha.2⟩))
    | some n =>
      cases j with
      | none => exact False.elim (ha.2 (Set.mem_iUnion.mpr ⟨n, ha.1⟩))
      | some m => exact False.elim (hij (congrArg some (hdisj n m a ha.1 ha.2)))
  obtain ⟨f, hfM, hf⟩ := exists_measurable_piecewise sets hsM values hvM hcompat
  let Z : E → E → (E × E) → ℝ≥0 → (ℕ → ℝ) → (E × E) :=
    fun y xRef z₀ t sample => f (((y, xRef), z₀), t, sample)
  have hZ (y xRef : E) (z₀ : E × E) (sample : ℕ → ℝ) (t : ℝ≥0)
      (n : ℕ) (a : ℝ≥0 × (E × E))
      (hl : eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0))
      (hu : (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1))
      (hr : record y xRef z₀ (ε sample) n = Sum.inl a) :
      Z y xRef z₀ t sample = Φ y xRef ((t - a.1 : ℝ≥0) : ℝ) a.2 := by
    have heq := hf (some n) (show (((y, xRef), z₀), t, sample) ∈ sets (some n) from ⟨hl, hu⟩)
    change f (((y, xRef), z₀), t, sample) = _
    rw [heq]
    dsimp [values, branch, L]
    rw [hr]
    rfl
  refine ⟨Z, hfM, hZ, ?_, ?_⟩
  · intro y xRef z₀ sample t hn
    exact hf none (show (((y, xRef), z₀), t, sample) ∈ sets none from by
      intro hx
      obtain ⟨n, hnD⟩ := Set.mem_iUnion.mp hx
      exact hn ⟨n, hnD⟩)
  · intro y xRef z₀
    have hc := ActualPhysicalTimeCover.actual_fixed_reference_physical_time_cover
      hα hαβ hV hH hη hβη y xRef z₀
    have hp := AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.2.2.2.1
    filter_upwards [hc, hp] with sample hcover hpositive
    constructor
    · intro t
      obtain ⟨n, hn, huniq⟩ := hcover.1 t
      obtain ⟨a, ha, hau⟩ := hcover.2 t n hn.1 hn.2
      exact ⟨n, a, hn.1, hn.2, ha.1, ha.2.1, ha.2.2,
        hZ y xRef z₀ sample t n a hn.1 hn.2 ha.1⟩
    · have hi0 : record y xRef z₀ (ε sample) 0 = Sum.inl (0, z₀) :=
        hinit y xRef z₀ (ε sample)
      have hT0 : eventTime y xRef z₀ (ε sample) 0 = 0 :=
        (hmono y xRef z₀ (ε sample)).1
      have hepos : 0 < ε sample 0 := Real.toNNReal_pos.mpr (hpositive 0).1
      have hfirst : (0 : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) 1 := by
        cases hr1 : record y xRef z₀ (ε sample) 1 with
        | inr u =>
          change (0 : WithTop ℝ≥0) <
            (record y xRef z₀ (ε sample) 1).elim (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
          rw [hr1]
          exact WithTop.coe_lt_top (0 : ℝ≥0)
        | inl b =>
          have hbpos : 0 < b.1 :=
            (hstrict y xRef z₀ (ε sample) 0 (0, z₀) hi0).2 b hepos hr1
          change (0 : WithTop ℝ≥0) <
            (record y xRef z₀ (ε sample) 1).elim (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
          rw [hr1]
          exact WithTop.coe_lt_coe.mpr hbpos
      have heq := hZ y xRef z₀ sample 0 0 (0, z₀)
        (by rw [hT0]; rfl) hfirst hi0
      simpa only [tsub_zero, NNReal.coe_zero, hΦ0] using heq

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhysicalTimeMeasurability

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Original six analytic conditions and actual AppendixA1 objects.Same six public binders and eleven exact literal actual definitions; measurability/cover/support are dependency edges.sameExact independent header/binder/definition readback; no supplied certificates.
Euclidean phase and independent positive Exp1 thresholds.Finite-dimensional real inner-product Borel carrier including rank0; actual infinitePi and total NNReal clamp.source-implicitCanonical actual realization and reviewed intrinsic carrier; exceptional nonpositive inputs remain explicit.
Between-jump prescription defines actual interpolation at every finite time after nonaccumulation.Existence of one jointly Borel phase in finite parameters/time/sample, deterministic covered-arc agreement, explicit uncovered z0 extension, per-fixedparams common-AE all-time live-arc realization and AE initialization.source-implicitReviewed ASTIS measurable-realization adapter, including stronger joint deterministic-parameter measurability without new source hypotheses. No uniform uncountable parameter event. Infinite next wait retains last live arc.
Full path/Markov/invariance/law and main error/query-cost/composition results.These obligations are excluded from the current representative theorem.unresolvedRandom parameter substitution needs law/independence/conditional kernels; no correlated input inference or full theorem completion.

Actual total jointly measurable finite-physical-time representative and common-AE all-time actual arc agreement/initialization per fixed parameter triple. V/alpha/beta/eta fixed. Uncovered fallback is explicit ASTIS convention. No uniform AE all parameters or arbitrary correlated random parameter substitution; path regularity/adaptedness/Markov/invariance/laws/kernel/hypocoercivity/full sampler errors/cost/composition, full Exposition Seal/main merge/PURIFIED/live/whole Goal remain open.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • objects: Product/clamp, zero-index epsilon_n=source E_(n+1), Sum stopped coding, WithTop and guarded finite extraction explicitly realize source input/recursion. — Native independent source review slot:objects;classification:notation-resolution in runs/20261007-companion-priority/pbps-actual-physical-time-measurability80/fresh-source80/source-review.result80.json; exact current module and nine proof regions bound by run 851df6819e602fb254fb553e2ce9a23a035b949da14b5a9f1c65241481df4f16.
  • domains: Finite-dimensional inner-product Borel carrier including rank0 explicitly generalizes Euclidean coordinates; all physical time/elapsed finite NNReal; no dimension positivity. — Native independent source review slot:domains;classification:domain-clarification in runs/20261007-companion-priority/pbps-actual-physical-time-measurability80/fresh-source80/source-review.result80.json; exact current module and nine proof regions bound by run 851df6819e602fb254fb553e2ce9a23a035b949da14b5a9f1c65241481df4f16.
  • conclusion: Proved joint parameter/time/sample Borel realization completes source-compressed construction; labelled ASTIS adapter, no supplied selector/process/measurability premise and no verbatim-source joint theorem claim. — Native independent source review slot:conclusion;classification:source-implicit in runs/20261007-companion-priority/pbps-actual-physical-time-measurability80/fresh-source80/source-review.result80.json; exact current module and nine proof regions bound by run 851df6819e602fb254fb553e2ce9a23a035b949da14b5a9f1c65241481df4f16.
  • scopes: Explicit uncovered Z=z0 convention, stopped L dummy only auxiliary. Actual good arcs including infinite-wait last live arc covered and use Phi; no phase at top or every-sample initialization claimed. — Native independent source review slot:scopes;classification:formalization-artifact-risk in runs/20261007-companion-priority/pbps-actual-physical-time-measurability80/fresh-source80/source-review.result80.json; exact current module and nine proof regions bound by run 851df6819e602fb254fb553e2ce9a23a035b949da14b5a9f1c65241481df4f16.
  • quantifiers: One global measurable Z, common-AE forall finite t/init for each fixed triple. Uniform-parameter AE and arbitrary sample-correlated random-parameter source laws require separate arguments and remain excluded. — Native independent source review slot:quantifiers;classification:quantifier-clarification in runs/20261007-companion-priority/pbps-actual-physical-time-measurability80/fresh-source80/source-review.result80.json; exact current module and nine proof regions bound by run 851df6819e602fb254fb553e2ce9a23a035b949da14b5a9f1c65241481df4f16.
  • scopes: Direct Exp first-moment/mean1 SLLN source route stays OPEN alternative; parent bounded-indicator SLLN suffices for current actual divergence without extra binder. — Native independent source review slot:scopes;classification:open-source-route in runs/20261007-companion-priority/pbps-actual-physical-time-measurability80/fresh-source80/source-review.result80.json; exact current module and nine proof regions bound by run 851df6819e602fb254fb553e2ce9a23a035b949da14b5a9f1c65241481df4f16.

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
  • Actual total jointly measurable finite-physical-time representative and common-AE all-time actual arc agreement/initialization per fixed parameter triple. V/alpha/beta/eta fixed. Uncovered fallback is explicit ASTIS convention. No uniform AE all parameters or arbitrary correlated random parameter substitution; path regularity/adaptedness/Markov/invariance/laws/kernel/hypocoercivity/full sampler errors/cost/composition, full Exposition Seal/main merge/PURIFIED/live/whole Goal remain open.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • exists_measurable_piecewise
  • Measurable.sumElim
  • measurable_pi_lambda
  • measurable_pi_apply
  • measurable_real_toNNReal
  • WithTop.measurable_coe
  • measurableSet_le
  • measurableSet_lt
  • Measurable.sub
  • measurable_coe_nnreal_real
  • MeasurableSet.iUnion
  • WithTop.coe_lt_top
  • WithTop.coe_lt_coe
  • Real.toNNReal_pos
  • Set.mem_iUnion
  • Filter.Eventually.and

Mathematical sources

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

Which proof obligations and prerequisites are covered?

  • Formalized proof edge; source adapter/review separate Actual joint measurable physical-time phase, common-AE all-time realization and initialization
  • TODO — not closed by these contributions Path regularity/adaptedness, random-parameter law/kernel, Markov/invariance and full sampler/cost/composition