AutoSamplingTheory.SALD.cycle14ForwardKlMiddleContract

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 cycle14ForwardKlMiddleContract :
    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.

Map the continuous forward-KL proof route from source lines to Lean-facing contracts and lower obligations, while keeping thm:forward-KL and its displayed bound fixed.

sourceStepMap : List String (explicit)

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

Ordered data items

1. main_body.tex:238-247 states the inverse slowdown setup, LSI constants C_LSI(t)>=0, finite alpha0-complexity for the transport velocity v_t, alpha in (0,alpha0], and the terminal KL display.
2. appendix.tex:168-185 differentiates KL(rho_s||tilde_pi_s), uses mass conservation and the SALD Fokker--Planck equation, and identifies the first term as -FI(rho_s||tilde_pi_s).
3. appendix.tex:187-208 uses the transport velocity v_t for pi_t, defines tilde_v_s=dot{t}(s)*v_{t(s)}, proves it transports tilde_pi_s, and bounds the second derivative term by Young.
4. appendix.tex:210-228 combines the derivative pieces with eq:LSI-KL-FI and changes from s to t, producing the pre-DV inequality with coefficient (1/2)*dot{s}(t)^(-1).
5. appendix.tex:230-241 applies lem:dv_variation with Z=alpha*||v_t||^2 and rewrites the log-mgf contribution as E_alpha(pi_t,v_t).
6. appendix.tex:244-252 applies lem:gronwall, splits the initial exponent, drops the nonpositive LSI contribution from the residual exponent, and matches main_body.tex:243-246.

leanStepMap : List String (explicit)

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

Ordered data items

1. The theorem statement remains represented by SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract.
2. Density regularity, mass conservation, differentiation under the integral, and integration by parts are tracked by SALD.forwardKlDerivativeSideConditionContract and sald.forward_kl.density_boundary_regular.
3. Slowed-target transport, inverse-schedule calculus, and endpoint rewrites are tracked by SALD.forwardKlEndpointScheduleContract, SALD.forwardKlMovingTargetDependencyContract, SALD.forwardKlDerivativeSideConditionContract, and sald.forward_kl.schedule_time_change.
4. The LSI step is routed through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi; no LSI proof is promoted.
5. The DV step is split between SALD.forwardKlDvAlphaMonotonicityContract, SALD.forwardKlDvFiniteLogMgfWitnessContract, and SALD.forwardKlDvEnergyCandidateContract.
6. The scalar coefficient and endpoint algebra are tracked by SALD.forwardKlDependencyChainAuditContract, SALD.forwardKlGronwallInstantiationContract, and SALD.forwardKlGronwallSideConditionContract.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. lem:dv_variation remains source-cited through Boucheron Corollary 4.15 or the SLT entropy_duality pattern; no SLT theorem is imported.
2. eq:LSI-KL-FI remains a local density-test obligation through probability.lsi_to_kl_fi.
3. lem:gronwall remains a local real-analysis obligation through sald.gronwall.integrating_factor, sald.gronwall.endpoint_calculus, and sald.gronwall.exponent_rewrite.
4. Transport-velocity existence/minimality is source background from main_body.tex:230-232; the proof only requires a stated transport velocity interface.

obligations : List String (explicit)

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

Ordered data items

1. sald.forward_kl.middle_source_to_lean_map
2. sald.forward_kl.endpoint_schedule_identities
3. sald.forward_kl.moving_target_dependency_chain
4. sald.forward_kl.density_boundary_regular
5. sald.forward_kl.schedule_time_change
6. sald.forward_kl.kl_derivative
7. probability.lsi_to_kl_fi
8. sald.forward_kl.dv_alpha_mgf_monotonicity
9. sald.forward_kl.dv_finite_log_mgf_witness
10. sald.forward_kl.dv_energy_bound
11. sald.forward_kl.coefficient_chain_audit
12. sald.forward_kl.gronwall_application
13. sald.forward_kl.gronwall_side_conditions

lowerPacket : List String (explicit)

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

Ordered data items

