Actual PBPS finite-time full-phase probability kernel

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.

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βη

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

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.