Actual PBPS: detailed balance after independent reference averaging

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang. ASTIS completes the measurable-indicator, finite signed Fubini and same-actual-witness details; this is not a complete paper.

Complete source statement (Samplinglib restatement)

Let E be a finite-dimensional real inner-product Borel space. Assume V is C2, 0<alpha<=beta, alpha||v||^2<=D2V(x)[v,v]<=beta||v||^2 for every x,v, eta>0 and beta eta<=1. For each y let q_y be the normalized law proportional to exp(-V(x)-||x-y||^2/(2 eta)) dx. Draw the reference r from q_y, momentum p from the standard Gaussian and unit exponential clocks independently. Run the actual fixed-reference flow to time pi and return its position. The SAME global jointly measurable probability kernel H(y,x) given by this literal pushforward satisfies detailed balance with q_y for EVERY y. The existing raw covered-arc and fallback equations, parameterwise clock-AE interval coverage, local zero-time law and half-turn initialization outputs are retained. None of these construction, normalization, probability or integrability facts is a new hypothesis.

Exact conditional detailed balance

Reference independence makes the average symmetric

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: detailed balance after independent reference averaging

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHalfTurnReversibility.actual_half_turn_reversible · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product Borel space. Assume V is C2, 0<alpha≤beta, alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for every x,v, eta>0 and beta eta≤1. For each y let q_y be the normalized law proportional to exp(-V(x)-||x-y||^2/(2 eta)) dx. Draw the reference r from q_y, momentum p from the standard Gaussian and unit exponential clocks independently. Run the actual fixed-reference flow to time pi and return its position. The SAME global jointly measurable probability kernel H(y,x) given by this literal pushforward satisfies detailed balance with q_y for EVERY y. The existing raw covered-arc and fallback equations, parameterwise clock-AE interval coverage, local zero-time law and half-turn initialization outputs are retained. None of these construction, normalization, probability or integrability facts is a new hypothesis.

\[q_y(dx)=\frac{e^{-V(x)-\|x-y\|^2/(2\eta)}}{Z_y}\,dx,\qquad\forall y\ \forall A,B\text{ measurable}:\ \int_A^-H(y,x)(B)\,q_y(dx)=\int_B^-H(y,x)(A)\,q_y(dx).\]

Lean statement · actual_half_turn_reversible

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_half_turn_reversible
    {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_half_turn_reversibility_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_half_turn_reversibility_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.

Download module (.lean)

private def actual_half_turn_reversibility_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 _ => ⊤)
    let q : E → Measure E := fun y =>
      (volume : Measure E).tilted (fun x => -V x - ‖x - y‖ ^ 2 / (2 * η))
    let γ : Measure E := stdGaussian E
    let M : E → Measure ((E × E) × (ℕ → ℝ)) := fun y => ((q y).prod γ).prod P
    let tπ : ℝ≥0 := ⟨Real.pi, Real.pi_pos.le⟩
    ∃ 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₀) ∧
      ∃ R : Kernel E E, IsMarkovKernel R ∧ (∀ y : E, R y = q y) ∧
      ∃ H : Kernel (E × E) E, IsMarkovKernel H ∧
      (∀ y : E, (H.comap (fun x : E => (y, x)) (by fun_prop)).IsReversible (q y)) ∧
      (∀ y x : E, H (y, x) = Measure.map
        (fun w : (E × E) × (ℕ → ℝ) => (Z y w.1.1 (x, w.1.2) tπ w.2).1)
        (M y)) ∧
      (∀ y x : E, Measure.map
        (fun w : (E × E) × (ℕ → ℝ) => Z y w.1.1 (x, w.1.2) 0 w.2)
        (M y) = (Measure.dirac x).prod γ) ∧
      (∀ y x : E, ∀ᵐ w ∂M y,
        Z y w.1.1 (x, w.1.2) 0 w.2 = (x, w.1.2) ∧
        ∃ n : ℕ, ∃ a : ℝ≥0 × (E × E),
          eventTime y w.1.1 (x, w.1.2) (ε w.2) n ≤ (tπ : WithTop ℝ≥0) ∧
          (tπ : WithTop ℝ≥0) < eventTime y w.1.1 (x, w.1.2) (ε w.2) (n + 1) ∧
          record y w.1.1 (x, w.1.2) (ε w.2) n = Sum.inl a ∧ a.1 ≤ tπ ∧
          ((tπ - a.1 : ℝ≥0) : WithTop ℝ≥0) < τ y w.1.1 a.2 (ε w.2 n) ∧
          Z y w.1.1 (x, w.1.2) tπ w.2 = Φ y w.1.1 ((tπ - a.1 : ℝ≥0) : ℝ) a.2)

