AutoSamplingTheory.SALD.cycle24GeneralVaSaldMiddleContract

Data definition / provenance and workflow record

Meaning and type

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

def cycle24GeneralVaSaldMiddleContract :
    GeneralVaSaldGuidedPathMiddleContract

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.

guidedResidualSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

generalContinuousSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

unifiedSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

discreteSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

objective : String (explicit)

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

Translate appendix.tex:909-945 into a lower-ready middle ledger for sald.general_moving_target.gronwall_side_conditions, with theorem-display endpoint rewrites, sigma-weighted coefficient regularity, exponent splitting, residual-exponent monotonicity, and zero-residual alpha-complexity kept as explicit obligations.

sourceStepMap : List String (explicit)

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

Ordered data items

1. appendix.tex:908-910 gives the scalar differential inequality after residual DV with 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).
2. appendix.tex:911-920 applies lem:gronwall and identifies the Gronwall endpoint K(T) with KL(rho_S||pi_T) and K(0) with KL(rho_0||pi_0).
3. appendix.tex:913-920 splits exp(-int_0^T a) into the theorem's LSI contraction factor and positive alpha factor without changing sigma_t, dot{s}(t), or alpha.
4. appendix.tex:921-932 rewrites the residual integral and drops only the nonpositive LSI contribution from exp(-int_t^T a), using C_LSI>=0, sigma_u^2>=0, and dot{s}(u)>0 as side conditions.
5. appendix.tex:936-945 specializes c_t=v_t, so m_t=0 and E_alpha(pi_t,m_t)=alpha^(-1)*log E_{pi_t}[1]=0, leaving the pure-contraction display.
6. appendix.tex:949-951 and main_body.tex:372-395 reuse the same bridge only after the unified specialization c_t<-u_t, v_t=u_t+w_t, and m_t=w_t.

leanStepMap : List String (explicit)

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

Ordered data items

1. SALD.generalMovingTargetGronwallInstantiationContract records the source a(t), b(t), and pre-split Gronwall output.
2. SALD.generalMovingTargetGronwallSideConditionContract records endpointScheduleIdentities, terminalKlIdentification, initialKlIdentification, coefficientRegularity, exponentSplitAlgebra, residualExponentBound, and pureContractionResidualZero.
3. SALD.cycle24GeneralVaSaldGronwallMiddleObligation keeps this middle source map synchronized with the lower target sald.general_moving_target.gronwall_side_conditions.
4. SALD.generalMovingTargetGronwallCoeffAdjacentIntervalIntegrable and SALD.generalMovingTargetGronwallExpProductRewriteIntegralCongrOfPieces package the cycle-24 lower coefficient slice only after theorem-specific interval-integrability for the sigma/LSI, alpha, and residual pieces is supplied.
5. The reusable scalar Gronwall exponent helpers may be used only after theorem-specific endpoint equalities, coefficient regularity, interval-integrability, and sign facts are supplied.
6. The unified theorem remains SALD.unifiedForwardKlSpecializationContract; this middle packet does not introduce a direct VA-SALD KL proof.
7. The discrete general theorem remains under the cycle-20 discrete Gronwall-side-condition packet and is only listed as downstream reuse.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. lem:gronwall remains a local real-analysis obligation through sald.gronwall.integrating_factor and theorem-specific side conditions.
2. lem:dv_variation remains source-cited through sald.general_moving_target.dv_m_energy; this middle packet starts after the residual DV inequality is available.
3. eq:LSI-KL-FI remains the inherited density-test obligation that supplies C_LSI>=0 and the FI-to-KL contraction step.
4. No SLT theorem applies to endpoint rewrites, sigma-weighted coefficient regularity, residual-exponent monotonicity, or zero-residual alpha-complexity.

obligations : List String (explicit)

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

Ordered data items

