AutoSamplingTheory.SALD.cycle60ForwardKlSkeletonMiddleContract

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

Cycle 60 middle: audit the post-cycle-59 continuous thm:forward-KL route against main_body.tex:238-247 and appendix.tex:164-252, verify that the five source-cited analytic interfaces are consumed in the paper order, and keep SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative over appendix.tex:168-228 as the lower packet without changing theorem constants, statements, labels, or statuses.

sourceStepMap : List String (explicit)

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

Ordered data items

1. main_body.tex:238-247 fixes the theorem statement: pi_t satisfies LSI with C_LSI(t)>=0, E_alpha0(pi_t,v_t)<+infty for the transport velocity field, alpha lies in (0,alpha0], rho_s is the SALD law, and the terminal bound keeps the two exponent factors and residual alpha-complexity integral.
2. appendix.tex:168-185 differentiates KL(rho_s||tilde pi_s), drops the mass term by int partial_s rho_s=0, substitutes the SALD Fokker--Planck equation, integrates by parts, and identifies the first term as -FI.
3. appendix.tex:187-208 builds the slowed target velocity tilde v_s=dot t(s)*v_{t(s)}, rewrites partial_s tilde pi_s as -div(tilde v_s tilde pi_s), integrates by parts, and applies Cauchy--Schwarz/Young with the exact one-half split.
4. appendix.tex:210-228 applies eq:LSI-KL-FI and the inverse-schedule chain rule to obtain the t-time derivative inequality with coefficient (1/2)*dot{s}(t)^(-1)*||v_t||^2.
5. appendix.tex:230-241 applies lem:dv_variation to Z=alpha*||v_t||^2 under the finite-log-mgf witness, producing the exact pre-Gronwall coefficient dot{s}(t)*C_LSI(t)-(1/2)*dot{s}(t)^(-1)*alpha^(-1).
6. appendix.tex:244-252 applies lem:gronwall, then performs only the source exponent split and residual exponent drop that yield the main-body theorem display.

leanStepMap : List String (explicit)

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

Ordered data items

1. Use SALD.cycle60ForwardKlSkeletonUpperPacket and SALD.cycle60ForwardKlSkeletonObligation as parent route data after the accepted cycle-59 analytic ledger.
2. Keep SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract contractOnly; this middle audit adds no theorem hypotheses.
3. Route appendix.tex:168-228 through SALD.forwardKlDerivativeCandidateContract, SALD.forwardKlDerivativeSideConditionContract, SALD.forwardKlDerivativeObligation, SALD.forwardKlDensityBoundaryObligation, SALD.forwardKlScheduleTimeChangeObligation, sald.forward_kl.density_boundary_regular, sald.forward_kl.schedule_time_change, and sald.forward_kl.kl_derivative.
4. Route appendix.tex:210-217 through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi, preserving density, zero-set convention, admissible sqrt-density test, entropy identity, finite KL/FI, and Fisher-chain obligations.
5. Route appendix.tex:230-241 through dvVariationalFormulaInterface saldDvVariationSource, SALD.saldDvFiniteLogMgfContract, SALD.forwardKlDvFiniteLogMgfWitnessContract, sald.forward_kl.dv_finite_log_mgf_witness, and sald.forward_kl.dv_energy_bound.
6. Route appendix.tex:244-252 through SALD.saldGronwallEndpointCalculusContract, SALD.forwardKlGronwallInstantiationContract, SALD.forwardKlGronwallSideConditionContract, sald.forward_kl.gronwall_side_conditions, and sald.forward_kl.gronwall_application.
7. Keep SALD.discreteForwardKlEmInterpolationSideConditionContract and sald.discrete_forward_kl.em_interpolation_fp visible only as the downstream EM/Fokker--Planck sibling backend for discrete theorem reuse.
8. Select the next lower target exactly as SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative over appendix.tex:168-228.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. lem:gronwall remains the endpoint-safe differentiability/FTC, coefficient-regularity, endpoint-rewrite, interval-integrability, and exponent-display obligation; cycle 60 middle only checks the theorem-specific instantiation.
2. lem:dv_variation remains source-cited with common-space, absolute-continuity, finite-KL, selected-test measurability, finite-log-mgf, and alpha-scaling witnesses.
3. eq:LSI-KL-FI remains the density-test, zero-set convention, admissible-test, entropy-identity, finite KL/FI, and Fisher-chain-rule obligation.
4. The continuous Fokker--Planck/KL derivative identity remains the selected local SDE/measure-analysis backend and is not promoted by this middle audit.
5. The Euler--Maruyama interpolation Fokker--Planck endpoint/conditional-law backend remains a downstream discrete obligation, not a hidden assumption of thm:forward-KL.

