AutoSamplingTheory.SALD.cycle26ForwardKlMiddleContract

Data definition / provenance and workflow record

Meaning and type

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

def cycle26ForwardKlMiddleContract :
    ForwardKlMiddleSourceToLeanContract

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.

sourceStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

sourceProof : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

derivativeSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

dvSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

gronwallSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlGronwallSource — 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 the cycle-26 upper target into a lower-ready map for sald.forward_kl.dv_finite_log_mgf_witness: isolate common-space/absolute-continuity, measurability of ||v_t||^2, alpha0-to-alpha finite-log-mgf, and positive-alpha scaling before the DV-energy inequality is used.

sourceStepMap : List String (explicit)

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

Ordered data items

1. main_body.tex:218-228 defines E_alpha(pi_t,v_t)=alpha^(-1)*log E_{pi_t}[exp(alpha*||v_t||^2)] and the integrated alpha-complexity; this supplies the log-mgf expression, not a Lean proof of finiteness.
2. main_body.tex:240-241 assumes there is alpha0>0 with E_{alpha0}(pi_t,v_t)<+infty for every t in [0,T]; appendix.tex:230-241 immediately applies the DV formula for any alpha in (0,alpha0].
3. appendix.tex:73-79 states lem:dv_variation on probability distributions on the same space with finite log-mgf; in this theorem the intended measures are nu=rho_{s(t)} and mu=pi_t.
4. appendix.tex:230-235 chooses the exact DV test function Z_t(x)=alpha*||v_t(x)||^2; lower work must expose measurability and real-valuedness of this squared-velocity test.
5. appendix.tex:234-238 gives E_{rho_{s(t)}}[alpha*||v_t||^2] <= KL(rho_{s(t)}||pi_t)+log E_{pi_t}[exp(alpha*||v_t||^2)]; the absolute-continuity/common-space facts are implicit and stay obligations.
6. appendix.tex:239-241 divides by alpha>0 and rewrites alpha^(-1)*log E_{pi_t}[exp(alpha*||v_t||^2)] as E_alpha(pi_t,v_t), preserving the downstream coefficient (1/2)*dot{s}(t)^(-1)*alpha^(-1).

leanStepMap : List String (explicit)

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

Ordered data items

1. Keep SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract unchanged; no new finite-mgf or absolute-continuity theorem hypothesis is added.
2. Route the selected lower target through SALD.forwardKlDvFiniteLogMgfWitnessContract, SALD.forwardKlDvFiniteLogMgfWitnessObligation, and sald.forward_kl.dv_finite_log_mgf_witness.
3. Use SALD.forwardKlDvAlphaMonotonicityContract and sald.forward_kl.dv_alpha_mgf_monotonicity only for the alpha0-to-alpha finite-log-mgf bridge.
4. Use SALD.saldDvFiniteLogMgfContract and probability.dv_variational_formula only as the source-cited DV interface; do not mark entropy duality formalized.
5. Use SALD.forwardKlDvPositiveAlphaScalingScalar and SALD.forwardKlDvPositiveAlphaCoefficientScalar only for the scalar division and coefficient-preservation substep after the DV inequality has been supplied.
6. Keep the common state space and rho_{s(t)} << pi_t requirements tied to SALD.forwardKlMovingTargetDependencyContract and the KL vocabulary rather than adding a theorem-level assumption.
7. Leave the subsequent coefficient audit and Gronwall assembly in SALD.forwardKlDependencyChainAuditContract, SALD.forwardKlGronwallSideConditionContract, and the cycle-22 Gronwall helpers.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. lem:dv_variation is external-cited-result via Boucheron Cor. 4.15; the SLT entropy_duality theorem remains a future port pattern, not an imported ASTIS dependency.
2. The alpha0-to-alpha finite-log-mgf bridge is a local measure/order lemma, not an external cited result.
3. The common-space, absolute-continuity, and measurability interfaces are source-contract gaps implicit in the paper's KL and vector-field vocabulary.
4. LSI-to-KL/FI, the KL derivative, endpoint schedule identities, coefficient regularity, and full Gronwall remain separate obligations outside this lower slice.

obligations : List String (explicit)

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

Ordered data items