1. Preferred lower target: refine SALD.forwardKlEndpointScheduleContract and sald.forward_kl.endpoint_schedule_identities for s(0)=0, S=s(T), t(s(T))=T, and tilde_pi_{s(t)}=pi_t.
2. Keep the source proof route derivative -> LSI -> DV -> Gronwall; do not introduce path-space, Girsanov, Pinsker, Talagrand, or a different Gronwall normalization.
3. If the endpoint slice is blocked, refine exactly one alternative interface: slowed-target transport, density/boundary side conditions, DV finite-log-mgf/common-space witness, or Gronwall coefficient regularity.
4. Preserve the differential inequality from appendix.tex:239-241 and the terminal theorem display in main_body.tex:243-246 byte-for-byte at the contract level.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. Every source step in appendix.tex:168-252 is classified as a Lean contract, cited result, or named proof obligation.
2. SALD.continuousSaldContract includes sald.forward_kl.middle_source_to_lean_map and still keeps all analytic backends at obligation or source-cited status.
3. SALD.forwardKlProofDag exposes ASTIS.SALD.forward_KL.middle_source_to_lean_map before lower proof-search blocks.
4. SALD.saldDependenciesForLabel "thm:forward-KL" includes SALD.cycle14ForwardKlMiddleContract, sald.forward_kl.middle_source_to_lean_map, and sald.forward_kl.endpoint_schedule_identities.
5. The source index still excludes sald_version_2.tex and no analytic dependency is marked formalized.

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 cycle14ForwardKlMiddleContract :
    ForwardKlMiddleSourceToLeanContract where
  sourceStatement := saldForwardKlSource
  sourceProof := saldForwardKlProofSource
  derivativeSource := saldForwardKlDerivativeSource
  dvSource := saldForwardKlDvEnergySource
  gronwallSource := saldForwardKlGronwallSource
  objective := "Map the continuous forward-KL proof route from source lines to Lean-facing contracts and lower obligations, while keeping thm:forward-KL and its displayed bound fixed."
  sourceStepMap := [
    "main_body.tex:238-247 states the inverse slowdown setup, LSI constants C_LSI(t)>=0, finite alpha0-complexity for the transport velocity v_t, alpha in (0,alpha0], and the terminal KL display.",
    "appendix.tex:168-185 differentiates KL(rho_s||tilde_pi_s), uses mass conservation and the SALD Fokker--Planck equation, and identifies the first term as -FI(rho_s||tilde_pi_s).",
    "appendix.tex:187-208 uses the transport velocity v_t for pi_t, defines tilde_v_s=dot{t}(s)*v_{t(s)}, proves it transports tilde_pi_s, and bounds the second derivative term by Young.",
    "appendix.tex:210-228 combines the derivative pieces with eq:LSI-KL-FI and changes from s to t, producing the pre-DV inequality with coefficient (1/2)*dot{s}(t)^(-1).",
    "appendix.tex:230-241 applies lem:dv_variation with Z=alpha*||v_t||^2 and rewrites the log-mgf contribution as E_alpha(pi_t,v_t).",
    "appendix.tex:244-252 applies lem:gronwall, splits the initial exponent, drops the nonpositive LSI contribution from the residual exponent, and matches main_body.tex:243-246."
  ]
  leanStepMap := [
    "The theorem statement remains represented by SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract.",
    "Density regularity, mass conservation, differentiation under the integral, and integration by parts are tracked by SALD.forwardKlDerivativeSideConditionContract and sald.forward_kl.density_boundary_regular.",
    "Slowed-target transport, inverse-schedule calculus, and endpoint rewrites are tracked by SALD.forwardKlEndpointScheduleContract, SALD.forwardKlMovingTargetDependencyContract, SALD.forwardKlDerivativeSideConditionContract, and sald.forward_kl.schedule_time_change.",
    "The LSI step is routed through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi; no LSI proof is promoted.",
    "The DV step is split between SALD.forwardKlDvAlphaMonotonicityContract, SALD.forwardKlDvFiniteLogMgfWitnessContract, and SALD.forwardKlDvEnergyCandidateContract.",
    "The scalar coefficient and endpoint algebra are tracked by SALD.forwardKlDependencyChainAuditContract, SALD.forwardKlGronwallInstantiationContract, and SALD.forwardKlGronwallSideConditionContract."
  ]
  citedResultInterfaces := [
    "lem:dv_variation remains source-cited through Boucheron Corollary 4.15 or the SLT entropy_duality pattern; no SLT theorem is imported.",
    "eq:LSI-KL-FI remains a local density-test obligation through probability.lsi_to_kl_fi.",
    "lem:gronwall remains a local real-analysis obligation through sald.gronwall.integrating_factor, sald.gronwall.endpoint_calculus, and sald.gronwall.exponent_rewrite.",
    "Transport-velocity existence/minimality is source background from main_body.tex:230-232; the proof only requires a stated transport velocity interface."
  ]
  obligations := [
    "sald.forward_kl.middle_source_to_lean_map",
    "sald.forward_kl.endpoint_schedule_identities",
    "sald.forward_kl.moving_target_dependency_chain",
    "sald.forward_kl.density_boundary_regular",
    "sald.forward_kl.schedule_time_change",
    "sald.forward_kl.kl_derivative",
    "probability.lsi_to_kl_fi",
    "sald.forward_kl.dv_alpha_mgf_monotonicity",
    "sald.forward_kl.dv_finite_log_mgf_witness",
    "sald.forward_kl.dv_energy_bound",
    "sald.forward_kl.coefficient_chain_audit",
    "sald.forward_kl.gronwall_application",
    "sald.forward_kl.gronwall_side_conditions"
  ]
  lowerPacket := [
    "Preferred lower target: refine SALD.forwardKlEndpointScheduleContract and sald.forward_kl.endpoint_schedule_identities for s(0)=0, S=s(T), t(s(T))=T, and tilde_pi_{s(t)}=pi_t.",
    "Keep the source proof route derivative -> LSI -> DV -> Gronwall; do not introduce path-space, Girsanov, Pinsker, Talagrand, or a different Gronwall normalization.",
    "If the endpoint slice is blocked, refine exactly one alternative interface: slowed-target transport, density/boundary side conditions, DV finite-log-mgf/common-space witness, or Gronwall coefficient regularity.",
    "Preserve the differential inequality from appendix.tex:239-241 and the terminal theorem display in main_body.tex:243-246 byte-for-byte at the contract level."
  ]
  reviewerChecklist := [
    "Every source step in appendix.tex:168-252 is classified as a Lean contract, cited result, or named proof obligation.",
    "SALD.continuousSaldContract includes sald.forward_kl.middle_source_to_lean_map and still keeps all analytic backends at obligation or source-cited status.",
    "SALD.forwardKlProofDag exposes ASTIS.SALD.forward_KL.middle_source_to_lean_map before lower proof-search blocks.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes SALD.cycle14ForwardKlMiddleContract, sald.forward_kl.middle_source_to_lean_map, and sald.forward_kl.endpoint_schedule_identities.",
    "The source index still excludes sald_version_2.tex and no analytic dependency is marked formalized."
  ]
  status := ProofStatus.obligation