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

Actual PBPS finite-time full-phase probability kernel

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, arXiv2609.06905v1 AppendixA.1 actual transition law and bounded measurable tests p3.1/p5.2/p6.1. All-finite jointly indexed probability-kernel packaging, exceptional total representative handling and explicit dual integrability are ASTIS elaborations; no path-reversal/invariance/Markov/main completion credit.

arXiv2609.06905v1 · Chen-Chewi-Lu-Zhang arXiv2609.06905v1 AppendixA.1 actual transition operators and bounded measurable tests p3.1/p5.2/p6.1. ASTIS all-finite jointly indexed full-phase probability-kernel elaboration. · 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. In addition, for this same single actual Z there exists a probability kernel K from the jointly indexed space A=(((E×E)×(E×E))×[0,∞)) to the full phase E×E. For every deterministic y,xRef,z0 and finite t≥0, K((((y,xRef),z0),t))=P.map(sample↦Z(y,xRef,z0,t,sample)). Equivalently, for every Borel phase event B, K((((y,xRef),z0),t))(B)=P{sample:Z(y,xRef,z0,t,sample)∈B}. The probability kernel supplies Borel dependence of these event probabilities on all of y,xRef,z0,t simultaneously. At zero time its exact law is K((((y,xRef),z0),0))=δ_z0. For every Borel real-valued test g:E×E→ℝ and every M≥0 satisfying |g(z)|≤M for all z, g is integrable under each displayed K fiber, sample↦g(Z(y,xRef,z0,t,sample)) is integrable under the actual P, and ∫g(z)K((((y,xRef),z0),t))(dz)=∫g(Z(y,xRef,z0,t,sample))P(dsample). The same Z and K precede every parameter, test and bound. All original six analytic assumptions and eleven literal definitions are retained; actual P probability, joint Z measurability, initialization, kernel existence and integrability are derived outputs, never convenience premises. All-finite jointly indexed kernel packaging is an attributed ASTIS measure-theoretic elaboration of the authors actual transition-law and bounded-measurable-test interface. The source terminal failed-limit0 convention and the total uncovered-initial-phase convention are distinct; only fixed-parameter AE compatibility of their laws is used. IsMarkovKernel means probability fibers here and asserts no process memorylessness, restart or Chapman-Kolmogorov equation. Actual invariance, path-law expansion/reversal, AE-safe all-L2 operators/Jensen contraction/density, hypocoercivity, implemented sampling, errors/unbounded query costs, composition and full main results remain separate OPEN obligations.

  • 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.
  • The same single Z supplies all outputs of one K, jointly indexed in deterministic y,xRef,z0 and every finite NNReal time; standing dynamics V,α,β,η stay fixed. The law is the actual exponential-clock full-phase pushforward, not ideal random-reference/momentum returned position at pi.
  • The bounded tests are Borel real g with every nonnegative global bound M; no continuity, differentiability, extra moment, supplied law or integrability premise is added. Rank0 and M=0 are included.
  • Zero-time law uses each fixed-parameter AE initialization; it does not assert all-sample zero-time identity or a common AE event over all parameters. Joint measurability alone does not justify correlated random-parameter substitution.
  • Probability-fiber Markov kernel is distinct from a Markov process. Actual restart/memorylessness/Chapman-Kolmogorov and phase invariance/path reversal remain independent open dependencies; kernel construction is only an optional representation for future invariance proofs.

Actual phase law 1

\[K((y,r,z,t),B)=P\{\omega:Z(y,r,z,t,\omega)\in B\}.\]

Actual phase law 2

\[K((y,r,z,t),E\times E)=1,\qquad K((y,r,z,0),\cdot)=\delta_z.\]

Actual phase law 3

\[g\in L^1(K_{y,r,z,t}),\quad g\circ Z_{y,r,z,t}\in L^1(P)\qquad(|g|\le M).\]

Actual phase law 4