Exact module and namespace context

Proof roadmap

1Identify the actual path, including exceptional raw clocks
The kernel construction and the signed-duality construction prescribe the same recursion. On a covered interval their live record gives the same harmonic arc; a dead record cannot bracket a finite time. When no interval covers the time, both use the existing initial-state fallback. The two global path witnesses therefore agree pointwise, before taking any expectation.
2Keep the literal independent-reference kernel
The existing reference kernel identifies q_y as a probability law for every y. Gaussian momentum and the clock product are also probability laws. Joint measurability of Z makes the returned-position map measurable in input, reference, momentum and clocks. Restrict the joint kernel to a fixed y; its fiber law is exactly the displayed pushforward, not an arbitrary reversible replacement.
3Remove both momentum flips from bounded position tests
Lift measurable functions f,g bounded in absolute value by1 to phase space using the position projection. The momentum flip leaves both lifts unchanged. Actual bounded signed phase duality therefore gives a symmetric pairing for each fixed reference r. The two written forms of the Gibbs potential are identified by real algebra.
4Average the reference only after proving signed Fubini conditions
Joint measurability gives a measurable clock expectation. Probability and |g|≤1 imply |E_w g|≤1; hence |f E_w g|≤1. These products are integrable under q_y times q_y times gamma, and the raw clock integrands are integrable under the corresponding product with P. Signed Fubini can now exchange input x and independent reference r. Integrating the fixed-reference symmetry yields symmetry of the actual kernel pairing.
5Convert measurable indicators to exact rectangle detailed balance
Choose f=1_A and g=1_B for measurable A,B. Each kernel fiber has finite mass one. Mathlib identifies the integral of an indicator with its real measure; nonnegative finite integration identifies its ofReal value with the ENNReal rectangle flux. Symmetry therefore gives the defining identity of Kernel.IsReversible on all measurable rectangles.

Full assumptions and notation

All objects and hypotheses

Exactly the six analytic assumptions in the statement; finite real Hilbert Borel E includes dimension zero.
Literal flow: c=y-eta grad V(r); x_t=c+cos(t)(x-c)+sqrt(eta)sin(t)p, p_t=-sin(t)(x-c)/sqrt(eta)+cos(t)p. Bounce reflects in grad V(x)-grad V(r), with identity at zero normal; rate sqrt(eta)max(0,<p,grad V(x)-grad V(r)>).
Independent unit exponential thresholds, integrated-hazard hitting times and the existing raw initial-state fallback define Z. The full literal recursion and retained outputs are available in the folded proposition.
Normalization, probability, joint measurability, integrability and detailed balance are derived, not extra source binders. AE initialization/coverage is parameterwise; no common null set uniform in every parameter is asserted.

Mathematical proof

1. Identify the actual path, including exceptional raw clocks

The kernel construction and the signed-duality construction prescribe the same recursion. On a covered interval their live record gives the same harmonic arc; a dead record cannot bracket a finite time. When no interval covers the time, both use the existing initial-state fallback. The two global path witnesses therefore agree pointwise, before taking any expectation.

\[Z_{\rm law}(y,r,z,t,w)=Z_{\rm dual}(y,r,z,t,w).\]

