Actual Gaussian numerical kernel: integrated law and source transport contraction

Fan Chen, Sinho Chewi, Jianfeng Lu, Matthew S. Zhang; ASTIS explicit transport prerequisite/actual-kernel interface, not the full local-error or main result.

Complete source statement (Samplinglib restatement)

Construct a Markov K whose law at every z is Gamma.map(zeta -> Phi(z,zeta)). For all probability mu,nu, K composed with each input equals the actual pushforward Phi#(input×Gamma), and W_M²(Kmu,Knu)<=(1-h/(65536kappa))² W_M²(mu,nu). This is the actual deterministic exact-gradient Gaussian numerical kernel, not an arbitrary supplied contracting kernel and not an invariant-target theorem.

Genuine randomized law and raw transport

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 Gaussian numerical kernel: integrated law and source transport contraction

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ActualKernelTransport.source_kernel_transport_contraction · theorem · Teaching coverage

Read this first

Mathematical statement

Construct a Markov K whose law at every z is Gamma.map(zeta → Phi(z,zeta)). For all probability mu,nu, K composed with each input equals the actual pushforward Phi#(input×Gamma), and W_M²(Kmu,Knu)≤(1-h/(65536kappa))² W_M²(mu,nu). This is the actual deterministic exact-gradient Gaussian numerical kernel, not an arbitrary supplied contracting kernel and not an invariant-target theorem.

\[K(z)=\Phi_z{}_{\#}\Gamma,\quad K\mu=\Phi_\#(\mu\otimes\Gamma),\quad W_{2,M_\kappa}^2(K\mu,K\nu)\le\left(1-\frac{h}{65536\kappa}\right)^2W_{2,M_\kappa}^2(\mu,\nu).\]

Lean statement · source_kernel_transport_contraction

Exact randomized law/actual Phi and Markov semantics, canonical raw source cost.

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 source_kernel_transport_contraction {f : E → ℝ} {κ h : ℝ} {J : ℕ}
    (hκ : 1 ≤ κ) (hf : ContDiff ℝ 2 f)
    (hH : ∀ z v, (1 / (2 * κ)) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ f) z v) v ∧
      (fderiv ℝ (fderiv ℝ f) z v) v ≤ ‖v‖ ^ 2)
    (hJ : 2 ≤ J) (hh : 0 < h) :
    let t := fun i : Fin J => h/2*(1-Real.cos ((i : ℝ)/(J-1 : ℝ)*Real.pi))
    let ell := fun j : Fin J => Lagrange.basis Finset.univ t j
    let Λ := sSup ((fun s : ℝ => ∑ j : Fin J, |(ell j).eval s|) '' Icc 0 h)
    let ω := fun i j : Fin J => ∫ s in 0..t i, (t i-s)*(ell j).eval s
    let b := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
    let c := fun j : Fin J => ∫ s in 0..h, (h-s)*(ell j).eval s
    h * Λ ≤ 1/(65536*κ) →
    let a := Real.exp (-h / 2)
    let sigma := Real.sqrt (1 - Real.exp (-h))
    let P0 := fun (z ζ : E × E) => a • z.2 + sigma • ζ.1
    let Y0 := fun (z ζ : E × E) j => z.1 + t j • P0 z ζ
    let Y1 := fun (z ζ : E × E) i => Y0 z ζ i - ∑ j, ω i j • gradient f (Y0 z ζ j)
    let Φ := fun w : (E × E) × (E × E) =>
      (w.1.1 + h • P0 w.1 w.2 - ∑ j, c j • gradient f (Y1 w.1 w.2 j),
        a • (P0 w.1 w.2 - ∑ j, b j • gradient f (Y1 w.1 w.2 j)) + sigma • w.2.2)
    let Γ := (stdGaussian E).prod (stdGaussian E)
    ∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧
      (∀ z, K z = Γ.map (fun ζ => Φ (z,ζ))) ∧
      ∀ (μ ν : Measure (E × E)), IsProbabilityMeasure μ → IsProbabilityMeasure ν →
        K ∘ₘ μ = (μ.prod Γ).map Φ ∧ K ∘ₘ ν = (ν.prod Γ).map Φ ∧
        phaseWassersteinSq κ (K ∘ₘ μ) (K ∘ₘ ν) ≤
          ENNReal.ofReal ((1-h/(65536*κ))^2) * phaseWassersteinSq κ μ ν