\[\int g\,dK_{y,r,z,t}=\int_\Omega g(Z(y,r,z,t,\omega))\,P(d\omega).\]

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-time full-phase probability kernel

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseTransitionKernel.actual_phase_transition_kernel · 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. In addition, for this same single actual Z there exists a probability kernel K from the jointly indexed space A=(((E×E)×(E×E))×[0,∞)) to the full phase E×E. For every deterministic y,xRef,z0 and finite t≥0, K((((y,xRef),z0),t))=P.map(sample↦Z(y,xRef,z0,t,sample)). Equivalently, for every Borel phase event B, K((((y,xRef),z0),t))(B)=P{sample:Z(y,xRef,z0,t,sample)∈B}. The probability kernel supplies Borel dependence of these event probabilities on all of y,xRef,z0,t simultaneously. At zero time its exact law is K((((y,xRef),z0),0))=δ_z0. For every Borel real-valued test g:E×E→ℝ and every M≥0 satisfying |g(z)|≤M for all z, g is integrable under each displayed K fiber, sample↦g(Z(y,xRef,z0,t,sample)) is integrable under the actual P, and ∫g(z)K((((y,xRef),z0),t))(dz)=∫g(Z(y,xRef,z0,t,sample))P(dsample). The same Z and K precede every parameter, test and bound. All original six analytic assumptions and eleven literal definitions are retained; actual P probability, joint Z measurability, initialization, kernel existence and integrability are derived outputs, never convenience premises. All-finite jointly indexed kernel packaging is an attributed ASTIS measure-theoretic elaboration of the authors actual transition-law and bounded-measurable-test interface. The source terminal failed-limit0 convention and the total uncovered-initial-phase convention are distinct; only fixed-parameter AE compatibility of their laws is used. IsMarkovKernel means probability fibers here and asserts no process memorylessness, restart or Chapman-Kolmogorov equation. Actual invariance, path-law expansion/reversal, AE-safe all-L2 operators/Jensen contraction/density, hypocoercivity, implemented sampling, errors/unbounded query costs, composition and full main results remain separate OPEN obligations.

