AutoSamplingTheory.SALD.cycle15DiscreteForwardKlUpperPacket

Data definition / provenance and workflow record

Meaning and type

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

def cycle15DiscreteForwardKlUpperPacket : DiscreteForwardKlUpperPacket

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.

objective : String (explicit)

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

Keep thm:forward-KL-discrete fixed and select the Euler--Maruyama interpolation side-condition spine as the next lower target: endpoint laws, conditional-drift Fokker--Planck equation, and stitched KL regularity before the one-step Gamma/Delta defects are accumulated.

sourceLabels : List String (explicit)

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

Ordered data items

1. thm:forward-KL-discrete
2. eq:frozen_interp_terminal_disc_prop_additive_final
3. lem:frozen_delta_cross_lip_sald
4. lem:dv_variation
5. lem:gronwall
6. eq:LSI-KL-FI

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper: use main_body.tex:299-323 and appendix.tex:260-590 from the original source root, with sald_version_2.tex excluded.
2. Preserve the source theorem statement, the linear slowdown t(s)=s/r, the EM interpolation law hat rho_s, the frozen one-step Gamma and Delta coefficients, and the final barGamma/barDelta accumulated-error display.
3. Keep endpoint laws, conditional drift, EM Fokker--Planck, density/boundary regularity, stitched-interval Gronwall regularity, DV, and Gronwall as obligations or source-cited facts until local Lean proofs replace them.
4. Treat SLT one_step_discretization only as a route reference for the EM backend; it is not an imported dependency and is not marked formalized.

nonGoals : List String (explicit)

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

Ordered data items

1. Do not restate or prove thm:forward-KL-discrete in this packet.
2. Do not bundle the EM interpolation, frozen-defect lemma, DV velocity estimate, and accumulated-error bridge into one hidden theorem assumption.
3. Do not change Gamma, Delta, barGamma, barDelta, alpha, alpha', eta, r, or the source step-size condition.
4. Do not replace the paper route EM interpolation -> frozen defect -> LSI -> DV -> Gronwall -> linear-slowdown collection with path-space, Girsanov, Pinsker, Talagrand, or another entropy route.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly one interface: SALD.discreteForwardKlEmInterpolationSideConditionContract, with the first lower slice sald.discrete_forward_kl.em_conditional_fokker_planck.
2. Refine appendix.tex:347-385 only: define bar b_{k,s}, derive partial_s hat rho_s = -div(hat rho_s*bar b_{k,s}) + Delta hat rho_s, and record the Laplacian split relative to tilde pi_s.
3. Keep sald.discrete_forward_kl.em_endpoint_laws and sald.discrete_forward_kl.stitched_interval_regularity as separate obligations; do not discharge them by adding endpoint or smoothness hypotheses to the theorem.
4. When the conditional Fokker--Planck backend is blocked, record the precise missing conditional-expectation, density, or integration-by-parts interface instead of weakening the discrete theorem.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.discreteSaldContract still lists the EM endpoint, conditional Fokker--Planck, stitched-interval, frozen defect, DV witness, Gronwall, and accumulated-error obligations.
2. SALD.discreteForwardKlProofDag routes through ASTIS.SALD.forward_KL_discrete.em_interpolation_side_conditions before derivative, DV velocity, and Gronwall accumulation blocks.
3. SALD.saldDependenciesForLabel "thm:forward-KL-discrete" includes SALD.cycle15DiscreteForwardKlUpperPacket and the EM endpoint, conditional Fokker--Planck, and stitched-interval obligations.
4. The conversion window, proof-obligation ledger, SLT reuse audit, and source index still point to main_body.tex:301 and appendix.tex:260-590, while sald_version_2.tex remains excluded.
5. No analytic dependency is marked formalized and no fake proof closure is introduced.

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 cycle15DiscreteForwardKlUpperPacket : DiscreteForwardKlUpperPacket where
  objective := "Keep thm:forward-KL-discrete fixed and select the Euler--Maruyama interpolation side-condition spine as the next lower target: endpoint laws, conditional-drift Fokker--Planck equation, and stitched KL regularity before the one-step Gamma/Delta defects are accumulated."
  sourceLabels := [
    "thm:forward-KL-discrete",
    "eq:frozen_interp_terminal_disc_prop_additive_final",
    "lem:frozen_delta_cross_lip_sald",
    "lem:dv_variation",
    "lem:gronwall",
    "eq:LSI-KL-FI"
  ]
  modeDiscipline := [
    "faithfulPaper: use main_body.tex:299-323 and appendix.tex:260-590 from the original source root, with sald_version_2.tex excluded.",
    "Preserve the source theorem statement, the linear slowdown t(s)=s/r, the EM interpolation law hat rho_s, the frozen one-step Gamma and Delta coefficients, and the final barGamma/barDelta accumulated-error display.",
    "Keep endpoint laws, conditional drift, EM Fokker--Planck, density/boundary regularity, stitched-interval Gronwall regularity, DV, and Gronwall as obligations or source-cited facts until local Lean proofs replace them.",
    "Treat SLT one_step_discretization only as a route reference for the EM backend; it is not an imported dependency and is not marked formalized."
  ]
  nonGoals := [
    "Do not restate or prove thm:forward-KL-discrete in this packet.",
    "Do not bundle the EM interpolation, frozen-defect lemma, DV velocity estimate, and accumulated-error bridge into one hidden theorem assumption.",
    "Do not change Gamma, Delta, barGamma, barDelta, alpha, alpha', eta, r, or the source step-size condition.",
    "Do not replace the paper route EM interpolation -> frozen defect -> LSI -> DV -> Gronwall -> linear-slowdown collection with path-space, Girsanov, Pinsker, Talagrand, or another entropy route."
  ]
  lowerPacket := [
    "Target exactly one interface: SALD.discreteForwardKlEmInterpolationSideConditionContract, with the first lower slice sald.discrete_forward_kl.em_conditional_fokker_planck.",
    "Refine appendix.tex:347-385 only: define bar b_{k,s}, derive partial_s hat rho_s = -div(hat rho_s*bar b_{k,s}) + Delta hat rho_s, and record the Laplacian split relative to tilde pi_s.",
    "Keep sald.discrete_forward_kl.em_endpoint_laws and sald.discrete_forward_kl.stitched_interval_regularity as separate obligations; do not discharge them by adding endpoint or smoothness hypotheses to the theorem.",
    "When the conditional Fokker--Planck backend is blocked, record the precise missing conditional-expectation, density, or integration-by-parts interface instead of weakening the discrete theorem."
  ]
  reviewerChecklist := [
    "SALD.discreteSaldContract still lists the EM endpoint, conditional Fokker--Planck, stitched-interval, frozen defect, DV witness, Gronwall, and accumulated-error obligations.",
    "SALD.discreteForwardKlProofDag routes through ASTIS.SALD.forward_KL_discrete.em_interpolation_side_conditions before derivative, DV velocity, and Gronwall accumulation blocks.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL-discrete\" includes SALD.cycle15DiscreteForwardKlUpperPacket and the EM endpoint, conditional Fokker--Planck, and stitched-interval obligations.",
    "The conversion window, proof-obligation ledger, SLT reuse audit, and source index still point to main_body.tex:301 and appendix.tex:260-590, while sald_version_2.tex remains excluded.",
    "No analytic dependency is marked formalized and no fake proof closure is introduced."
  ]
  status := ProofStatus.obligation