AutoSamplingTheory.SALD.generalMovingTargetDiscreteGronwallSideConditionContract

Data definition / provenance and workflow record

Meaning and type

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

def generalMovingTargetDiscreteGronwallSideConditionContract :
    GeneralMovingTargetDiscreteGronwallSideConditionContract

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.saldGeneralMovingTargetDiscreteGronwallSideConditionSource — audited data reference, not expanded and not a compiled dependency edge

theoremStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

endpointLawIdentities : String (explicit)

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

The global K(t) used at appendix.tex:1573-1583 must be stitched from EM interval laws with s(0)=0, s(T)=S, hat rho_{s_k}=rho_k^eta, hat rho_{s_{k+1}}=rho_{k+1}^eta, and pi_{t(s(t))}=pi_t.

constantScheduleIdentities : 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; the time-change from appendix.tex:1579-1583 must rewrite dot{s}(t)*dot{t}(s(t))^2 as dot{s}(t)^(-1) and dot{s}(t)*Gamma/Delta terms exactly as in lines 1588-1597.

terminalKlIdentification : String (explicit)

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

After Gronwall, K(T) is identified with KL(rho_K^eta||pi_T), using endpoint matching of the last frozen interpolation interval and the target endpoint t=T.

initialKlIdentification : String (explicit)

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

The initial Gronwall term K(0) is identified with KL(rho_0||pi_0), using X_0^eta~rho_0 and the first interpolation endpoint.

stitchedRegularity : String (explicit)

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

The interval-wise derivative inequalities for KL(hat rho_s||tilde pi_s) must assemble into a piecewise differentiable or absolutely continuous K(t) admissible for lem:gronwall.

coefficientRegularity : 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) and b(t)=2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t)+2*dot{s}(t)*eta*Delta(t) need the continuity or interval-integrability required by lem:gronwall.

gronwallDisplayMatch : String (explicit)

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

The Gronwall output with this a(t), b(t), K(0), and K(T) is the theorem display eq:general_moving_target_KL_bound_discrete at appendix.tex:1316-1347; no extra exponent split or residual LSI drop is used here.

residualCoefficientAudit : String (explicit)

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

The DV residual term 2*sigma_eta^(-2)*dot{t}(s)^2*(alpha^(-1)*K+E_alpha) becomes the two theorem coefficients 2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*alpha^(-1) in a(t) and 2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t) in b(t).

frozenDeltaCoefficientAudit : String (explicit)

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

The frozen-delta terms 2*Gamma(t(s))*eta^2*alpha'^(-1)*K_s and 2*Delta(t(s))*eta become 2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t) in a(t) and 2*dot{s}(t)*eta*Delta(t) in b(t).

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.constant_schedule_stitching
3. SALD.generalMovingTargetDiscreteConstantScheduleSquareScalar
4. SALD.generalMovingTargetDiscreteResidualCoefficientRewriteScalar
5. SALD.generalMovingTargetDiscreteGammaCoefficientRewriteScalar
6. SALD.generalMovingTargetDiscreteDeltaCoefficientRewriteScalar
7. SALD.generalMovingTargetDiscretePointwiseGronwallInputOfPostDvTimeChanged
8. SALD.generalMovingTargetDiscreteGronwallNamedCoefficientInput
9. SALD.generalMovingTargetDiscreteGronwallEndpointRewriteScalar
10. sald.general_moving_target_discrete.kl_derivative
11. sald.general_moving_target_discrete.dv_m_energy
12. sald.general_moving_target_discrete.frozen_delta_cross_lip
13. sald.forward_kl.schedule_time_change

sourceGaps : List String (explicit)

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

Ordered data items

1. the source proof does not isolate endpoint identifications K(T)=KL(rho_K^eta||pi_T) and K(0)=KL(rho_0||pi_0) as a separate lemma
2. the constant inverse-schedule assumption is stated in the theorem, while the proof uses it inside the coefficient rewrite after the s-to-t time change
3. the final Gronwall call requires stitched-interval regularity and coefficient integrability that are not stated explicitly
4. the exact doubled residual and frozen-delta coefficients must be preserved when passing from appendix.tex:1558-1570 to appendix.tex:1586-1597

lowerPacket : List String (explicit)

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

Ordered data items