obligations : List String (explicit)

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

Ordered data items

1. sald.forward_kl.cycle60_post_cycle59_route
2. sald.forward_kl.cycle60_middle_route_audit
3. sald.forward_kl.kl_derivative
4. sald.forward_kl.density_boundary_regular
5. sald.forward_kl.schedule_time_change
6. probability.lsi_to_kl_fi
7. sald.forward_kl.dv_finite_log_mgf_witness
8. sald.forward_kl.dv_energy_bound
9. sald.forward_kl.gronwall_side_conditions
10. sald.forward_kl.gronwall_application
11. sald.discrete_forward_kl.em_interpolation_fp

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative.
2. First lower sub-slice: appendix.tex:168-185 mass conservation, KL differentiation under the integral, SALD Fokker--Planck substitution, boundary/no-flux integration by parts, and -FI identification.
3. Second lower sub-slice: appendix.tex:187-208 slowed target transport velocity, target integration by parts, Cauchy--Schwarz/Young with the exact 1/2 share, and the L2 velocity term.
4. Third lower sub-slice: appendix.tex:218-228 inverse-schedule chain rule, slowed-velocity square scaling, and dot{s}(t)*dot t(s(t))^2=dot{s}(t)^(-1).
5. Leave LSI/KL/FI, DV finite-log-mgf, Gronwall endpoint/exponent conditions, and EM interpolation as separate named interfaces unless their exact analytic backends compile locally.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.continuousSaldContract lists SALD.cycle60ForwardKlSkeletonMiddleObligation while remaining contractOnly.
2. SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle60_middle_route_audit after ASTIS.SALD.forward_KL.cycle60_post_cycle59_route.
3. SALD.saldDependenciesForLabel "thm:forward-KL" includes SALD.cycle60ForwardKlSkeletonMiddleContract, SALD.cycle60ForwardKlSkeletonMiddleObligation, and sald.forward_kl.cycle60_middle_route_audit.
4. No theorem statement, source coefficient, source label, source-file selection, SLT reuse entry, or analytic backend status is changed.
5. python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass.

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 cycle60ForwardKlSkeletonMiddleContract :
    ForwardKlMiddleSourceToLeanContract where
  sourceStatement := saldForwardKlSource
  sourceProof := saldForwardKlProofSource
  derivativeSource := saldForwardKlDerivativeSource
  dvSource := saldForwardKlDvEnergySource
  gronwallSource := saldForwardKlGronwallSource
  objective := "Cycle 60 middle: audit the post-cycle-59 continuous thm:forward-KL route against main_body.tex:238-247 and appendix.tex:164-252, verify that the five source-cited analytic interfaces are consumed in the paper order, and keep SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative over appendix.tex:168-228 as the lower packet without changing theorem constants, statements, labels, or statuses."
  sourceStepMap := [
    "main_body.tex:238-247 fixes the theorem statement: pi_t satisfies LSI with C_LSI(t)>=0, E_alpha0(pi_t,v_t)<+infty for the transport velocity field, alpha lies in (0,alpha0], rho_s is the SALD law, and the terminal bound keeps the two exponent factors and residual alpha-complexity integral.",
    "appendix.tex:168-185 differentiates KL(rho_s||tilde pi_s), drops the mass term by int partial_s rho_s=0, substitutes the SALD Fokker--Planck equation, integrates by parts, and identifies the first term as -FI.",
    "appendix.tex:187-208 builds the slowed target velocity tilde v_s=dot t(s)*v_{t(s)}, rewrites partial_s tilde pi_s as -div(tilde v_s tilde pi_s), integrates by parts, and applies Cauchy--Schwarz/Young with the exact one-half split.",
    "appendix.tex:210-228 applies eq:LSI-KL-FI and the inverse-schedule chain rule to obtain the t-time derivative inequality with coefficient (1/2)*dot{s}(t)^(-1)*||v_t||^2.",
    "appendix.tex:230-241 applies lem:dv_variation to Z=alpha*||v_t||^2 under the finite-log-mgf witness, producing the exact pre-Gronwall coefficient dot{s}(t)*C_LSI(t)-(1/2)*dot{s}(t)^(-1)*alpha^(-1).",
    "appendix.tex:244-252 applies lem:gronwall, then performs only the source exponent split and residual exponent drop that yield the main-body theorem display."
  ]
  leanStepMap := [
    "Use SALD.cycle60ForwardKlSkeletonUpperPacket and SALD.cycle60ForwardKlSkeletonObligation as parent route data after the accepted cycle-59 analytic ledger.",
    "Keep SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract contractOnly; this middle audit adds no theorem hypotheses.",
    "Route appendix.tex:168-228 through SALD.forwardKlDerivativeCandidateContract, SALD.forwardKlDerivativeSideConditionContract, SALD.forwardKlDerivativeObligation, SALD.forwardKlDensityBoundaryObligation, SALD.forwardKlScheduleTimeChangeObligation, sald.forward_kl.density_boundary_regular, sald.forward_kl.schedule_time_change, and sald.forward_kl.kl_derivative.",
    "Route appendix.tex:210-217 through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi, preserving density, zero-set convention, admissible sqrt-density test, entropy identity, finite KL/FI, and Fisher-chain obligations.",
    "Route appendix.tex:230-241 through dvVariationalFormulaInterface saldDvVariationSource, SALD.saldDvFiniteLogMgfContract, SALD.forwardKlDvFiniteLogMgfWitnessContract, sald.forward_kl.dv_finite_log_mgf_witness, and sald.forward_kl.dv_energy_bound.",
    "Route appendix.tex:244-252 through SALD.saldGronwallEndpointCalculusContract, SALD.forwardKlGronwallInstantiationContract, SALD.forwardKlGronwallSideConditionContract, sald.forward_kl.gronwall_side_conditions, and sald.forward_kl.gronwall_application.",
    "Keep SALD.discreteForwardKlEmInterpolationSideConditionContract and sald.discrete_forward_kl.em_interpolation_fp visible only as the downstream EM/Fokker--Planck sibling backend for discrete theorem reuse.",
    "Select the next lower target exactly as SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative over appendix.tex:168-228."
  ]
  citedResultInterfaces := [
    "lem:gronwall remains the endpoint-safe differentiability/FTC, coefficient-regularity, endpoint-rewrite, interval-integrability, and exponent-display obligation; cycle 60 middle only checks the theorem-specific instantiation.",
    "lem:dv_variation remains source-cited with common-space, absolute-continuity, finite-KL, selected-test measurability, finite-log-mgf, and alpha-scaling witnesses.",
    "eq:LSI-KL-FI remains the density-test, zero-set convention, admissible-test, entropy-identity, finite KL/FI, and Fisher-chain-rule obligation.",
    "The continuous Fokker--Planck/KL derivative identity remains the selected local SDE/measure-analysis backend and is not promoted by this middle audit.",
    "The Euler--Maruyama interpolation Fokker--Planck endpoint/conditional-law backend remains a downstream discrete obligation, not a hidden assumption of thm:forward-KL."
  ]
  obligations := [
    "sald.forward_kl.cycle60_post_cycle59_route",
    "sald.forward_kl.cycle60_middle_route_audit",
    "sald.forward_kl.kl_derivative",
    "sald.forward_kl.density_boundary_regular",
    "sald.forward_kl.schedule_time_change",
    "probability.lsi_to_kl_fi",
    "sald.forward_kl.dv_finite_log_mgf_witness",
    "sald.forward_kl.dv_energy_bound",
    "sald.forward_kl.gronwall_side_conditions",
    "sald.forward_kl.gronwall_application",
    "sald.discrete_forward_kl.em_interpolation_fp"
  ]
  lowerPacket := [
    "Target exactly SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative.",
    "First lower sub-slice: appendix.tex:168-185 mass conservation, KL differentiation under the integral, SALD Fokker--Planck substitution, boundary/no-flux integration by parts, and -FI identification.",
    "Second lower sub-slice: appendix.tex:187-208 slowed target transport velocity, target integration by parts, Cauchy--Schwarz/Young with the exact 1/2 share, and the L2 velocity term.",
    "Third lower sub-slice: appendix.tex:218-228 inverse-schedule chain rule, slowed-velocity square scaling, and dot{s}(t)*dot t(s(t))^2=dot{s}(t)^(-1).",
    "Leave LSI/KL/FI, DV finite-log-mgf, Gronwall endpoint/exponent conditions, and EM interpolation as separate named interfaces unless their exact analytic backends compile locally."
  ]
  reviewerChecklist := [
    "SALD.continuousSaldContract lists SALD.cycle60ForwardKlSkeletonMiddleObligation while remaining contractOnly.",
    "SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle60_middle_route_audit after ASTIS.SALD.forward_KL.cycle60_post_cycle59_route.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes SALD.cycle60ForwardKlSkeletonMiddleContract, SALD.cycle60ForwardKlSkeletonMiddleObligation, and sald.forward_kl.cycle60_middle_route_audit.",
    "No theorem statement, source coefficient, source label, source-file selection, SLT reuse entry, or analytic backend status is changed.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

/-- Cycle-60 middle obligation tying the post-cycle-59 route audit to the
selected continuous derivative/Fokker--Planck lower packet. -/