1. sald.forward_kl.cycle26_dv_witness_middle
2. sald.forward_kl.dv_finite_log_mgf_witness
3. sald.forward_kl.dv_alpha_mgf_monotonicity
4. SALD.forwardKlDvPositiveAlphaScalingScalar
5. SALD.forwardKlDvPositiveAlphaCoefficientScalar
6. sald.dv_variation.finite_log_mgf_interface
7. probability.dv_variational_formula
8. sald.forward_kl.moving_target_dependency_chain
9. sald.forward_kl.dv_energy_bound

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.forwardKlDvFiniteLogMgfWitnessContract / SALD.forwardKlDvFiniteLogMgfWitnessObligation / sald.forward_kl.dv_finite_log_mgf_witness.
2. First sub-slice: provide a Lean-facing interface for the same measurable space of rho_{s(t)} and pi_t, rho_{s(t)} << pi_t, and measurability/real-valuedness of Z_t=alpha*||v_t||^2.
3. Second sub-slice if the first is blocked: refine sald.forward_kl.dv_alpha_mgf_monotonicity from finite E_alpha0(pi_t,v_t) to finite log E_{pi_t}[exp(alpha*||v_t||^2)] for 0<alpha<=alpha0.
4. Use the compiled scalar lemmas for positive-alpha division and coefficient preservation, but do not change the theorem alpha range or introduce a second finite-mgf assumption.
5. Do not reopen LSI, KL derivative, endpoint schedule, Gronwall side conditions, residual exponent drop, or full theorem proof in this lower attempt.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle26_middle_dv_witness before ASTIS.SALD.forward_KL.dv_finite_log_mgf_witness and the DV-energy block.
2. SALD.saldDependenciesForLabel "thm:forward-KL" includes SALD.cycle26ForwardKlMiddleContract and sald.forward_kl.cycle26_dv_witness_middle while retaining prior cycle-14, cycle-18, cycle-22, and cycle-26 upper dependencies.
3. The conversion window, proof-obligation ledger, SLT audit, and dialogue board classify cycle 26 middle as source-dependency synchronization, not as a proof of DV, alpha-mgf monotonicity, or thm:forward-KL.
4. SALD_original.jsonl indexes thm:forward-KL, def:alpha-complexity, lem:dv_variation, eq:LSI-KL-FI, and lem:gronwall from the original source while excluding sald_version_2.tex.
5. No fake proof closure appears and no analytic dependency is promoted beyond obligation or source-cited status.

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 cycle26ForwardKlMiddleContract :
    ForwardKlMiddleSourceToLeanContract where
  sourceStatement := saldForwardKlSource
  sourceProof := saldForwardKlProofSource
  derivativeSource := saldForwardKlDerivativeSource
  dvSource := saldForwardKlDvEnergySource
  gronwallSource := saldForwardKlGronwallSource
  objective := "Translate the cycle-26 upper target into a lower-ready map for sald.forward_kl.dv_finite_log_mgf_witness: isolate common-space/absolute-continuity, measurability of ||v_t||^2, alpha0-to-alpha finite-log-mgf, and positive-alpha scaling before the DV-energy inequality is used."
  sourceStepMap := [
    "main_body.tex:218-228 defines E_alpha(pi_t,v_t)=alpha^(-1)*log E_{pi_t}[exp(alpha*||v_t||^2)] and the integrated alpha-complexity; this supplies the log-mgf expression, not a Lean proof of finiteness.",
    "main_body.tex:240-241 assumes there is alpha0>0 with E_{alpha0}(pi_t,v_t)<+infty for every t in [0,T]; appendix.tex:230-241 immediately applies the DV formula for any alpha in (0,alpha0].",
    "appendix.tex:73-79 states lem:dv_variation on probability distributions on the same space with finite log-mgf; in this theorem the intended measures are nu=rho_{s(t)} and mu=pi_t.",
    "appendix.tex:230-235 chooses the exact DV test function Z_t(x)=alpha*||v_t(x)||^2; lower work must expose measurability and real-valuedness of this squared-velocity test.",
    "appendix.tex:234-238 gives E_{rho_{s(t)}}[alpha*||v_t||^2] <= KL(rho_{s(t)}||pi_t)+log E_{pi_t}[exp(alpha*||v_t||^2)]; the absolute-continuity/common-space facts are implicit and stay obligations.",
    "appendix.tex:239-241 divides by alpha>0 and rewrites alpha^(-1)*log E_{pi_t}[exp(alpha*||v_t||^2)] as E_alpha(pi_t,v_t), preserving the downstream coefficient (1/2)*dot{s}(t)^(-1)*alpha^(-1)."
  ]
  leanStepMap := [
    "Keep SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract unchanged; no new finite-mgf or absolute-continuity theorem hypothesis is added.",
    "Route the selected lower target through SALD.forwardKlDvFiniteLogMgfWitnessContract, SALD.forwardKlDvFiniteLogMgfWitnessObligation, and sald.forward_kl.dv_finite_log_mgf_witness.",
    "Use SALD.forwardKlDvAlphaMonotonicityContract and sald.forward_kl.dv_alpha_mgf_monotonicity only for the alpha0-to-alpha finite-log-mgf bridge.",
    "Use SALD.saldDvFiniteLogMgfContract and probability.dv_variational_formula only as the source-cited DV interface; do not mark entropy duality formalized.",
    "Use SALD.forwardKlDvPositiveAlphaScalingScalar and SALD.forwardKlDvPositiveAlphaCoefficientScalar only for the scalar division and coefficient-preservation substep after the DV inequality has been supplied.",
    "Keep the common state space and rho_{s(t)} << pi_t requirements tied to SALD.forwardKlMovingTargetDependencyContract and the KL vocabulary rather than adding a theorem-level assumption.",
    "Leave the subsequent coefficient audit and Gronwall assembly in SALD.forwardKlDependencyChainAuditContract, SALD.forwardKlGronwallSideConditionContract, and the cycle-22 Gronwall helpers."
  ]
  citedResultInterfaces := [
    "lem:dv_variation is external-cited-result via Boucheron Cor. 4.15; the SLT entropy_duality theorem remains a future port pattern, not an imported ASTIS dependency.",
    "The alpha0-to-alpha finite-log-mgf bridge is a local measure/order lemma, not an external cited result.",
    "The common-space, absolute-continuity, and measurability interfaces are source-contract gaps implicit in the paper's KL and vector-field vocabulary.",
    "LSI-to-KL/FI, the KL derivative, endpoint schedule identities, coefficient regularity, and full Gronwall remain separate obligations outside this lower slice."
  ]
  obligations := [
    "sald.forward_kl.cycle26_dv_witness_middle",
    "sald.forward_kl.dv_finite_log_mgf_witness",
    "sald.forward_kl.dv_alpha_mgf_monotonicity",
    "SALD.forwardKlDvPositiveAlphaScalingScalar",
    "SALD.forwardKlDvPositiveAlphaCoefficientScalar",
    "sald.dv_variation.finite_log_mgf_interface",
    "probability.dv_variational_formula",
    "sald.forward_kl.moving_target_dependency_chain",
    "sald.forward_kl.dv_energy_bound"
  ]
  lowerPacket := [
    "Target exactly SALD.forwardKlDvFiniteLogMgfWitnessContract / SALD.forwardKlDvFiniteLogMgfWitnessObligation / sald.forward_kl.dv_finite_log_mgf_witness.",
    "First sub-slice: provide a Lean-facing interface for the same measurable space of rho_{s(t)} and pi_t, rho_{s(t)} << pi_t, and measurability/real-valuedness of Z_t=alpha*||v_t||^2.",
    "Second sub-slice if the first is blocked: refine sald.forward_kl.dv_alpha_mgf_monotonicity from finite E_alpha0(pi_t,v_t) to finite log E_{pi_t}[exp(alpha*||v_t||^2)] for 0<alpha<=alpha0.",
    "Use the compiled scalar lemmas for positive-alpha division and coefficient preservation, but do not change the theorem alpha range or introduce a second finite-mgf assumption.",
    "Do not reopen LSI, KL derivative, endpoint schedule, Gronwall side conditions, residual exponent drop, or full theorem proof in this lower attempt."
  ]
  reviewerChecklist := [
    "SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle26_middle_dv_witness before ASTIS.SALD.forward_KL.dv_finite_log_mgf_witness and the DV-energy block.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes SALD.cycle26ForwardKlMiddleContract and sald.forward_kl.cycle26_dv_witness_middle while retaining prior cycle-14, cycle-18, cycle-22, and cycle-26 upper dependencies.",
    "The conversion window, proof-obligation ledger, SLT audit, and dialogue board classify cycle 26 middle as source-dependency synchronization, not as a proof of DV, alpha-mgf monotonicity, or thm:forward-KL.",
    "SALD_original.jsonl indexes thm:forward-KL, def:alpha-complexity, lem:dv_variation, eq:LSI-KL-FI, and lem:gronwall from the original source while excluding sald_version_2.tex.",
    "No fake proof closure appears and no analytic dependency is promoted beyond obligation or source-cited status."
  ]
  status := ProofStatus.obligation

/-- Cycle-30 upper packet for the continuous forward-KL derivative side.

This packet returns to the front of the `thm:forward-KL` proof after the
cycle-26 DV witness and cycle-29 LSI density-test refinements.  It selects only
the derivative-side interface from `appendix.tex:168-228`: KL differentiation,
mass conservation, SALD Fokker--Planck integration by parts, slowed-target
transport, Young's inequality, and the inverse-schedule time change.  It does
not change the source theorem, prove the KL derivative, or promote LSI, DV, or
Gronwall.
-/