AutoSamplingTheory.SALD.cycle30ForwardKlMiddleContract

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 cycle30ForwardKlMiddleContract :
    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-30 upper derivative-side target into a lower-ready map for sald.forward_kl.density_boundary_regular, with appendix.tex:168-185 as the first sub-slice and appendix.tex:187-208 as a follow-on density/boundary slice before the separate LSI, time-change, DV, and Gronwall obligations.

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, inverse slowdown notation, LSI constants, alpha-complexity assumption, alpha range, and terminal KL display; this middle packet does not change any of them.
2. appendix.tex:168-174 differentiates KL(rho_s||tilde_pi_s), passes the derivative through the integral, and uses int partial_s rho_s dx=0; the Lean target must expose mass conservation and differentiation-under-integral hypotheses.
3. appendix.tex:176-185 substitutes the SALD Fokker-Planck equation partial_s rho_s=div(rho_s*nabla log(rho_s/tilde_pi_s)) and integrates by parts to identify the first term as -FI(rho_s||tilde_pi_s).
4. appendix.tex:187-197 states that v_t transports pi_t and that tilde_v_s=dot{t}(s)*v_{t(s)} transports tilde_pi_s; this is a follow-on transport side condition, not part of the first density/FI slice.
5. appendix.tex:199-208 evaluates the target derivative term by integration by parts and Cauchy--Schwarz/Young, preserving the exact split (1/2)*FI+(1/2)*||tilde_v_s||^2.
6. appendix.tex:210-228 applies the LSI bridge and inverse-schedule chain rule only after the density/boundary and transport slices have produced the s-derivative inequality.

leanStepMap : List String (explicit)

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

Ordered data items

1. Route the selected lower target through SALD.forwardKlDerivativeSideConditionContract, SALD.forwardKlDensityBoundaryObligation, and sald.forward_kl.density_boundary_regular.
2. Use SALD.forwardKlDerivativeCandidateContract only as the parent derivative route; do not promote sald.forward_kl.kl_derivative before the density/boundary side conditions are available.
3. Keep FokkerPlanckContract, KLContract, and FIContract as vocabulary/backends for appendix.tex:168-185; the paper's smooth-density, positivity, boundary, and domination assumptions remain explicit source gaps.
4. Keep TransportVelocityContract and SALD.forwardKlScheduleTimeChangeObligation as sibling obligations for appendix.tex:187-228.
5. Keep SALD.saldLsiKlFiDensityTestContract, SALD.forwardKlDvFiniteLogMgfWitnessContract, and SALD.forwardKlGronwallSideConditionContract unchanged; they are downstream of this derivative-side middle packet.
6. This middle packet adds a workflow obligation sald.forward_kl.cycle30_derivative_side_middle and no theorem-level assumption.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. No SLT theorem applies to the derivative-side density, boundary, mass-conservation, or integration-by-parts interfaces.
2. eq:FP-eq is a local Fokker-Planck/SDE backend obligation for SALD, not an external cited theorem.
3. eq:LSI-KL-FI remains the cycle-29 density-test obligation and starts after the first derivative slice.
4. lem:dv_variation and lem:gronwall are downstream source-cited or local-analysis dependencies and are not reopened in this middle packet.

obligations : List String (explicit)

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

Ordered data items

