AutoSamplingTheory.SALD.cycle10ForwardKlUpperPacket

Data definition / provenance and workflow record

Meaning and type

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

def cycle10ForwardKlUpperPacket : ForwardKlUpperPacket

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 fixed and sharpen the source dependency audit from the post-Young derivative inequality through LSI, inverse-schedule time change, DV, and Gronwall to the terminal theorem display.

sourceLabels : List String (explicit)

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

Ordered data items

1. thm:forward-KL
2. eq:LSI-KL-FI
3. lem:dv_variation
4. lem:gronwall
5. def:alpha-complexity
6. eq:SALD
7. eq:FP-eq

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper: use main_body.tex:238-247 and appendix.tex:164-252 from the original source root, with sald_version_2.tex excluded.
2. Preserve the source theorem statement, the two initial-error exponent factors, and the residual alpha-complexity integral exactly.
3. Treat the KL derivative, LSI-to-KL/FI bridge, DV formula, inverse-schedule calculus, and Gronwall lemma as obligations or source-cited facts 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 in this cycle.
2. Do not replace the paper route derivative -> LSI -> DV -> Gronwall with Pinsker, Talagrand, Girsanov, or another entropy method.
3. Do not add endpoint, positivity, regularity, finite-log-mgf, or integrability assumptions silently to the theorem statement.
4. Do not merge away the source's two exponent factors or alter the factor (1/2)*dot{s}(t)^(-1)*alpha^(-1).

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly one interface: SALD.forwardKlDependencyChainAuditContract, SALD.forwardKlGronwallSideConditionContract, or the named obligation sald.forward_kl.coefficient_chain_audit.
2. Refine one slice only: LSI coefficient bookkeeping, inverse-schedule scalar rewrite, DV finite-log-mgf witness, Gronwall coefficient regularity, or endpoint/exponent algebra.
3. Use the new sourceLineLedger and scalarSideConditions entries as the checklist; unresolved analytic facts remain proof obligations.
4. Keep thm:forward-KL and continuousForwardKlStatementContract unchanged.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.forwardKlDependencyChainAuditContract has sourceLineLedger, scalarSideConditions, and sourceDependencyClassification entries for appendix.tex:210-252.
2. SALD.continuousSaldContract still lists the moving-target, coefficient-chain, gronwall-side-condition, derivative, DV, and Gronwall obligations.
3. SALD.forwardKlProofDag still routes thm:forward-KL through moving_target_dependencies, coefficient_chain_audit, derivative, dv_energy, and gronwall_application blocks.
4. The source index contains thm:forward-KL, eq:LSI-KL-FI, lem:dv_variation, and lem:gronwall, and 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 cycle10ForwardKlUpperPacket : ForwardKlUpperPacket where
  objective := "Keep thm:forward-KL fixed and sharpen the source dependency audit from the post-Young derivative inequality through LSI, inverse-schedule time change, DV, and Gronwall to the terminal theorem display."
  sourceLabels := [
    "thm:forward-KL",
    "eq:LSI-KL-FI",
    "lem:dv_variation",
    "lem:gronwall",
    "def:alpha-complexity",
    "eq:SALD",
    "eq:FP-eq"
  ]
  modeDiscipline := [
    "faithfulPaper: use main_body.tex:238-247 and appendix.tex:164-252 from the original source root, with sald_version_2.tex excluded.",
    "Preserve the source theorem statement, the two initial-error exponent factors, and the residual alpha-complexity integral exactly.",
    "Treat the KL derivative, LSI-to-KL/FI bridge, DV formula, inverse-schedule calculus, and Gronwall lemma as obligations or source-cited facts until local Lean proofs replace them."
  ]
  nonGoals := [
    "Do not restate or prove thm:forward-KL in this cycle.",
    "Do not replace the paper route derivative -> LSI -> DV -> Gronwall with Pinsker, Talagrand, Girsanov, or another entropy method.",
    "Do not add endpoint, positivity, regularity, finite-log-mgf, or integrability assumptions silently to the theorem statement.",
    "Do not merge away the source's two exponent factors or alter the factor (1/2)*dot{s}(t)^(-1)*alpha^(-1)."
  ]
  lowerPacket := [
    "Target exactly one interface: SALD.forwardKlDependencyChainAuditContract, SALD.forwardKlGronwallSideConditionContract, or the named obligation sald.forward_kl.coefficient_chain_audit.",
    "Refine one slice only: LSI coefficient bookkeeping, inverse-schedule scalar rewrite, DV finite-log-mgf witness, Gronwall coefficient regularity, or endpoint/exponent algebra.",
    "Use the new sourceLineLedger and scalarSideConditions entries as the checklist; unresolved analytic facts remain proof obligations.",
    "Keep thm:forward-KL and continuousForwardKlStatementContract unchanged."
  ]
  reviewerChecklist := [
    "SALD.forwardKlDependencyChainAuditContract has sourceLineLedger, scalarSideConditions, and sourceDependencyClassification entries for appendix.tex:210-252.",
    "SALD.continuousSaldContract still lists the moving-target, coefficient-chain, gronwall-side-condition, derivative, DV, and Gronwall obligations.",
    "SALD.forwardKlProofDag still routes thm:forward-KL through moving_target_dependencies, coefficient_chain_audit, derivative, dv_energy, and gronwall_application blocks.",
    "The source index contains thm:forward-KL, eq:LSI-KL-FI, lem:dv_variation, and lem:gronwall, and sald_version_2.tex remains excluded.",
    "No analytic dependency is marked formalized and no fake proof closure is introduced."
  ]
  status := ProofStatus.obligation