1. Target this contract or the named discrete gronwall-side-condition obligation only.
2. Preserve the theorem display at appendix.tex:1316-1347 and the differential inequality at appendix.tex:1586-1597.
3. Reuse SALD.generalMovingTargetDiscreteGronwallNamedCoefficientInput and SALD.generalMovingTargetDiscreteGronwallEndpointRewriteScalar for the local display-matching pieces, and refine endpoint stitching, constant-schedule coefficient rewrites, coefficient regularity, or exact Gronwall-display matching as obligations unless compiled Lean lemmas prove them.
4. Do not add new hypotheses to thm:general-moving-target-SALD-discrete or simplify the doubled residual coefficients.

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 generalMovingTargetDiscreteGronwallSideConditionContract :
    GeneralMovingTargetDiscreteGronwallSideConditionContract where
  sourceBlock := saldGeneralMovingTargetDiscreteGronwallSideConditionSource
  theoremStatement := saldGeneralMovingTargetDiscreteSource
  endpointLawIdentities := "The global K(t) used at appendix.tex:1573-1583 must be stitched from EM interval laws with s(0)=0, s(T)=S, hat rho_{s_k}=rho_k^eta, hat rho_{s_{k+1}}=rho_{k+1}^eta, and pi_{t(s(t))}=pi_t."
  constantScheduleIdentities := "The theorem assumes dot{t}(s)=dot{s}(t)^(-1) is constant; the time-change from appendix.tex:1579-1583 must rewrite dot{s}(t)*dot{t}(s(t))^2 as dot{s}(t)^(-1) and dot{s}(t)*Gamma/Delta terms exactly as in lines 1588-1597."
  terminalKlIdentification := "After Gronwall, K(T) is identified with KL(rho_K^eta||pi_T), using endpoint matching of the last frozen interpolation interval and the target endpoint t=T."
  initialKlIdentification := "The initial Gronwall term K(0) is identified with KL(rho_0||pi_0), using X_0^eta~rho_0 and the first interpolation endpoint."
  stitchedRegularity := "The interval-wise derivative inequalities for KL(hat rho_s||tilde pi_s) must assemble into a piecewise differentiable or absolutely continuous K(t) admissible for lem:gronwall."
  coefficientRegularity := "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) and b(t)=2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t)+2*dot{s}(t)*eta*Delta(t) need the continuity or interval-integrability required by lem:gronwall."
  gronwallDisplayMatch := "The Gronwall output with this a(t), b(t), K(0), and K(T) is the theorem display eq:general_moving_target_KL_bound_discrete at appendix.tex:1316-1347; no extra exponent split or residual LSI drop is used here."
  residualCoefficientAudit := "The DV residual term 2*sigma_eta^(-2)*dot{t}(s)^2*(alpha^(-1)*K+E_alpha) becomes the two theorem coefficients 2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*alpha^(-1) in a(t) and 2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t) in b(t)."
  frozenDeltaCoefficientAudit := "The frozen-delta terms 2*Gamma(t(s))*eta^2*alpha'^(-1)*K_s and 2*Delta(t(s))*eta become 2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t) in a(t) and 2*dot{s}(t)*eta*Delta(t) in b(t)."
  dependencies := [
    "lem:gronwall",
    "sald.general_moving_target_discrete.constant_schedule_stitching",
    "SALD.generalMovingTargetDiscreteConstantScheduleSquareScalar",
    "SALD.generalMovingTargetDiscreteResidualCoefficientRewriteScalar",
    "SALD.generalMovingTargetDiscreteGammaCoefficientRewriteScalar",
    "SALD.generalMovingTargetDiscreteDeltaCoefficientRewriteScalar",
    "SALD.generalMovingTargetDiscretePointwiseGronwallInputOfPostDvTimeChanged",
    "SALD.generalMovingTargetDiscreteGronwallNamedCoefficientInput",
    "SALD.generalMovingTargetDiscreteGronwallEndpointRewriteScalar",
    "sald.general_moving_target_discrete.kl_derivative",
    "sald.general_moving_target_discrete.dv_m_energy",
    "sald.general_moving_target_discrete.frozen_delta_cross_lip",
    "sald.forward_kl.schedule_time_change"
  ]
  sourceGaps := [
    "the source proof does not isolate endpoint identifications K(T)=KL(rho_K^eta||pi_T) and K(0)=KL(rho_0||pi_0) as a separate lemma",
    "the constant inverse-schedule assumption is stated in the theorem, while the proof uses it inside the coefficient rewrite after the s-to-t time change",
    "the final Gronwall call requires stitched-interval regularity and coefficient integrability that are not stated explicitly",
    "the exact doubled residual and frozen-delta coefficients must be preserved when passing from appendix.tex:1558-1570 to appendix.tex:1586-1597"
  ]
  lowerPacket := [
    "Target this contract or the named discrete gronwall-side-condition obligation only.",
    "Preserve the theorem display at appendix.tex:1316-1347 and the differential inequality at appendix.tex:1586-1597.",
    "Reuse SALD.generalMovingTargetDiscreteGronwallNamedCoefficientInput and SALD.generalMovingTargetDiscreteGronwallEndpointRewriteScalar for the local display-matching pieces, and refine endpoint stitching, constant-schedule coefficient rewrites, coefficient regularity, or exact Gronwall-display matching as obligations unless compiled Lean lemmas prove them.",
    "Do not add new hypotheses to thm:general-moving-target-SALD-discrete or simplify the doubled residual coefficients."
  ]
  status := ProofStatus.obligation