Actual PBPS zero-safe bounce, rate and energy-layer bound

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, arXiv:2609.06905v1, Section2 Eq2.4, Section3 Eq3.4, Algorithm1 steps6–7 and AppendixA.1 Ex4–6. ASTIS proves omitted deterministic/Borel estimates; Proposition3.1 stochastic construction is a later consumer.

Complete source statement (Samplinglib restatement)

Let E be a finite-dimensional real inner-product Borel space, including rank zero. Let V:E→ℝ be C² on all E, let α,β≥0 satisfy 0<α≤β and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, and let η>0 with βη≤1. For all y,xRef∈E define c=y−η∇V(xRef), h(xRef,x)=∇V(x)−∇V(xRef), R(n,p)=p−(2⟨p,n⟩/‖n‖²)n with total real division, S(xRef,(x,p))=(x,R(h(xRef,x),p)), λ(xRef,(x,p))=√η max(0,⟨p,h(xRef,x)⟩) and H(y,xRef,(x,p))=(η⁻¹‖x−c‖²+‖p‖²)/2. Then: (1) S is jointly Borel measurable in (xRef,x,p); (2) λ is jointly continuous; (3) λ is jointly Borel measurable; (4) R(0,p)=p for every p; (5) for every n,p, R(n,R(n,p))=p, ‖R(n,p)‖=‖p‖ and ⟨R(n,p),n⟩=−⟨p,n⟩; (6) for every xRef,z, S fixes the position coordinate and S(xRef,S(xRef,z))=z; (7) H(y,xRef,S(xRef,z))=H(y,xRef,z) for all y,xRef,z; (8) λ(xRef,z)≥0, λ(xRef,S(xRef,z))=√η max(0,−⟨p,h(xRef,x)⟩) and λ(xRef,z)−λ(xRef,S(xRef,z))=√η⟨p,h(xRef,x)⟩; (9) h(xRef,x)=0 implies both S(xRef,(x,p))=(x,p) and λ(xRef,(x,p))=0; (10) for every y,xRef,z₀ put ℰ=H(y,xRef,z₀). Then ℰ≥0, and every z=(x,p) with H(y,xRef,z)=ℰ obeys ‖p‖≤√(2ℰ), ‖x−c‖≤√(2ηℰ) and λ(xRef,z)≤√η β√(2ℰ)(√(2ηℰ)+‖c−xRef‖). The gradient β-Lipschitz bound is derived internally from the canonical Hessian producer, never supplied as a new premise. The original six callers persist. Positive α, α≤β and βη≤1 remain standing conditions unused by this bounded deterministic BODY; C², the global Hessian bounds and η>0 supply the proof. No joint continuity of S is claimed at its zero-normal locus. This result supplies actual jump/rate prerequisites for Algorithm1/AppendixA.1 Proposition3.1; random clocks, path construction, nonexplosion, invariant and terminal kernels, convergence and costs remain open.

Zero-safe reflection

Actual bounce, rate and energy

Identities and majorant

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 zero-safe bounce, rate and energy-layer bound

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBounceRate.actual_bounce_rate_energy_laws · theorem · Teaching coverage

Read this first

Mathematical statement

\[c=y-\eta\nabla V(x_{\rm ref}),\quad h=\nabla V(x)-\nabla V(x_{\rm ref}),\quad R(n,p)=p-\frac{2\langle p,n\rangle}{\|n\|^2}n,\quad R(0,p)=p.\quad S(x_{\rm ref},(x,p))=(x,R(h,p)),\quad\lambda(x_{\rm ref},(x,p))=\sqrt\eta\max\{0,\langle p,h\rangle\},\quad H=\tfrac12(\eta^{-1}\|x-c\|^2+\|p\|^2).\quad H(Sz)=H(z),\quad\lambda(z)-\lambda(Sz)=\sqrt\eta\langle p,h\rangle,\quad\lambda(z)\le\Lambda_{\mathcal E}=\sqrt\eta\,\beta\sqrt{2\mathcal E}\bigl(\sqrt{2\eta\mathcal E}+\|c-x_{\rm ref}\|\bigr)\quad(H(z)=\mathcal E).\]

