AutoSamplingTheory.SALD.cycle11DiscreteForwardKlUpperPacket

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 cycle11DiscreteForwardKlUpperPacket : 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 isolate the discrete Donsker--Varadhan finite-log-mgf witness used for the EM interpolation velocity term in appendix.tex:493-523.

sourceLabels : List String (explicit)

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

Ordered data items

1. thm:forward-KL-discrete
2. lem:dv_variation
3. def:alpha-complexity
4. eq:frozen_interp_terminal_disc_prop_additive_final
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:301-323 and appendix.tex:493-523 for this refinement, with sald_version_2.tex excluded.
2. Preserve the EM interpolation law hat rho_s, the DV choice nu=hat rho_s, mu=tilde pi_s, and Z=alpha*||v_{t(s)}||^2 exactly.
3. Reuse the continuous alpha0-to-alpha monotonicity obligation for the pi_t log-mgf, but keep the discrete common-space and absolute-continuity interfaces separate because nu is now hat rho_s.
4. Treat DV, EM endpoint laws, density regularity, finite log-mgf, and positive-alpha scaling as obligations or source-cited dependencies until local Lean proofs replace them.

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 cycle.
2. Do not replace the source DV step by path-space, Girsanov, Pinsker, Talagrand, or another entropy method.
3. Do not add a new finite-mgf or absolute-continuity hypothesis to the theorem statement.
4. Do not change the coefficient dot t(s)^2*(alpha^(-1)*K_s+E_alpha(pi_{t(s)},v_{t(s)})) or the later dot{s}(t)^(-1)*alpha^(-1) term.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly one interface: SALD.discreteForwardKlDvFiniteLogMgfWitnessContract or SALD.discreteForwardKlDvFiniteLogMgfWitnessObligation.
2. Refine one backend only: EM-interpolation common-space/absolute-continuity, measurability of ||v_{t(s)}||^2, alpha0-to-alpha finite-log-mgf reuse, positive-alpha scaling, or dot t(s)^2 coefficient preservation.
3. Use appendix.tex:493-523 as the source line ledger and keep lem:dv_variation source-cited.
4. Keep SALD.discreteForwardKlStatementContract and the theorem bound in main_body.tex:309-323 unchanged.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.discreteSaldContract lists SALD.discreteForwardKlDvFiniteLogMgfWitnessObligation before SALD.discreteForwardKlDvVelocityObligation.
2. SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.dv_finite_log_mgf_witness before the Gronwall accumulation block.
3. SALD.discreteForwardKlDvVelocityObligation depends on sald.discrete_forward_kl.dv_finite_log_mgf_witness and keeps the appendix.tex:493-523 coefficient.
4. The conversion window and proof-obligation ledger mention the discrete DV witness under thm:forward-KL-discrete.
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 cycle11DiscreteForwardKlUpperPacket : DiscreteForwardKlUpperPacket where
  objective := "Keep thm:forward-KL-discrete fixed and isolate the discrete Donsker--Varadhan finite-log-mgf witness used for the EM interpolation velocity term in appendix.tex:493-523."
  sourceLabels := [
    "thm:forward-KL-discrete",
    "lem:dv_variation",
    "def:alpha-complexity",
    "eq:frozen_interp_terminal_disc_prop_additive_final",
    "lem:gronwall",
    "eq:LSI-KL-FI"
  ]
  modeDiscipline := [
    "faithfulPaper: use main_body.tex:301-323 and appendix.tex:493-523 for this refinement, with sald_version_2.tex excluded.",
    "Preserve the EM interpolation law hat rho_s, the DV choice nu=hat rho_s, mu=tilde pi_s, and Z=alpha*||v_{t(s)}||^2 exactly.",
    "Reuse the continuous alpha0-to-alpha monotonicity obligation for the pi_t log-mgf, but keep the discrete common-space and absolute-continuity interfaces separate because nu is now hat rho_s.",
    "Treat DV, EM endpoint laws, density regularity, finite log-mgf, and positive-alpha scaling as obligations or source-cited dependencies until local Lean proofs replace them."
  ]
  nonGoals := [
    "Do not restate or prove thm:forward-KL-discrete in this cycle.",
    "Do not replace the source DV step by path-space, Girsanov, Pinsker, Talagrand, or another entropy method.",
    "Do not add a new finite-mgf or absolute-continuity hypothesis to the theorem statement.",
    "Do not change the coefficient dot t(s)^2*(alpha^(-1)*K_s+E_alpha(pi_{t(s)},v_{t(s)})) or the later dot{s}(t)^(-1)*alpha^(-1) term."
  ]
  lowerPacket := [
    "Target exactly one interface: SALD.discreteForwardKlDvFiniteLogMgfWitnessContract or SALD.discreteForwardKlDvFiniteLogMgfWitnessObligation.",
    "Refine one backend only: EM-interpolation common-space/absolute-continuity, measurability of ||v_{t(s)}||^2, alpha0-to-alpha finite-log-mgf reuse, positive-alpha scaling, or dot t(s)^2 coefficient preservation.",
    "Use appendix.tex:493-523 as the source line ledger and keep lem:dv_variation source-cited.",
    "Keep SALD.discreteForwardKlStatementContract and the theorem bound in main_body.tex:309-323 unchanged."
  ]
  reviewerChecklist := [
    "SALD.discreteSaldContract lists SALD.discreteForwardKlDvFiniteLogMgfWitnessObligation before SALD.discreteForwardKlDvVelocityObligation.",
    "SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.dv_finite_log_mgf_witness before the Gronwall accumulation block.",
    "SALD.discreteForwardKlDvVelocityObligation depends on sald.discrete_forward_kl.dv_finite_log_mgf_witness and keeps the appendix.tex:493-523 coefficient.",
    "The conversion window and proof-obligation ledger mention the discrete DV witness under thm:forward-KL-discrete.",
    "No analytic dependency is marked formalized and no fake proof closure is introduced."
  ]
  status := ProofStatus.obligation