AutoSamplingTheory.SALD.generalMovingTargetGronwallSideConditionContract

Data definition / provenance and workflow record

Meaning and type

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

def generalMovingTargetGronwallSideConditionContract :
    GeneralMovingTargetGronwallSideConditionContract

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

theoremStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

endpointScheduleIdentities : String (explicit)

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

The theorem bound is stated at t=T and t=0; the Lean route must provide s(0)=0, S=s(T), t(s(T))=T, and the slowed-target identity tilde_pi_{s(t)}=pi_t.

terminalKlIdentification : String (explicit)

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

The Gronwall output K(T) is rewritten as KL(rho_S||pi_T) using S=s(T) and K(t)=KL(rho_{s(t)}||pi_t).

initialKlIdentification : String (explicit)

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

The initial term K(0) is rewritten as KL(rho_0||pi_0) using s(0)=0 and the source initial law X_0~rho_0.

coefficientRegularity : String (explicit)

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

a(t)=(sigma_t^2/2)*dot{s}(t)*C_LSI(t)-sigma_t^(-2)*dot{s}(t)^(-1)*alpha^(-1) and b(t)=sigma_t^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t) must satisfy the continuity or interval-integrability hypotheses required by lem:gronwall.

signFactsForResidualDrop : String (explicit)

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

The residual-exponent simplification uses C_LSI(u)>=0, sigma_u^2>=0, and dot{s}(u)>0, so -int_t^T (sigma_u^2/2)*dot{s}(u)*C_LSI(u) du <= 0.

exponentSplitAlgebra : String (explicit)

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

Split exp(-int_0^T a) into exp(-int_0^T (sigma_t^2/2)*dot{s}(t)*C_LSI(t)dt)*exp(int_0^T sigma_t^(-2)*dot{s}(t)^(-1)*alpha^(-1)dt).

residualExponentBound : String (explicit)

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

For the residual integral, bound exp(-int_t^T a(u)du) by exp(int_t^T sigma_u^(-2)*dot{s}(u)^(-1)*alpha^(-1)du) after dropping the nonpositive LSI contribution.

pureContractionResidualZero : String (explicit)

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

Under c_t=v_t, m_t=0; hence exp(alpha*||m_t||^2)=1, E_alpha(pi_t,m_t)=alpha^(-1)*log 1=0, and the residual integral in eq:general_moving_target_KL_bound vanishes.

dependencies : List String (explicit)

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

Ordered data items

1. SALD.cycle24GeneralVaSaldUpperPacket
2. SALD.cycle24GeneralVaSaldMiddleContract
3. sald.general_moving_target.cycle24_gronwall_middle
4. sald.forward_kl.schedule_time_change
5. sald.general_moving_target.kl_derivative
6. sald.general_moving_target.dv_m_energy
7. sald.general_moving_target.gronwall_application
8. sald.gronwall.integrating_factor
9. SALD.generalMovingTargetGronwallCoeffAdjacentIntervalIntegrable
10. SALD.generalMovingTargetGronwallExpProductRewriteIntegralCongrOfPieces
11. def:alpha-complexity

sourceGaps : List String (explicit)

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

Ordered data items