Lean statement · actual_bounce_rate_energy_laws

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_bounce_rate_energy_laws
    {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_bounce_rate_energy_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_bounce_rate_energy_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_bounce_rate_energy_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 c : E → E → E := fun y xRef => y - η • gradient V xRef
    let h : E → E → E := fun xRef x => gradient V x - gradient V xRef
    let R : E → E → E := fun n p =>
      p - (2 * inner ℝ p n / ‖n‖ ^ 2) • n
    let S : E → (E × E) → (E × E) := fun xRef z =>
      (z.1, R (h xRef z.1) z.2)
    let rate : E → (E × E) → ℝ := fun xRef z =>
      Real.sqrt η * max 0 (inner ℝ z.2 (h xRef z.1))
    let H : E → E → (E × E) → ℝ := fun y xRef z =>
      (η⁻¹ * ‖z.1 - c y xRef‖ ^ 2 + ‖z.2‖ ^ 2) / 2
    Measurable (fun a : E × (E × E) => S a.1 a.2) ∧
    Continuous (fun a : E × (E × E) => rate a.1 a.2) ∧
    Measurable (fun a : E × (E × E) => rate a.1 a.2) ∧
    (∀ p : E, R 0 p = p) ∧
    (∀ n p : E, R n (R n p) = p ∧ ‖R n p‖ = ‖p‖ ∧
      inner ℝ (R n p) n = -inner ℝ p n) ∧
    (∀ xRef : E, ∀ z : E × E,
      (S xRef z).1 = z.1 ∧ S xRef (S xRef z) = z) ∧
    (∀ y xRef : E, ∀ z : E × E,
      H y xRef (S xRef z) = H y xRef z) ∧
    (∀ xRef : E, ∀ z : E × E, 0 ≤ rate xRef z ∧
      rate xRef (S xRef z) =
        Real.sqrt η * max 0 (-inner ℝ z.2 (h xRef z.1)) ∧
      rate xRef z - rate xRef (S xRef z) =
        Real.sqrt η * inner ℝ z.2 (h xRef z.1)) ∧
    (∀ xRef x p : E, h xRef x = 0 →
      S xRef (x,p) = (x,p) ∧ rate xRef (x,p) = 0) ∧
    (∀ y xRef : E, ∀ z₀ : E × E,
      0 ≤ H y xRef z₀ ∧
      ∀ z : E × E, H y xRef z = H y xRef z₀ →
        ‖z.2‖ ≤ Real.sqrt (2 * H y xRef z₀) ∧
        ‖z.1 - c y xRef‖ ≤ Real.sqrt (2 * η * H y xRef z₀) ∧
        rate xRef z ≤ Real.sqrt η * (β : ℝ) *
          Real.sqrt (2 * H y xRef z₀) *
          (Real.sqrt (2 * η * H y xRef z₀) + ‖c y xRef - xRef‖))

Exact module and namespace context

Proof roadmap

1Derive the gradient bound internally
Finite dimension supplies completeness. Apply the existing quadratic-regularization Hessian theorem with r=0 to obtain LipschitzWith β (gradient V), hence continuity of the actual gradient. This closes a proof ingredient without adding a caller.
2Identify the zero-safe orthogonal reflection
Total division gives R(0,p)=p. For all n, R is the existing isometric reflection in the orthogonal complement of span(n). Its square is identity and it preserves norm. Expanding the inner product gives its sign reversal; the nonzero branch uses ‖n‖²≠0, while n=0 is handled separately.
3Check Borel and continuous operations
The state-dependent reflection uses continuous gradients, inner products and norms, together with total real division, which is Borel. Thus S is jointly Borel, including h=0. The positive-part rate uses no quotient, so it is jointly continuous and consequently Borel. Joint continuity of S is not required or asserted.
4Prove the actual bounce and rate identities
The position stays fixed, so its residual h stays fixed. Reflection involution proves S²=I and norm preservation proves exact H conservation. Its pairing sign reversal gives the flipped rate. For a=⟨p,h⟩, the two sign cases prove max(0,a)−max(0,−a)=a. The zero-residual case gives identity and zero rate.
5Keep zero energy and collect the first nine laws
η>0 makes η⁻¹ nonnegative, so H is nonnegative as the weighted sum of two squared vector norms divided by two. Collect the first nine laws, then fix arbitrary y,xRef,z₀ and z on its actual energy layer.
6Extract the two energy-layer radii
The equality H(z)=ℰ gives η⁻¹‖x−c‖²+‖p‖²=2ℰ. Dropping each nonnegative summand gives the momentum radius and, after multiplication by positive η, the position radius. Taking square roots requires no ℰ>0 and no division by ℰ.
7Derive the exact pointwise majorant
The triangle inequality bounds ‖x−xRef‖ by ‖x−c‖+‖c−xRef‖. Apply the internally derived β-Lipschitz estimate to h, then Cauchy–Schwarz and max(0,⟨p,h⟩)≤‖p‖‖h‖. Insert both radii and multiply by √η≥0. The resulting Λ is the printed same-energy-layer majorant, not a stochastic path or cost bound.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product space with compatible norm and its Borel measurable structure; products have product structures. Rank zero is allowed.
V:E→ℝ is C² on all E. The nonnegative α,β satisfy 0<α and α≤β, with α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E.
η is real, η>0 and βη≤1. These are the original six analytic callers. No gradient-Lipschitz, nonzero-normal, positive-energy, positive-dimension, flow or stochastic-law certificate is a caller.
All y,xRef,x,p are independent arbitrary points of E. Define c,h,R,S,λ,H exactly as displayed. Real division is total, so R(0,p)=p. H is a weighted sum of separate vector squared norms.
The final bound quantifies each z₀ and each z in the SAME actual H energy layer. It assumes no strictly positive energy or positive majorant; no division by either occurs.

Mathematical proof

1. Derive the gradient bound internally

Finite dimension supplies completeness. Apply the existing quadratic-regularization Hessian theorem with r=0 to obtain LipschitzWith β (gradient V), hence continuity of the actual gradient. This closes a proof ingredient without adding a caller.

\[\|\nabla V(x)-\nabla V(u)\|\le\beta\|x-u\|.\]

Corresponding Lean step

  letI : CompleteSpace E := FiniteDimensional.complete ℝ E
  have hLip : LipschitzWith β (gradient V) := by
    simpa using
      (AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
        (m := α) (L := β) (r := 0) hV hH (0 : E)).2
  have hgrad : Continuous (gradient V) := hLip.continuous