Exact module and namespace context

Proof roadmap

1Recover actual joint measurability
The genuine source quadrature constructor gives Lambda≥1. The actual step condition gives h≤1 and h²Lambda≤1. Reuse FirstOrderDifference for exactly the same coefficients/potential/Phi; its jointly measurable actual numerical map is the needed random-map producer.
2Build the Markov kernel and prove both laws
Use (id times const Gamma).map Phi. Markovness follows from actual independent probability refreshes and measurable Phi. At each z, dirac×Gamma followed by map composition gives Gamma.map(Phi_z). For any probability input, the map-composition and constant-kernel product identities yield Kmu=Phi#(mu×Gamma). These identities justify the actual kernel semantics before applying a law-level inequality.
3Square the actual source norm contraction
The existing ActualContraction theorem proves the source Q norm contraction for every input and common noise, using the actual numerical phase. Delta=1-h/(65536kappa) is strictly positive. The unchanged Q lower comparison gives nonnegative Q for all phase displacements. Square the genuine sqrt inequality and reuse the squared sqrt identity, then apply ofReal multiplication. This proves the measurable extended pointwise cost bound with A=ofReal(delta²); it is not a public supplied premise of this consumer.
4Consume the shared genuine coupling lift
The source cost is measurable by its exact Q formula. A is positive and finite. Apply the shared randomized-map transport theorem to the actual Phi, actual Gaussian product law and arbitrary input probabilities, then rewrite both actual kernel laws. No optimizer, finite transport premise, invariant measure or selection of the state-dependent H/R is introduced.

Full assumptions and notation

All objects and hypotheses

E is a complete finite-dimensional real inner-product Borel space, including zero dimension. kappa≥1, f:E→R is globally C2 and its actual nested second derivative satisfies (2kappa)^-1||v||²≤D²f(z)[v,v]≤||v||² for every z,v. Producing the actual source f=V_eta remains open.
J≥2,h>0; t_j=h(1-cos(j*pi/(J-1)))/2, cardinal ell_j, and omega_ij=integral_0^t_i(t_i-s)ell_j(s)ds, b_j=integral_0^h ell_j(s)ds,c_j=integral_0^h(h-s)ell_j(s)ds are the actual coefficients. Lambda=sup_[0,h] sum_j |ell_j| and actual hLambda≤1/(65536kappa).
a=exp(-h/2),sigma=sqrt(1-exp(-h)); P0=a p+sigma zeta0, Y0_j=x+t_jP0, Y1_i=Y0_i-sum_j omega_ij gradient f(Y0_j), Phi=(x+hP0-sum_j c_j gradient f(Y1_j),a(P0-sum_j b_j gradient f(Y1_j))+sigma zeta1). Gamma=standard Gaussian E product standard Gaussian E, with independent refresh vectors.
Both input laws mu,nu are arbitrary probability laws on phase space; their source quadratic transport may be infinite. Q_kappa(x,p)=((2kappa)^-1+1/2)||x||²+inner(x,p)+||p||², c_kappa(z,zprime)=ofReal Q_kappa(z-zprime), and W_M²=T_c_kappa. Source Q is retained, not the ordinary product max norm.

Mathematical proof

1. Recover actual joint measurability

The genuine source quadrature constructor gives Lambda≥1. The actual step condition gives h≤1 and h²Lambda≤1. Reuse FirstOrderDifference for exactly the same coefficients/potential/Phi; its jointly measurable actual numerical map is the needed random-map producer.

\[\Lambda_J\ge1,\quad h\le1,\quad h^2\Lambda_J\le1,\quad\Phi\text{ jointly measurable}.\]