1. the source theorem does not isolate s(0)=0, S=s(T), and slowed-target endpoint identities as a separate lemma
2. the proof applies Gronwall without separately proving continuity or interval-integrability of the sigma-weighted coefficients; SALD.generalMovingTargetGronwallCoeffAdjacentIntervalIntegrable packages only the local interval-integrability closure once those hypotheses are supplied
3. the residual exponent drop relies on nonnegativity of C_LSI, sigma_t^2, and dot{s}, which must be exposed before formal proof search
4. the zero-residual alpha-complexity calculation uses normalization of pi_t and log(1)=0, which are not formalized locally

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 gronwall-side-condition obligation only.
2. Preserve the sigma-weighted coefficients and the exponent split from appendix.tex:908-934 and theorem lines 727-743.
3. Preferred first lower sub-slice after cycle 24 middle: theorem-specific coefficient regularity and adjacent interval-integrability for the LSI coefficient, alpha coefficient, and residual b(t) term.
4. SALD.generalMovingTargetGronwallCoeffAdjacentIntervalIntegrable and SALD.generalMovingTargetGronwallExpProductRewriteIntegralCongrOfPieces are compiled local algebra wrappers only after those source regularity hypotheses are supplied.
5. Record endpoint rewrites, coefficient regularity, residual-exponent monotonicity, and zero-residual alpha-complexity as obligations unless compiled Lean lemmas prove them.
6. Do not add these side conditions to the theorem statement as hidden assumptions.

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 generalMovingTargetGronwallSideConditionContract :
    GeneralMovingTargetGronwallSideConditionContract where
  sourceBlock := saldGeneralMovingTargetDvGronwallSource
  theoremStatement := saldGeneralMovingTargetSource
  endpointScheduleIdentities := "The theorem bound is stated at t=T and t=0; the Lean route must provide s(0)=0, S=s(T), t(s(T))=T, and the slowed-target identity tilde_pi_{s(t)}=pi_t."
  terminalKlIdentification := "The Gronwall output K(T) is rewritten as KL(rho_S||pi_T) using S=s(T) and K(t)=KL(rho_{s(t)}||pi_t)."
  initialKlIdentification := "The initial term K(0) is rewritten as KL(rho_0||pi_0) using s(0)=0 and the source initial law X_0~rho_0."
  coefficientRegularity := "a(t)=(sigma_t^2/2)*dot{s}(t)*C_LSI(t)-sigma_t^(-2)*dot{s}(t)^(-1)*alpha^(-1) and b(t)=sigma_t^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t) must satisfy the continuity or interval-integrability hypotheses required by lem:gronwall."
  signFactsForResidualDrop := "The residual-exponent simplification uses C_LSI(u)>=0, sigma_u^2>=0, and dot{s}(u)>0, so -int_t^T (sigma_u^2/2)*dot{s}(u)*C_LSI(u) du <= 0."
  exponentSplitAlgebra := "Split exp(-int_0^T a) into exp(-int_0^T (sigma_t^2/2)*dot{s}(t)*C_LSI(t)dt)*exp(int_0^T sigma_t^(-2)*dot{s}(t)^(-1)*alpha^(-1)dt)."
  residualExponentBound := "For the residual integral, bound exp(-int_t^T a(u)du) by exp(int_t^T sigma_u^(-2)*dot{s}(u)^(-1)*alpha^(-1)du) after dropping the nonpositive LSI contribution."
  pureContractionResidualZero := "Under c_t=v_t, m_t=0; hence exp(alpha*||m_t||^2)=1, E_alpha(pi_t,m_t)=alpha^(-1)*log 1=0, and the residual integral in eq:general_moving_target_KL_bound vanishes."
  dependencies := [
    "SALD.cycle24GeneralVaSaldUpperPacket",
    "SALD.cycle24GeneralVaSaldMiddleContract",
    "sald.general_moving_target.cycle24_gronwall_middle",
    "sald.forward_kl.schedule_time_change",
    "sald.general_moving_target.kl_derivative",
    "sald.general_moving_target.dv_m_energy",
    "sald.general_moving_target.gronwall_application",
    "sald.gronwall.integrating_factor",
    "SALD.generalMovingTargetGronwallCoeffAdjacentIntervalIntegrable",
    "SALD.generalMovingTargetGronwallExpProductRewriteIntegralCongrOfPieces",
    "def:alpha-complexity"
  ]
  sourceGaps := [
    "the source theorem does not isolate s(0)=0, S=s(T), and slowed-target endpoint identities as a separate lemma",
    "the proof applies Gronwall without separately proving continuity or interval-integrability of the sigma-weighted coefficients; SALD.generalMovingTargetGronwallCoeffAdjacentIntervalIntegrable packages only the local interval-integrability closure once those hypotheses are supplied",
    "the residual exponent drop relies on nonnegativity of C_LSI, sigma_t^2, and dot{s}, which must be exposed before formal proof search",
    "the zero-residual alpha-complexity calculation uses normalization of pi_t and log(1)=0, which are not formalized locally"
  ]
  lowerPacket := [
    "Target this contract or the named gronwall-side-condition obligation only.",
    "Preserve the sigma-weighted coefficients and the exponent split from appendix.tex:908-934 and theorem lines 727-743.",
    "Preferred first lower sub-slice after cycle 24 middle: theorem-specific coefficient regularity and adjacent interval-integrability for the LSI coefficient, alpha coefficient, and residual b(t) term.",
    "SALD.generalMovingTargetGronwallCoeffAdjacentIntervalIntegrable and SALD.generalMovingTargetGronwallExpProductRewriteIntegralCongrOfPieces are compiled local algebra wrappers only after those source regularity hypotheses are supplied.",
    "Record endpoint rewrites, coefficient regularity, residual-exponent monotonicity, and zero-residual alpha-complexity as obligations unless compiled Lean lemmas prove them.",
    "Do not add these side conditions to the theorem statement as hidden assumptions."
  ]
  status := ProofStatus.obligation