\[\int g\,dK_{y,r,z,t}=\int_\Omega g(Z(y,r,z,t,\omega))\,P(d\omega).\]
Lean statement · actual_phase_transition_kernel

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. In addition, for this same single actual Z there exists a probability kernel K from the jointly indexed space A=(((E×E)×(E×E))×[0,∞)) to the full phase E×E. For every deterministic y,xRef,z0 and finite t≥0, K((((y,xRef),z0),t))=P.map(sample↦Z(y,xRef,z0,t,sample)). Equivalently, for every Borel phase event B, K((((y,xRef),z0),t))(B)=P{sample:Z(y,xRef,z0,t,sample)∈B}. The probability kernel supplies Borel dependence of these event probabilities on all of y,xRef,z0,t simultaneously. At zero time its exact law is K((((y,xRef),z0),0))=δ_z0. For every Borel real-valued test g:E×E→ℝ and every M≥0 satisfying |g(z)|≤M for all z, g is integrable under each displayed K fiber, sample↦g(Z(y,xRef,z0,t,sample)) is integrable under the actual P, and ∫g(z)K((((y,xRef),z0),t))(dz)=∫g(Z(y,xRef,z0,t,sample))P(dsample). The same Z and K precede every parameter, test and bound. All original six analytic assumptions and eleven literal definitions are retained; actual P probability, joint Z measurability, initialization, kernel existence and integrability are derived outputs, never convenience premises. All-finite jointly indexed kernel packaging is an attributed ASTIS measure-theoretic elaboration of the authors actual transition-law and bounded-measurable-test interface. The source terminal failed-limit0 convention and the total uncovered-initial-phase convention are distinct; only fixed-parameter AE compatibility of their laws is used. IsMarkovKernel means probability fibers here and asserts no process memorylessness, restart or Chapman-Kolmogorov equation. Actual invariance, path-law expansion/reversal, AE-safe all-L2 operators/Jensen contraction/density, hypocoercivity, implemented sampling, errors/unbounded query costs, composition and full main results remain separate OPEN obligations.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem actual_phase_transition_kernel
    {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_phase_transition_kernel_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_phase_transition_kernel_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_phase_transition_kernel_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₀)
      ∧ (∃ K : Kernel (((E × E) × (E × E)) × ℝ≥0) (E × E),
        IsMarkovKernel K ∧
        (∀ y xRef : E, ∀ z₀ : E × E, ∀ t : ℝ≥0,
          K (((y, xRef), z₀), t) = Measure.map (Z y xRef z₀ t) P) ∧
        (∀ y xRef : E, ∀ z₀ : E × E, ∀ t : ℝ≥0,
          ∀ B : Set (E × E), MeasurableSet B →
            K (((y, xRef), z₀), t) B = P ((Z y xRef z₀ t) ⁻¹' B)) ∧
        (∀ y xRef : E, ∀ z₀ : E × E,
          K (((y, xRef), z₀), 0) = Measure.dirac z₀) ∧
        (∀ y xRef : E, ∀ z₀ : E × E, ∀ t : ℝ≥0,
          ∀ g : (E × E) → ℝ, Measurable g →
            ∀ M : ℝ, 0 ≤ M → (∀ z : E × E, |g z| ≤ M) →
              Integrable g (K (((y, xRef), z₀), t)) ∧
              Integrable (fun sample => g (Z y xRef z₀ t sample)) P ∧
              (∫ z, g z ∂K (((y, xRef), z₀), t)) =
                ∫ sample, g (Z y xRef z₀ t sample) ∂P))


set_option maxHeartbeats 1600000 in

Exact module and namespace context

Proof roadmap

  1. 1Keep the actual clocks and the same physical phase

    Use the canonical countable Exp(1) product P and its existing probability theorem. Consume the verified actual physical-time phase producer with exactly the six original analytic assumptions. Its single Z retains joint measurability, every covered live arc, the uncovered-initial-phase convention and the fixed-parameter common-AE all-finite-time/initialization contract. No arbitrary supplied process is substituted.

  2. 2Reassociate the joint parameter and clock coordinates

    Write Param=((y,r),z), A=(Param,t). The measurable evaluation F((a,ω))=Z(y,r,z,t,ω) is obtained from the existing Param×(time×sample) measurable phase by the explicit product reassociation ((Param,t),ω)↦(Param,(t,ω)). Inserting a fixed Param and time gives each measurable clock section. This preserves joint index measurability rather than assuming it from separate sections.

  3. 3Construct the jointly indexed probability kernel and exact fiber law

    At index a, Q=const(P) draws the actual clocks. Kernel.id×Q has fiber δ_a⊗P and is a probability kernel. Push it through measurable F to obtain K. The Dirac-product and map-composition identities give K(a)=map(ω↦F(a,ω))P exactly. Generic Mathlib kernel operations supply measurability and probability; they do not supply process Markovness.

  4. 4Return the unchanged phase contract and identify every Borel event

    Return the same actual Z, all retained deterministic/AE clauses, and the constructed K. For any Borel phase event B, measurable pushforward evaluation gives K(a)(B)=P(Z_a^{-1}(B)). This is equality of the actual full-phase laws for every finite time and deterministic index.

  5. 5Derive zero-time Dirac initialization from the actual AE event

    For each fixed y,r,z, the retained actual AE event implies Z(y,r,z,0,ω)=z for P-almost every ω. Pushforwards of AE-equal functions coincide, so the zero-time law is the pushforward of the constant z. Since P has mass one, this is δ_z. No parameter-uniform AE event or all-sample identity is needed.

  6. 6Prove both integrability statements and transfer the expectation

    For a Borel real g with |g|≤M, measurability and the finite probability of K(a) give g∈L1(K(a)). The measurable actual clock section composed with g is bounded by the same M, hence belongs to L1(P). Rewrite the fiber as the exact pushforward and apply the Bochner integral-map identity. This proves the displayed transition test identity with the actual clocks, including M=0; no unbounded cost transfer or invariance claim follows.

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.
  • The same single Z supplies all outputs of one K, jointly indexed in deterministic y,xRef,z0 and every finite NNReal time; standing dynamics V,α,β,η stay fixed. The law is the actual exponential-clock full-phase pushforward, not ideal random-reference/momentum returned position at pi.
  • The bounded tests are Borel real g with every nonnegative global bound M; no continuity, differentiability, extra moment, supplied law or integrability premise is added. Rank0 and M=0 are included.
  • Zero-time law uses each fixed-parameter AE initialization; it does not assert all-sample zero-time identity or a common AE event over all parameters. Joint measurability alone does not justify correlated random-parameter substitution.
  • Probability-fiber Markov kernel is distinct from a Markov process. Actual restart/memorylessness/Chapman-Kolmogorov and phase invariance/path reversal remain independent open dependencies; kernel construction is only an optional representation for future invariance proofs.

Mathematical proof

1. Keep the actual clocks and the same physical phase

Use the canonical countable Exp(1) product P and its existing probability theorem. Consume the verified actual physical-time phase producer with exactly the six original analytic assumptions. Its single Z retains joint measurability, every covered live arc, the uncovered-initial-phase convention and the fixed-parameter common-AE all-finite-time/initialization contract. No arbitrary supplied process is substituted.

\[P=\bigotimes_{k\ge0}\operatorname{Exp}(1),\qquad P(\Omega)=1.\]
Corresponding Lean step
  classical
  let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
  letI : IsProbabilityMeasure P :=
    AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
  obtain ⟨Z, hZM, harc, hfallback, hgood⟩ :=
    ActualPhysicalTimeMeasurability.actual_physical_time_measurable_phase
      hα hαβ hV hH hη hβη

Exact contiguous compiled BODY region; earlier definitions/facts and enclosing subgoals remain in scope.

2. Reassociate the joint parameter and clock coordinates

Write Param=((y,r),z), A=(Param,t). The measurable evaluation F((a,ω))=Z(y,r,z,t,ω) is obtained from the existing Param×(time×sample) measurable phase by the explicit product reassociation ((Param,t),ω)↦(Param,(t,ω)). Inserting a fixed Param and time gives each measurable clock section. This preserves joint index measurability rather than assuming it from separate sections.

\[F(((\mathrm{Param},t),\omega))=Z(\mathrm{Param},t,\omega).\]
Corresponding Lean step
  let A := ((E × E) × (E × E)) × ℝ≥0
  let F : A × (ℕ → ℝ) → E × E := fun a =>
    Z a.1.1.1.1 a.1.1.1.2 a.1.1.2 a.1.2 a.2
  have hFM : Measurable F := hZM.comp
    (measurable_fst.fst.prodMk (measurable_fst.snd.prodMk measurable_snd))
  have hzM (y xRef : E) (z₀ : E × E) (t : ℝ≥0) :
      Measurable (Z y xRef z₀ t) := hZM.comp
    (show Measurable (fun sample : ℕ → ℝ => (((y, xRef), z₀), t, sample)) from
      measurable_const.prodMk (measurable_const.prodMk measurable_id))

Exact contiguous compiled BODY region; earlier definitions/facts and enclosing subgoals remain in scope.

3. Construct the jointly indexed probability kernel and exact fiber law

At index a, Q=const(P) draws the actual clocks. Kernel.id×Q has fiber δ_a⊗P and is a probability kernel. Push it through measurable F to obtain K. The Dirac-product and map-composition identities give K(a)=map(ω↦F(a,ω))P exactly. Generic Mathlib kernel operations supply measurability and probability; they do not supply process Markovness.

\[K=(\mathrm{id}\times\mathrm{const}(P)).\mathrm{map}(F),\quad K(a)=F(a,\cdot)_*P.\]
Corresponding Lean step
  let Q : Kernel A (ℕ → ℝ) := Kernel.const A P
  let K : Kernel A (E × E) := (Kernel.id ×ₖ Q).map F
  have hK : IsMarkovKernel K := Kernel.IsMarkovKernel.map _ hFM
  have hfiber (y xRef : E) (z₀ : E × E) (t : ℝ≥0) :
      K (((y, xRef), z₀), t) = Measure.map (Z y xRef z₀ t) P := by
    dsimp only [K]
    rw [Kernel.map_apply _ hFM, Kernel.prod_apply, Kernel.id_apply,
      show Q (((y, xRef), z₀), t) = P from rfl,
      Measure.dirac_prod, Measure.map_map hFM (by fun_prop)]
    rfl

Exact contiguous compiled BODY region; earlier definitions/facts and enclosing subgoals remain in scope.

4. Return the unchanged phase contract and identify every Borel event

Return the same actual Z, all retained deterministic/AE clauses, and the constructed K. For any Borel phase event B, measurable pushforward evaluation gives K(a)(B)=P(Z_a^{-1}(B)). This is equality of the actual full-phase laws for every finite time and deterministic index.

\[K((y,r,z,t),B)=P\{\omega:Z(y,r,z,t,\omega)\in B\}.\]
Corresponding Lean step
  refine ⟨Z, hZM, harc, hfallback, hgood, K, hK, hfiber, ?_, ?_, ?_⟩
  · intro y xRef z₀ t B hB
    rw [hfiber, Measure.map_apply (hzM y xRef z₀ t) hB]

Exact contiguous compiled BODY region; earlier definitions/facts and enclosing subgoals remain in scope.

5. Derive zero-time Dirac initialization from the actual AE event

For each fixed y,r,z, the retained actual AE event implies Z(y,r,z,0,ω)=z for P-almost every ω. Pushforwards of AE-equal functions coincide, so the zero-time law is the pushforward of the constant z. Since P has mass one, this is δ_z. No parameter-uniform AE event or all-sample identity is needed.

\[K((y,r,z,t),E\times E)=1,\qquad K((y,r,z,0),\cdot)=\delta_z.\]
Corresponding Lean step
  · intro y xRef z₀
    rw [hfiber]
    calc
      Measure.map (Z y xRef z₀ 0) P =
          Measure.map (fun _ : ℕ → ℝ => z₀) P :=
        Measure.map_congr ((hgood y xRef z₀).mono fun _ hs => hs.2)
      _ = Measure.dirac z₀ := by simp

Exact contiguous compiled BODY region; earlier definitions/facts and enclosing subgoals remain in scope.

6. Prove both integrability statements and transfer the expectation

For a Borel real g with |g|≤M, measurability and the finite probability of K(a) give g∈L1(K(a)). The measurable actual clock section composed with g is bounded by the same M, hence belongs to L1(P). Rewrite the fiber as the exact pushforward and apply the Bochner integral-map identity. This proves the displayed transition test identity with the actual clocks, including M=0; no unbounded cost transfer or invariance claim follows.

\[\int g\,dK_{y,r,z,t}=\int_\Omega g(Z(y,r,z,t,\omega))\,P(d\omega).\]
Corresponding Lean step
  · intro y xRef z₀ t g hg M hM hbound
    letI : IsMarkovKernel K := hK
    have hIntK : Integrable g (K (((y, xRef), z₀), t)) :=
      Integrable.of_bound hg.aestronglyMeasurable M
        (Filter.Eventually.of_forall fun z => by simpa only [Real.norm_eq_abs] using hbound z)
    have hIntP : Integrable (fun sample => g (Z y xRef z₀ t sample)) P :=
      Integrable.of_bound (hg.comp (hzM y xRef z₀ t)).aestronglyMeasurable M
        (Filter.Eventually.of_forall fun sample => by
          simpa only [Real.norm_eq_abs] using hbound (Z y xRef z₀ t sample))
    refine ⟨hIntK, hIntP, ?_⟩
    rw [hfiber]
    exact integral_map (hzM y xRef z₀ t).aemeasurable hg.aestronglyMeasurable

Exact contiguous compiled BODY region; earlier definitions/facts and enclosing subgoals 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_phase_transition_kernel

Keep the actual clocks and the same physical phase; Reassociate the joint parameter and clock coordinates; Construct the jointly indexed probability kernel and exact fiber law; Return the unchanged phase contract and identify every Borel event; Derive zero-time Dirac initialization from the actual AE event; Prove both integrability statements and transfer the expectation

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_phase_transition_kernel
    {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_phase_transition_kernel_statement hα hαβ hV hH hη hβη := by
  classical
  let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
  letI : IsProbabilityMeasure P :=
    AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
  obtain ⟨Z, hZM, harc, hfallback, hgood⟩ :=
    ActualPhysicalTimeMeasurability.actual_physical_time_measurable_phase
      hα hαβ hV hH hη hβη
  let A := ((E × E) × (E × E)) × ℝ≥0
  let F : A × (ℕ → ℝ) → E × E := fun a =>
    Z a.1.1.1.1 a.1.1.1.2 a.1.1.2 a.1.2 a.2
  have hFM : Measurable F := hZM.comp
    (measurable_fst.fst.prodMk (measurable_fst.snd.prodMk measurable_snd))
  have hzM (y xRef : E) (z₀ : E × E) (t : ℝ≥0) :
      Measurable (Z y xRef z₀ t) := hZM.comp
    (show Measurable (fun sample : ℕ → ℝ => (((y, xRef), z₀), t, sample)) from
      measurable_const.prodMk (measurable_const.prodMk measurable_id))
  let Q : Kernel A (ℕ → ℝ) := Kernel.const A P
  let K : Kernel A (E × E) := (Kernel.id ×ₖ Q).map F
  have hK : IsMarkovKernel K := Kernel.IsMarkovKernel.map _ hFM
  have hfiber (y xRef : E) (z₀ : E × E) (t : ℝ≥0) :
      K (((y, xRef), z₀), t) = Measure.map (Z y xRef z₀ t) P := by
    dsimp only [K]
    rw [Kernel.map_apply _ hFM, Kernel.prod_apply, Kernel.id_apply,
      show Q (((y, xRef), z₀), t) = P from rfl,
      Measure.dirac_prod, Measure.map_map hFM (by fun_prop)]
    rfl
  refine ⟨Z, hZM, harc, hfallback, hgood, K, hK, hfiber, ?_, ?_, ?_⟩
  · intro y xRef z₀ t B hB
    rw [hfiber, Measure.map_apply (hzM y xRef z₀ t) hB]
  · intro y xRef z₀
    rw [hfiber]
    calc
      Measure.map (Z y xRef z₀ 0) P =
          Measure.map (fun _ : ℕ → ℝ => z₀) P :=
        Measure.map_congr ((hgood y xRef z₀).mono fun _ hs => hs.2)
      _ = Measure.dirac z₀ := by simp
  · intro y xRef z₀ t g hg M hM hbound
    letI : IsMarkovKernel K := hK
    have hIntK : Integrable g (K (((y, xRef), z₀), t)) :=
      Integrable.of_bound hg.aestronglyMeasurable M
        (Filter.Eventually.of_forall fun z => by simpa only [Real.norm_eq_abs] using hbound z)
    have hIntP : Integrable (fun sample => g (Z y xRef z₀ t sample)) P :=
      Integrable.of_bound (hg.comp (hzM y xRef z₀ t)).aestronglyMeasurable M
        (Filter.Eventually.of_forall fun sample => by
          simpa only [Real.norm_eq_abs] using hbound (Z y xRef z₀ t sample))
    refine ⟨hIntK, hIntP, ?_⟩
    rw [hfiber]
    exact integral_map (hzM y xRef z₀ t).aemeasurable hg.aestronglyMeasurable

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseTransitionKernel

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Actual between-jump phase, exponential clocks and source transition tests.Retain original six analytic hypotheses/eleven literal definitions/full actual phase contract and construct the same-Z actual-clock jointly indexed full-phase kernel.source-implicitExplicit ASTIS measure-theoretic packaging; no arbitrary measurable process or probability premise.
Source terminal failed-limit0 convention; actual initial phase and bounded measurable test operator.Uncovered initial-phase total extension, fixed-parameter AE initialization yields Dirac0; bounded Borel real tests are integrable on both sides with exact expectation transfer.source-implicitDistinct exceptional conventions explicitly retained; fixed-parameter AE law suffices without uniform or correlated substitution.
Path-reversal/invariance, process restart and general L2 operator conclusions are additional source claims.Probability fibers only; future source path law/reversal/invariance/AE-safe contraction/density/process/main obligations stay OPEN.unresolvedSource graph explicitly retains6 future OPEN dependency edges and3 excluded associations; K is an optional law representation, not an invariance or process Markov proof.

Original six analytic hypotheses and all eleven literal actual algorithm definitions/fullactual80 phase clauses retained. Same actual Z precedes the jointly indexed K and every bounded Borel real test. Exact iidExp1 fiber laws, measurable-event identity, probability fibers, Dirac0 and both clock/law integrability with exact expectation transfer only. Source failed-limit0 versus uncovered-z0 conventions agree only at each fixed-parameter AE law. No uniform-parameter AE or arbitrary correlated input substitution. IsMarkovKernel is a probability-fiber class, not process Markov/restart/Chapman-Kolmogorov. Invariance/path-law reversal/fullL2/Jensen contraction/density/hypocoercivity/implemented sampler/error/unbounded expected cost/composition/main/PURIFIED/live/fullpaper/Goal remain OPEN.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • objects: SourceE_(n+1)/clockindex1 becomes literal zeroindexed actualP coordinates and toNNReal support adapter; actual Exp1 laws agree AE. Totaldivision realizesR0=I. No source assumption change. — Native independent review D85-OBJECT-INDEX in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-phase-transition-kernel85/independent-source85/source-review.result85.json; exact module and all six BODY/formula regions bound by run 2a98c62ccd15b723b80363d9e15439a56828d29aab3a1430b37a62017bd2d76a.
  • domains: Coordinate-free finite real Borel E, including rank0, packages sourceEuclidean phase without new dynamics premise. WithTop stopping does not add physical timeinfinity. — Native independent review D85-DOMAIN-EUCLIDEAN in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-phase-transition-kernel85/independent-source85/source-review.result85.json; exact module and all six BODY/formula regions bound by run 2a98c62ccd15b723b80363d9e15439a56828d29aab3a1430b37a62017bd2d76a.
  • quantifiers: Allfinite jointly indexed law measurability explicitly elaborates source actualrecursion/Borelterminal construction. Fixedtuple AE alltime/init remains inherited; no uniformparams or correlatedclock inference. — Native independent review D85-QUANTIFIER-JOINT in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-phase-transition-kernel85/independent-source85/source-review.result85.json; exact module and all six BODY/formula regions bound by run 2a98c62ccd15b723b80363d9e15439a56828d29aab3a1430b37a62017bd2d76a.
  • assumptions: Borelreal g with explicitM>=0 globalbound is the source bounded-test class made explicit, not an extra analytic dynamics assumption. Dualintegrability is derived. — Native independent review D85-ASSUMPTION-TEST in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-phase-transition-kernel85/independent-source85/source-review.result85.json; exact module and all six BODY/formula regions bound by run 2a98c62ccd15b723b80363d9e15439a56828d29aab3a1430b37a62017bd2d76a.
  • conclusion: Actual fullphase law is packaged as one jointly indexed probabilitykernel and exacttestconsumer using existing generic APIs; this is bounded ASTIS integration, not fullPropA1/Markov/invariance. — Native independent review D85-CONCLUSION-KERNEL in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-phase-transition-kernel85/independent-source85/source-review.result85.json; exact module and all six BODY/formula regions bound by run 2a98c62ccd15b723b80363d9e15439a56828d29aab3a1430b37a62017bd2d76a.
  • scopes: Sourcefailedterminal-limit0 and actualuncoveredinitialphase conventions remain distinct. Fixedparameter AE-lawcompatibility suffices; no allsample equality ofversions is claimed. — Native independent review D85-SCOPE-EXCEPTIONAL in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-phase-transition-kernel85/independent-source85/source-review.result85.json; exact module and all six BODY/formula regions bound by run 2a98c62ccd15b723b80363d9e15439a56828d29aab3a1430b37a62017bd2d76a.
  • scopes: Source pathlaw/reversal/invariance/AE-safeJensen/allL2density/restart/CK/main/cost remain OPEN. Sixfuturedependencyedges andthreeexcludedassociations carry no proof credit. — Native independent review D85-SCOPE-GLOBAL in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-phase-transition-kernel85/independent-source85/source-review.result85.json; exact module and all six BODY/formula regions bound by run 2a98c62ccd15b723b80363d9e15439a56828d29aab3a1430b37a62017bd2d76a.
  • constant_dependencies: SameglobalM bounds bothrealtests on finiteprobabilitylaws,includingM0. No additional error/cost/uniformstate/time constant or higherderivative hypothesis. — Native independent review D85-CONSTANT-BOUND in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-phase-transition-kernel85/independent-source85/source-review.result85.json; exact module and all six BODY/formula regions bound by run 2a98c62ccd15b723b80363d9e15439a56828d29aab3a1430b37a62017bd2d76a.

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
  • Original six analytic hypotheses and all eleven literal actual algorithm definitions/fullactual80 phase clauses retained. Same actual Z precedes the jointly indexed K and every bounded Borel real test. Exact iidExp1 fiber laws, measurable-event identity, probability fibers, Dirac0 and both clock/law integrability with exact expectation transfer only. Source failed-limit0 versus uncovered-z0 conventions agree only at each fixed-parameter AE law. No uniform-parameter AE or arbitrary correlated input substitution. IsMarkovKernel is a probability-fiber class, not process Markov/restart/Chapman-Kolmogorov. Invariance/path-law reversal/fullL2/Jensen contraction/density/hypocoercivity/implemented sampler/error/unbounded expected cost/composition/main/PURIFIED/live/fullpaper/Goal remain OPEN.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • Kernel.map
  • Kernel.IsMarkovKernel.map
  • Kernel.prod_apply
  • Kernel.id_apply
  • Measure.dirac_prod
  • Measure.map_map
  • Measure.map_apply
  • Measure.map_congr
  • Measure.map_const
  • Integrable.of_bound
  • integral_map

Mathematical sources

  • Chen-Chewi-Lu-Zhang arXiv2609.06905v1 AppendixA.1 actual transition operators and bounded measurable tests p3.1/p5.2/p6.1. ASTIS all-finite jointly indexed full-phase probability-kernel elaboration. — Original six analytic hypotheses and all eleven literal actual algorithm definitions/fullactual80 phase clauses retained. Same actual Z precedes the jointly indexed K and every bounded Borel real test. Exact iidExp1 fiber laws, measurable-event identity, probability fibers, Dirac0 and both clock/law integrability with exact expectation transfer only. Source failed-limit0 versus uncovered-z0 conventions agree only at each fixed-parameter AE law. No uniform-parameter AE or arbitrary correlated input substitution. IsMarkovKernel is a probability-fiber class, not process Markov/restart/Chapman-Kolmogorov. Invariance/path-law reversal/fullL2/Jensen contraction/density/hypocoercivity/implemented sampler/error/unbounded expected cost/composition/main/PURIFIED/live/fullpaper/Goal remain OPEN.

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

Which proof obligations and prerequisites are covered?

  • Formalized proof edge; source adapter/review separate Actual jointly indexed full-phase law, Dirac0 and bounded Borel expectation transfer
  • TODO — not closed by these contributions Path-law/reversal/invariance/restart/Markov/fullL2/main/implementation/cost/composition