1. sald.forward_kl.cycle30_derivative_side_middle
2. sald.forward_kl.cycle30_derivative_side_upper
3. sald.forward_kl.density_boundary_regular
4. sald.forward_kl.schedule_time_change
5. sald.forward_kl.kl_derivative
6. probability.lsi_to_kl_fi
7. sald.forward_kl.dv_finite_log_mgf_witness
8. 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. Target exactly SALD.forwardKlDerivativeSideConditionContract / SALD.forwardKlDensityBoundaryObligation / sald.forward_kl.density_boundary_regular.
2. First lower sub-slice: appendix.tex:168-185 only. Expose mass conservation, differentiation under the KL integral, the SALD Fokker-Planck equation, boundary/no-flux or decay assumptions, and the FI identification.
3. If appendix.tex:168-185 is blocked, refine the missing density, domination, positivity, or integration-by-parts interface as a proof obligation rather than adding a theorem assumption.
4. Second sub-slice after the first is stable: appendix.tex:187-208 target-side transport, integration by parts, and Young's inequality with the exact 1/2 coefficients.
5. Leave appendix.tex:210-228 time change, eq:LSI-KL-FI, the DV finite-log-mgf witness, coefficient-chain audit, and Gronwall side conditions as named downstream obligations.

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.cycle30_derivative_side_middle between the upper packet and the derivative block.
2. SALD.continuousSaldContract lists SALD.cycle30ForwardKlDerivativeSideMiddleObligation while keeping thm:forward-KL contract-only.
3. SALD.saldDependenciesForLabel "thm:forward-KL" includes SALD.cycle30ForwardKlMiddleContract and sald.forward_kl.cycle30_derivative_side_middle.
4. The conversion window, proof-obligation ledger, and SLT audit classify cycle 30 middle as derivative-side source-to-Lean synchronization, not as a proof of the KL derivative.
5. 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 cycle30ForwardKlMiddleContract :
    ForwardKlMiddleSourceToLeanContract where
  sourceStatement := saldForwardKlSource
  sourceProof := saldForwardKlProofSource
  derivativeSource := saldForwardKlDerivativeSource
  dvSource := saldForwardKlDvEnergySource
  gronwallSource := saldForwardKlGronwallSource
  objective := "Translate the cycle-30 upper derivative-side target into a lower-ready map for sald.forward_kl.density_boundary_regular, with appendix.tex:168-185 as the first sub-slice and appendix.tex:187-208 as a follow-on density/boundary slice before the separate LSI, time-change, DV, and Gronwall obligations."
  sourceStepMap := [
    "main_body.tex:238-247 fixes the theorem statement, inverse slowdown notation, LSI constants, alpha-complexity assumption, alpha range, and terminal KL display; this middle packet does not change any of them.",
    "appendix.tex:168-174 differentiates KL(rho_s||tilde_pi_s), passes the derivative through the integral, and uses int partial_s rho_s dx=0; the Lean target must expose mass conservation and differentiation-under-integral hypotheses.",
    "appendix.tex:176-185 substitutes the SALD Fokker-Planck equation partial_s rho_s=div(rho_s*nabla log(rho_s/tilde_pi_s)) and integrates by parts to identify the first term as -FI(rho_s||tilde_pi_s).",
    "appendix.tex:187-197 states that v_t transports pi_t and that tilde_v_s=dot{t}(s)*v_{t(s)} transports tilde_pi_s; this is a follow-on transport side condition, not part of the first density/FI slice.",
    "appendix.tex:199-208 evaluates the target derivative term by integration by parts and Cauchy--Schwarz/Young, preserving the exact split (1/2)*FI+(1/2)*||tilde_v_s||^2.",
    "appendix.tex:210-228 applies the LSI bridge and inverse-schedule chain rule only after the density/boundary and transport slices have produced the s-derivative inequality."
  ]
  leanStepMap := [
    "Route the selected lower target through SALD.forwardKlDerivativeSideConditionContract, SALD.forwardKlDensityBoundaryObligation, and sald.forward_kl.density_boundary_regular.",
    "Use SALD.forwardKlDerivativeCandidateContract only as the parent derivative route; do not promote sald.forward_kl.kl_derivative before the density/boundary side conditions are available.",
    "Keep FokkerPlanckContract, KLContract, and FIContract as vocabulary/backends for appendix.tex:168-185; the paper's smooth-density, positivity, boundary, and domination assumptions remain explicit source gaps.",
    "Keep TransportVelocityContract and SALD.forwardKlScheduleTimeChangeObligation as sibling obligations for appendix.tex:187-228.",
    "Keep SALD.saldLsiKlFiDensityTestContract, SALD.forwardKlDvFiniteLogMgfWitnessContract, and SALD.forwardKlGronwallSideConditionContract unchanged; they are downstream of this derivative-side middle packet.",
    "This middle packet adds a workflow obligation sald.forward_kl.cycle30_derivative_side_middle and no theorem-level assumption."
  ]
  citedResultInterfaces := [
    "No SLT theorem applies to the derivative-side density, boundary, mass-conservation, or integration-by-parts interfaces.",
    "eq:FP-eq is a local Fokker-Planck/SDE backend obligation for SALD, not an external cited theorem.",
    "eq:LSI-KL-FI remains the cycle-29 density-test obligation and starts after the first derivative slice.",
    "lem:dv_variation and lem:gronwall are downstream source-cited or local-analysis dependencies and are not reopened in this middle packet."
  ]
  obligations := [
    "sald.forward_kl.cycle30_derivative_side_middle",
    "sald.forward_kl.cycle30_derivative_side_upper",
    "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_finite_log_mgf_witness",
    "sald.forward_kl.gronwall_side_conditions"
  ]
  lowerPacket := [
    "Target exactly SALD.forwardKlDerivativeSideConditionContract / SALD.forwardKlDensityBoundaryObligation / sald.forward_kl.density_boundary_regular.",
    "First lower sub-slice: appendix.tex:168-185 only. Expose mass conservation, differentiation under the KL integral, the SALD Fokker-Planck equation, boundary/no-flux or decay assumptions, and the FI identification.",
    "If appendix.tex:168-185 is blocked, refine the missing density, domination, positivity, or integration-by-parts interface as a proof obligation rather than adding a theorem assumption.",
    "Second sub-slice after the first is stable: appendix.tex:187-208 target-side transport, integration by parts, and Young's inequality with the exact 1/2 coefficients.",
    "Leave appendix.tex:210-228 time change, eq:LSI-KL-FI, the DV finite-log-mgf witness, coefficient-chain audit, and Gronwall side conditions as named downstream obligations."
  ]
  reviewerChecklist := [
    "SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle30_derivative_side_middle between the upper packet and the derivative block.",
    "SALD.continuousSaldContract lists SALD.cycle30ForwardKlDerivativeSideMiddleObligation while keeping thm:forward-KL contract-only.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes SALD.cycle30ForwardKlMiddleContract and sald.forward_kl.cycle30_derivative_side_middle.",
    "The conversion window, proof-obligation ledger, and SLT audit classify cycle 30 middle as derivative-side source-to-Lean synchronization, not as a proof of the KL derivative.",
    "No analytic dependency is promoted beyond obligation or source-cited status."
  ]
  status := ProofStatus.obligation

/-- Cycle-34 upper packet for the continuous forward-KL derivative closure sprint.

This packet explicitly checks the proof-closure order and assigns only the
next proof-producing derivative slice inside `appendix.tex:168-228`.  The new
compiled scalar lemmas combine already-supplied analytic inputs; they do not
close the Fokker--Planck, integration-by-parts, LSI density-test, or
time-change analytic backends.
-/