Corresponding Lean step

hcoeff; hLambda; hs; hfirst.1; hΦ

2. Build the Markov kernel and prove both laws

Use (id times const Gamma).map Phi. Markovness follows from actual independent probability refreshes and measurable Phi. At each z, dirac×Gamma followed by map composition gives Gamma.map(Phi_z). For any probability input, the map-composition and constant-kernel product identities yield Kmu=Phi#(mu×Gamma). These identities justify the actual kernel semantics before applying a law-level inequality.

\[K=(\mathrm{id}\times\mathrm{const}\,\Gamma).\mathrm{map}\,\Phi,\qquad K\mu=\Phi_\#(\mu\otimes\Gamma).\]

Corresponding Lean step

K; hK; Kernel.map_apply; Kernel.prod_apply; Measure.dirac_prod; hlaw; Measure.map_comp; Measure.compProd_eq_comp_prod; Measure.compProd_const

3. Square the actual source norm contraction

The existing ActualContraction theorem proves the source Q norm contraction for every input and common noise, using the actual numerical phase. Delta=1-h/(65536kappa) is strictly positive. The unchanged Q lower comparison gives nonnegative Q for all phase displacements. Square the genuine sqrt inequality and reuse the squared sqrt identity, then apply ofReal multiplication. This proves the measurable extended pointwise cost bound with A=ofReal(delta²); it is not a public supplied premise of this consumer.

\[c_\kappa(\Phi_z(\zeta),\Phi_{z\prime}(\zeta))\le\delta^2c_\kappa(z,z\prime),\qquad\delta>0.\]

Corresponding Lean step

hδ; nonnegQ; ActualContraction.source_synchronous_contraction; hcon; hsq; Real.sq_sqrt; ENNReal.ofReal_mul

4. Consume the shared genuine coupling lift

The source cost is measurable by its exact Q formula. A is positive and finite. Apply the shared randomized-map transport theorem to the actual Phi, actual Gaussian product law and arbitrary input probabilities, then rewrite both actual kernel laws. No optimizer, finite transport premise, invariant measure or selection of the state-dependent H/R is introduced.

\[W_{2,M_\kappa}^2(K\mu,K\nu)\le\delta^2W_{2,M_\kappa}^2(\mu,\nu).\]

Corresponding Lean step

hc; transportCost_randomized_map_le; hlaw

Lean verification

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

Lean proof · source_kernel_transport_contraction

Genuine synchronous coupling / actual kernel-law producer, measurable nonnegative integrals and positive finite scaled raw infimum.

Download module (.lean)

theorem source_kernel_transport_contraction {f : E → ℝ} {κ h : ℝ} {J : ℕ}
    (hκ : 1 ≤ κ) (hf : ContDiff ℝ 2 f)
    (hH : ∀ z v, (1 / (2 * κ)) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ f) z v) v ∧
      (fderiv ℝ (fderiv ℝ f) z v) v ≤ ‖v‖ ^ 2)
    (hJ : 2 ≤ J) (hh : 0 < h) :
    let t := fun i : Fin J => h/2*(1-Real.cos ((i : ℝ)/(J-1 : ℝ)*Real.pi))
    let ell := fun j : Fin J => Lagrange.basis Finset.univ t j
    let Λ := sSup ((fun s : ℝ => ∑ j : Fin J, |(ell j).eval s|) '' Icc 0 h)
    let ω := fun i j : Fin J => ∫ s in 0..t i, (t i-s)*(ell j).eval s
    let b := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
    let c := fun j : Fin J => ∫ s in 0..h, (h-s)*(ell j).eval s
    h * Λ ≤ 1/(65536*κ) →
    let a := Real.exp (-h / 2)
    let sigma := Real.sqrt (1 - Real.exp (-h))
    let P0 := fun (z ζ : E × E) => a • z.2 + sigma • ζ.1
    let Y0 := fun (z ζ : E × E) j => z.1 + t j • P0 z ζ
    let Y1 := fun (z ζ : E × E) i => Y0 z ζ i - ∑ j, ω i j • gradient f (Y0 z ζ j)
    let Φ := fun w : (E × E) × (E × E) =>
      (w.1.1 + h • P0 w.1 w.2 - ∑ j, c j • gradient f (Y1 w.1 w.2 j),
        a • (P0 w.1 w.2 - ∑ j, b j • gradient f (Y1 w.1 w.2 j)) + sigma • w.2.2)
    let Γ := (stdGaussian E).prod (stdGaussian E)
    ∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧
      (∀ z, K z = Γ.map (fun ζ => Φ (z,ζ))) ∧
      ∀ (μ ν : Measure (E × E)), IsProbabilityMeasure μ → IsProbabilityMeasure ν →
        K ∘ₘ μ = (μ.prod Γ).map Φ ∧ K ∘ₘ ν = (ν.prod Γ).map Φ ∧
        phaseWassersteinSq κ (K ∘ₘ μ) (K ∘ₘ ν) ≤
          ENNReal.ofReal ((1-h/(65536*κ))^2) * phaseWassersteinSq κ μ ν := by
  classical
  dsimp only
  let t := fun i : Fin J => h/2*(1-Real.cos ((i : ℝ)/(J-1 : ℝ)*Real.pi))
  let ell := fun j : Fin J => Lagrange.basis Finset.univ t j
  let Λ := sSup ((fun s : ℝ => ∑ j : Fin J, |(ell j).eval s|) '' Icc 0 h)
  let ω := fun i j : Fin J => ∫ s in 0..t i, (t i-s)*(ell j).eval s
  let b := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
  let c := fun j : Fin J => ∫ s in 0..h, (h-s)*(ell j).eval s
  intro hstep
  change h*Λ ≤ 1/(65536*κ) at hstep
  have hcoeff := TechnicalLemmas.Analysis.ChebyshevLobattoQuadrature.chebyshev_lobatto_coefficients hJ hh
  rcases hcoeff with ⟨_,_,_,_,_,hΛ,_,_⟩
  change 1 ≤ Λ at hΛ
  have hk : 0 < κ := lt_of_lt_of_le zero_lt_one hκ
  have hi : 1/(65536*κ) ≤ (1:ℝ) := (div_le_one (by positivity)).mpr (by linarith)
  have hh1 : h ≤ 1 := by nlinarith
  have hs : h^2*Λ ≤ 1 := by
    have hm := mul_le_mul_of_nonneg_left (hstep.trans hi) (le_of_lt hh)
    nlinarith
  let a := Real.exp (-h / 2)
  let sigma := Real.sqrt (1 - Real.exp (-h))
  let P0 := fun (z ζ : E × E) => a • z.2 + sigma • ζ.1
  let Y0 := fun (z ζ : E × E) j => z.1 + t j • P0 z ζ
  let Y1 := fun (z ζ : E × E) i => Y0 z ζ i - ∑ j, ω i j • gradient f (Y0 z ζ j)
  let Φ := fun w : (E × E) × (E × E) =>
    (w.1.1 + h • P0 w.1 w.2 - ∑ j, c j • gradient f (Y1 w.1 w.2 j),
      a • (P0 w.1 w.2 - ∑ j, b j • gradient f (Y1 w.1 w.2 j)) + sigma • w.2.2)
  let Γ := (stdGaussian E).prod (stdGaussian E)
  have hfirst := FirstOrderDifference.source_first_order_difference hκ hf hH hJ hh hs
  have hΦ : Measurable Φ := hfirst.1
  let K := (Kernel.id ×ₖ Kernel.const (E × E) Γ).map Φ
  have hK : IsMarkovKernel K := Kernel.IsMarkovKernel.map _ hΦ
  refine ⟨K,hK,?_,?_⟩
  · intro z
    dsimp only [K]
    rw [Kernel.map_apply _ hΦ, Kernel.prod_apply, Kernel.id_apply, Kernel.const_apply,
      Measure.dirac_prod, Measure.map_map hΦ (by fun_prop)]
    rfl
  · intro μ ν hμ hν
    letI : IsProbabilityMeasure μ := hμ
    letI : IsProbabilityMeasure ν := hν
    have hlaw (ρ : Measure (E × E)) [IsProbabilityMeasure ρ] :
        K ∘ₘ ρ = (ρ.prod Γ).map Φ := by
      dsimp only [K]
      rw [← Measure.map_comp ρ _ hΦ, ← Measure.compProd_eq_comp_prod,
        Measure.compProd_const]
    refine ⟨hlaw μ,hlaw ν,?_⟩
    rw [hlaw μ,hlaw ν]
    let δ := 1-h/(65536*κ)
    have hδ : 0 < δ := by
      dsimp only [δ]
      apply sub_pos.mpr
      exact (div_lt_one (by positivity)).mpr (by linarith)
    have nonnegQ (v : E × E) : 0 ≤ phaseQuadraticForm κ v := by
      have hl := ordinary_energy_le_phaseQuadraticForm hκ v
      nlinarith [sq_nonneg ‖v.1‖,sq_nonneg ‖v.2‖]
    have hcost : ∀ z z' ζ : E × E,
        phaseCost κ (Φ (z,ζ),Φ (z',ζ)) ≤
          ENNReal.ofReal (δ^2)*phaseCost κ (z,z') := by
      intro z z' ζ
      have hcon := ActualContraction.source_synchronous_contraction hκ hf hH hJ hh hstep z z' ζ
      change Real.sqrt (phaseQuadraticForm κ (Φ (z,ζ)-Φ (z',ζ))) ≤
        δ*Real.sqrt (phaseQuadraticForm κ (z-z')) at hcon
      have hsq := (sq_le_sq₀ (Real.sqrt_nonneg _)
        (mul_nonneg hδ.le (Real.sqrt_nonneg _))).mpr hcon
      rw [mul_pow, Real.sq_sqrt (nonnegQ _), Real.sq_sqrt (nonnegQ _)] at hsq
      change ENNReal.ofReal (phaseQuadraticForm κ (Φ (z,ζ)-Φ (z',ζ))) ≤
        ENNReal.ofReal (δ^2)*ENNReal.ofReal (phaseQuadraticForm κ (z-z'))
      rw [← ENNReal.ofReal_mul (sq_nonneg δ)]
      exact ENNReal.ofReal_le_ofReal hsq
    have hc : Measurable (phaseCost (E := E) κ) := by
      unfold phaseCost phaseQuadraticForm
      fun_prop
    exact TechnicalLemmas.Measure.RandomizedMapTransport.transportCost_randomized_map_le
      Φ hΦ (phaseCost κ) hc (ENNReal.ofReal (δ^2))
      (ne_of_gt (ENNReal.ofReal_pos.mpr (sq_pos_of_pos hδ)))
      ENNReal.ofReal_ne_top hcost μ ν Γ

end
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ActualKernelTransport

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Common-noise coupling of the source phase and its induced law.	E is a complete finite-dimensional real inner-product Borel space, including zero dimension. kappa>=1, f:E->R is globally C2 and its actual nested second derivative satisfies (2kappa)^-1\|\|v\|\|²<=D²f(z)[v,v]<=\|\|v\|\|² for every z,v. Producing the actual source f=V_eta remains open. J>=2,h>0; t_j=h(1-cos(j*pi/(J-1)))/2, cardinal ell_j, and omega_ij=integral_0^t_i(t_i-s)ell_j(s)ds, b_j=integral_0^h ell_j(s)ds,c_j=integral_0^h(h-s)ell_j(s)ds are the actual coefficients. Lambda=sup_[0,h] sum_j \|ell_j\| and actual hLambda<=1/(65536kappa). a=exp(-h/2),sigma=sqrt(1-exp(-h)); P0=a p+sigma zeta0, Y0_j=x+t_jP0, Y1_i=Y0_i-sum_j omega_ij gradient f(Y0_j), Phi=(x+hP0-sum_j c_j gradient f(Y1_j),a(P0-sum_j b_j gradient f(Y1_j))+sigma zeta1). Gamma=standard Gaussian E product standard Gaussian E, with independent refresh vectors. Both input laws mu,nu are arbitrary probability laws on phase space; their source quadratic transport may be infinite. Q_kappa(x,p)=((2kappa)^-1+1/2)\|\|x\|\|²+inner(x,p)+\|\|p\|\|², c_kappa(z,zprime)=ofReal Q_kappa(z-zprime), and W_M²=T_c_kappa. Source Q is retained, not the ordinary product max norm.	unresolved	Shared prerequisite abstracts measurable maps/costs with an explicit pointwise premise and API-only Borel group structure; the actual source consumer proves that premise for its genuine Phi. At the actual consumer, f=V_eta remains an exposed unresolved producer, and source Q/Gaussian kernel semantics are exact. Arbitrary probability inputs may have infinite raw costs; no moment/invariance claim.
Source universal constant c and squared source metric costs.	Construct a Markov K whose law at every z is Gamma.map(zeta -> Phi(z,zeta)). For all probability mu,nu, K composed with each input equals the actual pushforward Phi#(input×Gamma), and W_M²(Kmu,Knu)<=(1-h/(65536kappa))² W_M²(mu,nu). This is the actual deterministic exact-gradient Gaussian numerical kernel, not an arbitrary supplied contracting kernel and not an invariant-target theorem.	same	Actual consumer retains the simultaneously valid c=1/65536, squares its pointwise norm contraction, and constructs a real synchronous coupling. Shared A>0 finite is explicit; no zero-times-infinity or hidden optimizer argument.

Actual Gaussian exact-gradient numerical K at the explicit normalized global C2 curvature interface. Actual f=V_eta smoothing/C2/curvature remains separate. No target invariance/stationarity, numerical target bias, stochastic Khat/Kbar, local errors/history/expected query cost, Wp/proxy-warmness/initialization, PBPS or either complete main/composition result. TV proximity does not transfer unbounded cost.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

Actual Gaussian exact-gradient numerical K at the explicit normalized global C2 curvature interface. Actual f=V_eta smoothing/C2/curvature remains separate. No target invariance/stationarity, numerical target bias, stochastic Khat/Kbar, local errors/history/expected query cost, Wp/proxy-warmness/initialization, PBPS or either complete main/composition result. TV proximity does not transfer unbounded cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Kernel.IsMarkovKernel.map
Kernel.map_apply
Kernel.prod_apply
Kernel.id_apply
Kernel.const_apply
Measure.dirac_prod
Measure.map_map
Measure.map_comp
Measure.compProd_eq_comp_prod
Measure.compProd_const
sq_le_sq₀
Real.sq_sqrt
ENNReal.ofReal_mul
ENNReal.ofReal_le_ofReal
ENNReal.ofReal_pos
ENNReal.ofReal_ne_top
div_lt_one

Mathematical sources

SPHMC actual common-noise transport prerequisite — Actual Gaussian exact-gradient numerical K at the explicit normalized global C2 curvature interface. Actual f=V_eta smoothing/C2/curvature remains separate. No target invariance/stationarity, numerical target bias, stochastic Khat/Kbar, local errors/history/expected query cost, Wp/proxy-warmness/initialization, PBPS or either complete main/composition result. TV proximity does not transfer unbounded cost.

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 Gaussian numerical kernel: integrated law and source transport contraction

Complete source statement (Samplinglib restatement)

Genuine randomized law and raw transport

Read the formalized proofs

Actual Gaussian numerical kernel: integrated law and source transport contraction

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Recover actual joint measurability

2. Build the Markov kernel and prove both laws

3. Square the actual source norm contraction

4. Consume the shared genuine coupling lift

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?