AutoSamplingTheory.SALD.generalMovingTargetDiscreteGronwallInstantiationContract

Data definition / provenance and workflow record

Meaning and type

The result has data type AutoSamplingTheory.SALD.GeneralMovingTargetDiscreteGronwallInstantiationContract. A value of this type stores descriptions; it is not a proof of the statements in those descriptions.

def generalMovingTargetDiscreteGronwallInstantiationContract :
    GeneralMovingTargetDiscreteGronwallInstantiationContract

Construction and field-by-field explanation

Construct a data record from explicit fields and the audited defaults shown below.

This Lean definition constructs provenance or workflow data. It does not prove the mathematical statements stored as text. Status labels, named dependencies and citations are data, not compilation, proof or source certificates.

sourceBlock : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteGronwallSource — audited data reference, not expanded and not a compiled dependency edge

quantityK : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

K(t)=KL(hat rho_{s(t)}||pi_t), with K(T)=KL(rho_K^eta||pi_T).

gronwallA : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

a(t)=(sigma_eta(t)^2/2)*dot{s}(t)*C_LSI(t)-2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*alpha^(-1)-2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t).

gronwallB : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

b(t)=2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t)+2*dot{s}(t)*eta*Delta(t).

theoremBound : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

The source bound eq:general_moving_target_KL_bound_discrete is exactly the Gronwall bound with this a(t) and b(t), without the later exponent simplifications used in main-body corollaries.

constantScheduleInterface : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

The theorem assumes dot{t}(s)=dot{s}(t)^(-1) is constant; Lean must represent the endpoint laws and K(t) over the stitched EM intervals under this schedule.

requiredRegularity : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. interval-integrability of C_LSI, sigma_eta, Gamma, Delta, and E_alpha(pi_t,m_t)
2. piecewise differentiability or absolute continuity of K(t) after stitching EM intervals
3. positivity of sigma_eta(t) and dot{s}(t)

sourceGaps : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. the theorem assumes a constant inverse schedule but does not spell out the schedule API needed by the Gronwall backend
2. the final proof says only that applying lem:gronwall finishes the proof; all regularity and endpoint matching remain obligations

dependencies : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. lem:gronwall
2. sald.general_moving_target_discrete.kl_derivative
3. sald.general_moving_target_discrete.dv_m_energy
4. sald.general_moving_target_discrete.em_interpolation_fp

status : AutoSamplingTheory.ProofStatus (explicit)

Stored workflow tag; honor the exact default but do not infer mathematical certification.

AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

def generalMovingTargetDiscreteGronwallInstantiationContract :
    GeneralMovingTargetDiscreteGronwallInstantiationContract where
  sourceBlock := saldGeneralMovingTargetDiscreteGronwallSource
  quantityK := "K(t)=KL(hat rho_{s(t)}||pi_t), with K(T)=KL(rho_K^eta||pi_T)."
  gronwallA := "a(t)=(sigma_eta(t)^2/2)*dot{s}(t)*C_LSI(t)-2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*alpha^(-1)-2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t)."
  gronwallB := "b(t)=2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t)+2*dot{s}(t)*eta*Delta(t)."
  theoremBound := "The source bound eq:general_moving_target_KL_bound_discrete is exactly the Gronwall bound with this a(t) and b(t), without the later exponent simplifications used in main-body corollaries."
  constantScheduleInterface := "The theorem assumes dot{t}(s)=dot{s}(t)^(-1) is constant; Lean must represent the endpoint laws and K(t) over the stitched EM intervals under this schedule."
  requiredRegularity := [
    "interval-integrability of C_LSI, sigma_eta, Gamma, Delta, and E_alpha(pi_t,m_t)",
    "piecewise differentiability or absolute continuity of K(t) after stitching EM intervals",
    "positivity of sigma_eta(t) and dot{s}(t)"
  ]
  sourceGaps := [
    "the theorem assumes a constant inverse schedule but does not spell out the schedule API needed by the Gronwall backend",
    "the final proof says only that applying lem:gronwall finishes the proof; all regularity and endpoint matching remain obligations"
  ]
  dependencies := [
    "lem:gronwall",
    "sald.general_moving_target_discrete.kl_derivative",
    "sald.general_moving_target_discrete.dv_m_energy",
    "sald.general_moving_target_discrete.em_interpolation_fp"
  ]
  status := ProofStatus.obligation