1. sald.general_moving_target.cycle24_gronwall_middle
2. sald.general_moving_target.gronwall_side_conditions
3. sald.general_moving_target.gronwall_application
4. sald.general_moving_target.dv_m_energy
5. sald.general_moving_target.kl_derivative
6. sald.forward_kl.schedule_time_change
7. sald.gronwall.integrating_factor
8. sald.gronwall.exponent_rewrite
9. probability.lsi_to_kl_fi

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.generalMovingTargetGronwallSideConditionContract / SALD.generalMovingTargetGronwallSideConditionObligation / sald.general_moving_target.gronwall_side_conditions.
2. Preferred first sub-slice: theorem-specific coefficient regularity and adjacent interval-integrability for the LSI coefficient (sigma_t^2/2)*dot{s}(t)*C_LSI(t), the alpha coefficient 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).
3. Use SALD.generalMovingTargetGronwallCoeffAdjacentIntervalIntegrable only as the local assembly step; it does not prove the source regularity hypotheses.
4. Alternative one-slice targets are endpoint K(0)/K(T) rewrites, exponent-split algebra against appendix.tex:727-743, residual-exponent monotonicity on [t,T], or zero-residual alpha-complexity for appendix.tex:936-945.
5. Keep the derivative, LSI-to-KL/FI, residual DV witness, full Gronwall theorem, unified transport bridge, and discrete general theorem as separate dependencies.
6. Do not add endpoint, sign, sigma positivity, coefficient-integrability, normalization, or finite-log-mgf assumptions to theorem statements; record blocked interfaces as obligations.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. Every source step from appendix.tex:909-945 and theorem display appendix.tex:727-743 is classified as Lean contract, cited result, or named obligation.
2. SALD.generalVaSaldContract and SALD.unifiedForwardKlContract list SALD.cycle24GeneralVaSaldGronwallMiddleObligation while preserving contractOnly status.
3. SALD.generalVaSaldProofDag contains ASTIS.SALD.general_moving_target.cycle24_middle_gronwall_bridge between the upper packet and gronwall_side_conditions blocks.
4. SALD.saldDependenciesForLabel "thm:general-moving-target-SALD" and "thm:unified-forward-KL" include SALD.cycle24GeneralVaSaldMiddleContract and sald.general_moving_target.cycle24_gronwall_middle.
5. No theorem statement, source coefficient, source file selection, or analytic dependency status is changed.

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 cycle24GeneralVaSaldMiddleContract :
    GeneralVaSaldGuidedPathMiddleContract where
  guidedResidualSource := saldGuidedResidualSource
  generalContinuousSource := saldGeneralMovingTargetSource
  unifiedSource := saldUnifiedForwardKlSource
  discreteSource := saldGeneralMovingTargetDiscreteSource
  objective := "Translate appendix.tex:909-945 into a lower-ready middle ledger for sald.general_moving_target.gronwall_side_conditions, with theorem-display endpoint rewrites, sigma-weighted coefficient regularity, exponent splitting, residual-exponent monotonicity, and zero-residual alpha-complexity kept as explicit obligations."
  sourceStepMap := [
    "appendix.tex:908-910 gives the scalar differential inequality after residual DV with 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).",
    "appendix.tex:911-920 applies lem:gronwall and identifies the Gronwall endpoint K(T) with KL(rho_S||pi_T) and K(0) with KL(rho_0||pi_0).",
    "appendix.tex:913-920 splits exp(-int_0^T a) into the theorem's LSI contraction factor and positive alpha factor without changing sigma_t, dot{s}(t), or alpha.",
    "appendix.tex:921-932 rewrites the residual integral and drops only the nonpositive LSI contribution from exp(-int_t^T a), using C_LSI>=0, sigma_u^2>=0, and dot{s}(u)>0 as side conditions.",
    "appendix.tex:936-945 specializes c_t=v_t, so m_t=0 and E_alpha(pi_t,m_t)=alpha^(-1)*log E_{pi_t}[1]=0, leaving the pure-contraction display.",
    "appendix.tex:949-951 and main_body.tex:372-395 reuse the same bridge only after the unified specialization c_t<-u_t, v_t=u_t+w_t, and m_t=w_t."
  ]
  leanStepMap := [
    "SALD.generalMovingTargetGronwallInstantiationContract records the source a(t), b(t), and pre-split Gronwall output.",
    "SALD.generalMovingTargetGronwallSideConditionContract records endpointScheduleIdentities, terminalKlIdentification, initialKlIdentification, coefficientRegularity, exponentSplitAlgebra, residualExponentBound, and pureContractionResidualZero.",
    "SALD.cycle24GeneralVaSaldGronwallMiddleObligation keeps this middle source map synchronized with the lower target sald.general_moving_target.gronwall_side_conditions.",
    "SALD.generalMovingTargetGronwallCoeffAdjacentIntervalIntegrable and SALD.generalMovingTargetGronwallExpProductRewriteIntegralCongrOfPieces package the cycle-24 lower coefficient slice only after theorem-specific interval-integrability for the sigma/LSI, alpha, and residual pieces is supplied.",
    "The reusable scalar Gronwall exponent helpers may be used only after theorem-specific endpoint equalities, coefficient regularity, interval-integrability, and sign facts are supplied.",
    "The unified theorem remains SALD.unifiedForwardKlSpecializationContract; this middle packet does not introduce a direct VA-SALD KL proof.",
    "The discrete general theorem remains under the cycle-20 discrete Gronwall-side-condition packet and is only listed as downstream reuse."
  ]
  citedResultInterfaces := [
    "lem:gronwall remains a local real-analysis obligation through sald.gronwall.integrating_factor and theorem-specific side conditions.",
    "lem:dv_variation remains source-cited through sald.general_moving_target.dv_m_energy; this middle packet starts after the residual DV inequality is available.",
    "eq:LSI-KL-FI remains the inherited density-test obligation that supplies C_LSI>=0 and the FI-to-KL contraction step.",
    "No SLT theorem applies to endpoint rewrites, sigma-weighted coefficient regularity, residual-exponent monotonicity, or zero-residual alpha-complexity."
  ]
  obligations := [
    "sald.general_moving_target.cycle24_gronwall_middle",
    "sald.general_moving_target.gronwall_side_conditions",
    "sald.general_moving_target.gronwall_application",
    "sald.general_moving_target.dv_m_energy",
    "sald.general_moving_target.kl_derivative",
    "sald.forward_kl.schedule_time_change",
    "sald.gronwall.integrating_factor",
    "sald.gronwall.exponent_rewrite",
    "probability.lsi_to_kl_fi"
  ]
  lowerPacket := [
    "Target exactly SALD.generalMovingTargetGronwallSideConditionContract / SALD.generalMovingTargetGronwallSideConditionObligation / sald.general_moving_target.gronwall_side_conditions.",
    "Preferred first sub-slice: theorem-specific coefficient regularity and adjacent interval-integrability for the LSI coefficient (sigma_t^2/2)*dot{s}(t)*C_LSI(t), the alpha coefficient 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).",
    "Use SALD.generalMovingTargetGronwallCoeffAdjacentIntervalIntegrable only as the local assembly step; it does not prove the source regularity hypotheses.",
    "Alternative one-slice targets are endpoint K(0)/K(T) rewrites, exponent-split algebra against appendix.tex:727-743, residual-exponent monotonicity on [t,T], or zero-residual alpha-complexity for appendix.tex:936-945.",
    "Keep the derivative, LSI-to-KL/FI, residual DV witness, full Gronwall theorem, unified transport bridge, and discrete general theorem as separate dependencies.",
    "Do not add endpoint, sign, sigma positivity, coefficient-integrability, normalization, or finite-log-mgf assumptions to theorem statements; record blocked interfaces as obligations."
  ]
  reviewerChecklist := [
    "Every source step from appendix.tex:909-945 and theorem display appendix.tex:727-743 is classified as Lean contract, cited result, or named obligation.",
    "SALD.generalVaSaldContract and SALD.unifiedForwardKlContract list SALD.cycle24GeneralVaSaldGronwallMiddleObligation while preserving contractOnly status.",
    "SALD.generalVaSaldProofDag contains ASTIS.SALD.general_moving_target.cycle24_middle_gronwall_bridge between the upper packet and gronwall_side_conditions blocks.",
    "SALD.saldDependenciesForLabel \"thm:general-moving-target-SALD\" and \"thm:unified-forward-KL\" include SALD.cycle24GeneralVaSaldMiddleContract and sald.general_moving_target.cycle24_gronwall_middle.",
    "No theorem statement, source coefficient, source file selection, or analytic dependency status is changed."
  ]
  status := ProofStatus.obligation

/-- Cycle-28 upper packet for the discrete general VA-SALD derivative side conditions.

This returns to the guided/general path after the discrete forward-KL accumulated
collection work.  It selects the pre-Gronwall derivative side-condition ledger
for `thm:general-moving-target-SALD-discrete`, especially the frozen/residual
algebra and the two Young coefficient splits that produce the doubled residual
coefficient and the Gamma/Delta terms.
-/