Corresponding Lean step

  obtain ⟨Z, hZM, hZa, hZf, hgood, R, hR, hRq, H, hHK, hHlaw, hH0, hHgood⟩ :=
    IdealHalfTurnKernel.ideal_half_turn_returned_position_kernel hα hαβ hV hH hη hβη
  refine ⟨Z, hZM, hZa, hZf, hgood, R, hR, hRq, H, hHK, ?_, hHlaw, hH0, hHgood⟩
  obtain ⟨Zb, _hZbm, hZba, hZbf, _hZb0, hD⟩ :=
    ActualBoundedGibbsDuality.actual_bounded_gibbs_duality hα hαβ hV hH hη hβη
  have hZd : Zb = Z := by
    funext y r z t w
    by_cases hw : ∃ n : ℕ, eventTime y r z (ε w) n ≤ (t : WithTop ℝ≥0) ∧
        (t : WithTop ℝ≥0) < eventTime y r z (ε w) (n + 1)
    · obtain ⟨n, hn, hn'⟩ := hw
      cases hr : record y r z (ε w) n with
      | inl a =>
          exact (hZba y r z w t n a (by exact ⟨hn, hn'⟩) hr).trans
            (hZa y r z w t n a hn hn' hr).symm
      | inr a =>
          have hnot : ¬ (⊤ : WithTop ℝ≥0) ≤ (t : WithTop ℝ≥0) :=
            WithTop.not_top_le_coe t
          apply False.elim
          apply hnot
          simpa only [eventTime, hr, Sum.elim_inr] using hn
    · exact (hZbf y r z w t hw).trans (hZf y r z w t hw).symm
  subst Zb

This is equality for all raw inputs, not an informal identification of laws or a common null event over all parameters.

2. Keep the literal independent-reference kernel

The existing reference kernel identifies q_y as a probability law for every y. Gaussian momentum and the clock product are also probability laws. Joint measurability of Z makes the returned-position map measurable in input, reference, momentum and clocks. Restrict the joint kernel to a fixed y; its fiber law is exactly the displayed pushforward, not an arbitrary reversible replacement.

\[\kappa_y(x)=\bigl[(r,p,w)\mapsto\operatorname{fst}Z(y,r,(x,p),\pi,w)\bigr]_{\#}(q_y\otimes\gamma\otimes P).\]

Corresponding Lean step

  letI : IsMarkovKernel R := hR
  letI : IsMarkovKernel H := hHK
  letI : IsProbabilityMeasure P :=
    AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
  letI : IsProbabilityMeasure γ := inferInstanceAs (IsProbabilityMeasure (stdGaussian E))
  intro y
  letI : IsProbabilityMeasure (q y) := by
    have he : R y = q y := hRq y
    rw [← he]
    infer_instance
  let κ : Kernel E E := H.comap (fun x : E => (y, x)) (by fun_prop)
  let F : E → E → E → (ℕ → ℝ) → E := fun r x p w => (Z y r (x, p) tπ w).1
  have hFM : Measurable (fun a : ((E × E) × E) × (ℕ → ℝ) =>
      F a.1.1.2 a.1.1.1 a.1.2 a.2) :=
    (hZM.comp (((measurable_const.prodMk measurable_fst.fst.snd).prodMk
      (measurable_fst.fst.fst.prodMk measurable_fst.snd)).prodMk
      (measurable_const.prodMk measurable_snd))).fst
  have hKl (x : E) : κ x = Measure.map
      (fun a : (E × E) × (ℕ → ℝ) => F a.1.1 x a.1.2 a.2)
      (((q y).prod γ).prod P) := hHlaw y x
  apply reversible_of_reference_average (q y) γ P F hFM κ hKl

The reference distribution q_y does not depend on the current input x. Global warm-start initialization is not supplied or proved here.

3. Remove both momentum flips from bounded position tests

Lift measurable functions f,g bounded in absolute value by1 to phase space using the position projection. The momentum flip leaves both lifts unchanged. Actual bounded signed phase duality therefore gives a symmetric pairing for each fixed reference r. The two written forms of the Gibbs potential are identified by real algebra.

\[\int f(x)\,\mathbb E_w g(\operatorname{fst}Z_{y,r,(x,p),\pi}(w))\,q_y(dx)\gamma(dp)=\int g(x)\,\mathbb E_w f(\operatorname{fst}Z_{y,r,(x,p),\pi}(w))\,q_y(dx)\gamma(dp).\]

Corresponding Lean step

  intro r f g hf hg hfb hgb
  have hbd := (hD y r tπ).2 (fun z : E × E => f z.1)
    (fun z : E × E => g z.1) 1 1 (hf.comp measurable_fst)
    (hg.comp measurable_fst) zero_le_one zero_le_one
    (fun z => hfb z.1) (fun z => hgb z.1)
  have hflux := hbd.2.2
  have hqeq : (volume : Measure E).tilted
      (fun x => -(V x + ‖x - y‖ ^ 2 / (2 * η))) = q y := by
    apply congrArg (fun U : E → ℝ => (volume : Measure E).tilted U)
    funext x
    ring
  change (∫ z : E × E, f z.1 * (∫ w, g (Z y r z tπ w).1 ∂P)
      ∂((volume : Measure E).tilted
        (fun x => -(V x + ‖x - y‖ ^ 2 / (2 * η)))).prod γ) =
    (∫ z : E × E, g z.1 * (∫ w, f (Z y r z tπ w).1 ∂P)
      ∂((volume : Measure E).tilted
        (fun x => -(V x + ‖x - y‖ ^ 2 / (2 * η)))).prod γ) at hflux
  rw [hqeq] at hflux
  exact hflux

This is the bounded-test adapter to the source operator proof, not a claim that a temporal semigroup has been constructed.

4. Average the reference only after proving signed Fubini conditions

Joint measurability gives a measurable clock expectation. Probability and |g|≤1 imply |E_w g|≤1; hence |f E_w g|≤1. These products are integrable under q_y times q_y times gamma, and the raw clock integrands are integrable under the corresponding product with P. Signed Fubini can now exchange input x and independent reference r. Integrating the fixed-reference symmetry yields symmetry of the actual kernel pairing.

\[\langle f,\kappa_y g\rangle_{q_y}=\int q_y(dr)\int q_y(dx)\gamma(dp)\,f(x)\mathbb E_w g(\operatorname{fst}Z_{y,r,(x,p),\pi}(w)).\]

Corresponding Lean step

private theorem pairing_eq_reference_average
    {X Y W : Type*} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace W]
    (q : Measure X) (γ : Measure Y) (P : Measure W)
    [IsProbabilityMeasure q] [IsProbabilityMeasure γ] [IsProbabilityMeasure P]
    (F : X → X → Y → W → X)
    (hF : Measurable (fun a : ((X × X) × Y) × W =>
      F a.1.1.2 a.1.1.1 a.1.2 a.2))
    (κ : Kernel X X)
    (hlaw : ∀ x, κ x = Measure.map
      (fun a : (X × Y) × W => F a.1.1 x a.1.2 a.2) ((q.prod γ).prod P))
    (f g : X → ℝ) (hf : Measurable f) (hg : Measurable g)
    (hfb : ∀ x, |f x| ≤ 1) (hgb : ∀ x, |g x| ≤ 1) :
    (∫ x, f x * (∫ z, g z ∂κ x) ∂q) =
      ∫ r, (∫ z : X × Y, f z.1 * (∫ w, g (F r z.1 z.2 w) ∂P)
        ∂q.prod γ) ∂q := by
  let op : X → X → Y → ℝ := fun x r p => ∫ w, g (F r x p w) ∂P
  have hopm : Measurable (fun a : (X × X) × Y => op a.1.1 a.1.2 a.2) :=
    (hg.comp hF).stronglyMeasurable.integral_prod_right'.measurable
  have hopb (x r : X) (p : Y) : |op x r p| ≤ 1 := by
    have hh := norm_integral_le_of_norm_le_const (μ := P)
      (f := fun w => g (F r x p w))
      (Eventually.of_forall fun w => by
        simpa only [Real.norm_eq_abs] using hgb (F r x p w))
    simpa [op] using hh
  have hdb (x r : X) (p : Y) : |f x * op x r p| ≤ 1 := by
    calc
      |f x * op x r p| = |f x| * |op x r p| := abs_mul _ _
      _ ≤ 1 * 1 := mul_le_mul (hfb x) (hopb x r p) (abs_nonneg _) zero_le_one
      _ = 1 := mul_one 1
  have hdm : Measurable (fun a : (X × X) × Y =>
      f a.1.1 * op a.1.1 a.1.2 a.2) := (hf.comp measurable_fst.fst).mul hopm
  have hdi : Integrable (fun a : (X × X) × Y =>
      f a.1.1 * op a.1.1 a.1.2 a.2) ((q.prod q).prod γ) :=
    Integrable.of_bound hdm.aestronglyMeasurable 1
      (Eventually.of_forall fun a => by
        simpa only [Real.norm_eq_abs] using hdb a.1.1 a.1.2 a.2)
  have hinner (x : X) : (∫ z, g z ∂κ x) = ∫ r, ∫ p, op x r p ∂γ ∂q := by
    have hfx : Measurable (fun a : (X × Y) × W => F a.1.1 x a.1.2 a.2) :=
      hF.comp (((measurable_const.prodMk measurable_fst.fst).prodMk
        measurable_fst.snd).prodMk measurable_snd)
    have hi : Integrable (fun a : (X × Y) × W => g (F a.1.1 x a.1.2 a.2))
        ((q.prod γ).prod P) :=
      Integrable.of_bound (hg.comp hfx).aestronglyMeasurable 1
        (Eventually.of_forall fun a => by
          simpa only [Real.norm_eq_abs] using hgb (F a.1.1 x a.1.2 a.2))
    rw [hlaw x, integral_map hfx.aemeasurable hg.aestronglyMeasurable,
      integral_prod _ hi]
    exact integral_prod _ hi.integral_prod_left
  calc
    (∫ x, f x * (∫ z, g z ∂κ x) ∂q) =
        ∫ x, ∫ r, ∫ p, f x * op x r p ∂γ ∂q ∂q := by
      simp_rw [hinner, ← integral_const_mul]
    _ = ∫ r, ∫ x, ∫ p, f x * op x r p ∂γ ∂q ∂q :=
      integral_integral_swap hdi.integral_prod_left
    _ = ∫ r, (∫ z : X × Y, f z.1 * (∫ w, g (F r z.1 z.2 w) ∂P)
        ∂q.prod γ) ∂q := by
      apply integral_congr_ae
      exact Eventually.of_forall fun r => by
        have hm : Measurable (fun z : X × Y => f z.1 * op z.1 r z.2) :=
          hdm.comp ((measurable_fst.prodMk measurable_const).prodMk measurable_snd)
        have hi : Integrable (fun z : X × Y => f z.1 * op z.1 r z.2)
            (q.prod γ) :=
          Integrable.of_bound hm.aestronglyMeasurable 1
            (Eventually.of_forall fun z => by
              simpa only [Real.norm_eq_abs] using hdb z.1 r z.2)
        exact (integral_prod _ hi).symm

/-- Combine the exact raw returned law with fixed-reference bounded position duality. -/
private theorem reversible_of_reference_average
    {X Y W : Type*} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace W]
    (q : Measure X) (γ : Measure Y) (P : Measure W)
    [IsProbabilityMeasure q] [IsProbabilityMeasure γ] [IsProbabilityMeasure P]
    (F : X → X → Y → W → X)
    (hF : Measurable (fun a : ((X × X) × Y) × W =>
      F a.1.1.2 a.1.1.1 a.1.2 a.2))
    (κ : Kernel X X) [IsMarkovKernel κ]
    (hlaw : ∀ x, κ x = Measure.map
      (fun a : (X × Y) × W => F a.1.1 x a.1.2 a.2) ((q.prod γ).prod P))
    (hdual : ∀ r : X, ∀ f g : X → ℝ, Measurable f → Measurable g →
      (∀ x, |f x| ≤ 1) → (∀ x, |g x| ≤ 1) →
      (∫ z : X × Y, f z.1 * (∫ w, g (F r z.1 z.2 w) ∂P) ∂q.prod γ) =
        ∫ z : X × Y, g z.1 * (∫ w, f (F r z.1 z.2 w) ∂P) ∂q.prod γ) :
    κ.IsReversible q := by
  apply reversible_of_bounded_pairing q κ
  intro f g hf hg hfb hgb
  rw [pairing_eq_reference_average q γ P F hF κ hlaw f g hf hg hfb hgb,
    pairing_eq_reference_average q γ P F hF κ hlaw g f hg hf hgb hfb]
  exact integral_congr_ae (Eventually.of_forall fun r => hdual r f g hf hg hfb hgb)

No unbounded reference-energy moment, integration over y, or transfer of an unbounded cost by TV proximity is used.

5. Convert measurable indicators to exact rectangle detailed balance

Choose f=1_A and g=1_B for measurable A,B. Each kernel fiber has finite mass one. Mathlib identifies the integral of an indicator with its real measure; nonnegative finite integration identifies its ofReal value with the ENNReal rectangle flux. Symmetry therefore gives the defining identity of Kernel.IsReversible on all measurable rectangles.

\[\int_A^-\kappa_y(x,B)\,q_y(dx)=\operatorname{ofReal}\langle\mathbf1_A,\kappa_y\mathbf1_B\rangle=\operatorname{ofReal}\langle\mathbf1_B,\kappa_y\mathbf1_A\rangle=\int_B^-\kappa_y(x,A)\,q_y(dx).\]

Corresponding Lean step

private theorem flux_ofReal
    {X : Type*} [MeasurableSpace X] (μ : Measure X) [IsFiniteMeasure μ]
    (κ : Kernel X X) [IsMarkovKernel κ]
    {A B : Set X} (hA : MeasurableSet A) (hB : MeasurableSet B) :
    ENNReal.ofReal (∫ x, A.indicator (fun _ => (1 : ℝ)) x *
      (∫ z, B.indicator (fun _ => (1 : ℝ)) z ∂κ x) ∂μ) =
      ∫⁻ x in A, κ x B ∂μ := by
  have hi : Integrable (fun x => (κ x).real B) (μ.restrict A) := by
    apply Integrable.of_bound
      (κ.measurable_coe hB).ennreal_toReal.aestronglyMeasurable 1
    exact Eventually.of_forall fun x => by
      simpa only [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg,
        Measure.real] using
        (measureReal_le_one (μ := κ x) (s := B))
  have hreal : (∫ x, A.indicator (fun _ => (1 : ℝ)) x *
      (∫ z, B.indicator (fun _ => (1 : ℝ)) z ∂κ x) ∂μ) =
      ∫ x in A, (κ x).real B ∂μ := by
    have hIB (x : X) : (∫ z, B.indicator (fun _ => (1 : ℝ)) z ∂κ x) =
        (κ x).real B := integral_indicator_one hB
    simp_rw [hIB]
    rw [← integral_indicator hA]
    congr 1
    funext x
    by_cases hx : x ∈ A <;> simp [hx]
  rw [hreal, ofReal_integral_eq_lintegral_ofReal hi
    (Eventually.of_forall fun _ => measureReal_nonneg)]
  apply lintegral_congr_ae
  exact Eventually.of_forall fun x => ENNReal.ofReal_toReal (measure_ne_top (κ x) B)

/-- Test symmetry on measurable indicators; no countability/singleton criterion. -/
private theorem reversible_of_bounded_pairing
    {X : Type*} [MeasurableSpace X] (μ : Measure X) [IsFiniteMeasure μ]
    (κ : Kernel X X) [IsMarkovKernel κ]
    (hsym : ∀ f g : X → ℝ, Measurable f → Measurable g →
      (∀ x, |f x| ≤ 1) → (∀ x, |g x| ≤ 1) →
      (∫ x, f x * (∫ z, g z ∂κ x) ∂μ) =
        ∫ x, g x * (∫ z, f z ∂κ x) ∂μ) : κ.IsReversible μ := by
  intro A B hA hB
  rw [← flux_ofReal μ κ hA hB, ← flux_ofReal μ κ hB hA]
  congr 1
  apply hsym _ _ (measurable_const.indicator hA) (measurable_const.indicator hB)
  · intro x
    by_cases hx : x ∈ A <;> simp [hx]
  · intro x
    by_cases hx : x ∈ B <;> simp [hx]

The criterion works on atomless E. The countable-state singleton-balance lemma is inapplicable. The private adapters below are not additional Registry leaves.

Lean verification

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

Lean proof · actual_half_turn_reversible

Same literal Z -> exact probability kernel -> position lifts absorb flips -> bounded signed reference Fubini -> measurable-rectangle detailed balance.

Download module (.lean)

theorem actual_half_turn_reversible
    {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_half_turn_reversibility_statement hα hαβ hV hH hη hβη := by
  classical
  unfold actual_half_turn_reversibility_statement
  intro P ε c Φ S rate Λ τ next record eventTime q γ M tπ
  obtain ⟨Z, hZM, hZa, hZf, hgood, R, hR, hRq, H, hHK, hHlaw, hH0, hHgood⟩ :=
    IdealHalfTurnKernel.ideal_half_turn_returned_position_kernel hα hαβ hV hH hη hβη
  refine ⟨Z, hZM, hZa, hZf, hgood, R, hR, hRq, H, hHK, ?_, hHlaw, hH0, hHgood⟩
  obtain ⟨Zb, _hZbm, hZba, hZbf, _hZb0, hD⟩ :=
    ActualBoundedGibbsDuality.actual_bounded_gibbs_duality hα hαβ hV hH hη hβη
  have hZd : Zb = Z := by
    funext y r z t w
    by_cases hw : ∃ n : ℕ, eventTime y r z (ε w) n ≤ (t : WithTop ℝ≥0) ∧
        (t : WithTop ℝ≥0) < eventTime y r z (ε w) (n + 1)
    · obtain ⟨n, hn, hn'⟩ := hw
      cases hr : record y r z (ε w) n with
      | inl a =>
          exact (hZba y r z w t n a (by exact ⟨hn, hn'⟩) hr).trans
            (hZa y r z w t n a hn hn' hr).symm
      | inr a =>
          have hnot : ¬ (⊤ : WithTop ℝ≥0) ≤ (t : WithTop ℝ≥0) :=
            WithTop.not_top_le_coe t
          apply False.elim
          apply hnot
          simpa only [eventTime, hr, Sum.elim_inr] using hn
    · exact (hZbf y r z w t hw).trans (hZf y r z w t hw).symm
  subst Zb
  letI : IsMarkovKernel R := hR
  letI : IsMarkovKernel H := hHK
  letI : IsProbabilityMeasure P :=
    AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
  letI : IsProbabilityMeasure γ := inferInstanceAs (IsProbabilityMeasure (stdGaussian E))
  intro y
  letI : IsProbabilityMeasure (q y) := by
    have he : R y = q y := hRq y
    rw [← he]
    infer_instance
  let κ : Kernel E E := H.comap (fun x : E => (y, x)) (by fun_prop)
  let F : E → E → E → (ℕ → ℝ) → E := fun r x p w => (Z y r (x, p) tπ w).1
  have hFM : Measurable (fun a : ((E × E) × E) × (ℕ → ℝ) =>
      F a.1.1.2 a.1.1.1 a.1.2 a.2) :=
    (hZM.comp (((measurable_const.prodMk measurable_fst.fst.snd).prodMk
      (measurable_fst.fst.fst.prodMk measurable_fst.snd)).prodMk
      (measurable_const.prodMk measurable_snd))).fst
  have hKl (x : E) : κ x = Measure.map
      (fun a : (E × E) × (ℕ → ℝ) => F a.1.1 x a.1.2 a.2)
      (((q y).prod γ).prod P) := hHlaw y x
  apply reversible_of_reference_average (q y) γ P F hFM κ hKl
  intro r f g hf hg hfb hgb
  have hbd := (hD y r tπ).2 (fun z : E × E => f z.1)
    (fun z : E × E => g z.1) 1 1 (hf.comp measurable_fst)
    (hg.comp measurable_fst) zero_le_one zero_le_one
    (fun z => hfb z.1) (fun z => hgb z.1)
  have hflux := hbd.2.2
  have hqeq : (volume : Measure E).tilted
      (fun x => -(V x + ‖x - y‖ ^ 2 / (2 * η))) = q y := by
    apply congrArg (fun U : E → ℝ => (volume : Measure E).tilted U)
    funext x
    ring
  change (∫ z : E × E, f z.1 * (∫ w, g (Z y r z tπ w).1 ∂P)
      ∂((volume : Measure E).tilted
        (fun x => -(V x + ‖x - y‖ ^ 2 / (2 * η)))).prod γ) =
    (∫ z : E × E, g z.1 * (∫ w, f (Z y r z tπ w).1 ∂P)
      ∂((volume : Measure E).tilted
        (fun x => -(V x + ‖x - y‖ ^ 2 / (2 * η)))).prod γ) at hflux
  rw [hqeq] at hflux
  exact hflux

end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHalfTurnReversibility

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Euclidean conditional half-turn under the paper standing Hessian and eta regime.	Same six analytic hypotheses on finite real Hilbert Borel E, including rank zero.	generalization	Isometric coordinates preserve the actual flow, Gaussian, volume and rectangle law; no extra analytic binder.
A.2 averages fixed-reference self-adjoint Markov contractions, then states detailed balance.	The bounded-position-test adapter uses actual signed phase duality, proves all joint/product integrability and applies measurable indicators to the SAME literal returned kernel.	source-implicit	An explicit elementary adapter to the source route, not a new reversibility/integrability premise or an assumed Markov semigroup.
A.2 continues to the augmented-space all-L2 operator; later sections prove invariance, hypocoercivity and complexity.	Conditional detailed balance for the same actual returned-position kernel only. No temporal restart/semigroup, augmented all-L2 operator, hypocoercive rate, capped implementation, error/cost, global warm start, composition or complete paper.	unresolved	Conditional detailed balance does not discharge the later augmented, convergence or actual-cost obligations.

Conditional detailed balance for the same actual returned-position kernel only. No temporal restart/semigroup, augmented all-L2 operator, hypocoercive rate, capped implementation, error/cost, global warm start, composition or complete paper.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

scopes: The implementation proves the conditional kernel claim via bounded signed phase tests, signed Fubini and indicator flux conversion. It does not claim to have implemented the source A.2 all-L2 self-adjoint-contraction argument. This proof-route distinction is explicit and does not weaken detailed balance. — Independent source review classification: source-faithful-sufficient-proof-adapter; nonblocking.
objects: The theorem fixes the existing initial-state fallback on uncovered raw clocks; A.2 describes a zero extension of a terminal limit off its existence set. These raw versions need not agree on exceptional samples. The source process law and target kernel are compared on their full-measure valid paths, with separate retained parameterwise/mixed AE coverage. The public proof identifies its two actual witnesses using the SAME fallback pointwise, so it does not change the returned law or assume canonical raw-version equality with the source zero extension. — Independent source review classification: explicit-representative-elaboration; nonblocking.
quantifiers: The expanded target retains one jointly measurable raw process and global kernels, all raw equations and local initialization laws from the imported construction. These are conclusions, not new premises. They make the actual-law identity auditable without promoting parameterwise AE coverage into a universal common full set. — Independent source review classification: explicit-construction-elaboration; nonblocking.

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

Conditional detailed balance for the same actual returned-position kernel only. No temporal restart/semigroup, augmented all-L2 operator, hypocoercive rate, capped implementation, error/cost, global warm start, composition or complete paper.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.Integrable.of_bound
MeasureTheory.integral_indicator_one
MeasureTheory.ofReal_integral_eq_lintegral_ofReal
MeasureTheory.integral_map
MeasureTheory.integral_prod
MeasureTheory.integral_integral_swap
MeasureTheory.StronglyMeasurable.integral_prod_right
ProbabilityTheory.Kernel.IsReversible

Mathematical sources

Proposition3.2, A.1 bounded duality819-820 and A.2 proof832-853 — Conditional detailed balance for the same actual returned-position kernel only. No temporal restart/semigroup, augmented all-L2 operator, hypocoercive rate, capped implementation, error/cost, global warm start, composition or complete paper.

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

Actual PBPS: detailed balance after independent reference averaging

Complete source statement (Samplinglib restatement)

Exact conditional detailed balance

Reference independence makes the average symmetric

Read the formalized proofs

Actual PBPS: detailed balance after independent reference averaging

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Identify the actual path, including exceptional raw clocks

2. Keep the literal independent-reference kernel

3. Remove both momentum flips from bounded position tests

4. Average the reference only after proving signed Fubini conditions

5. Convert measurable indicators to exact rectangle detailed balance

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?