AutoSamplingTheory.SALD.cycle14ForwardKlUpperPacket

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 cycle14ForwardKlUpperPacket : 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 select the theorem-level moving-target side conditions as the next lower target: endpoint schedule identities, transport/Fokker--Planck interfaces, DV finite-log-mgf witness, and Gronwall coefficient regularity along the original derivative -> LSI -> DV -> Gronwall route.

sourceLabels : List String (explicit)

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

Ordered data items

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

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, the residual alpha-complexity integral, and the scalar coefficients a(t)=dot{s}(t)*C_LSI(t)-(1/2)*dot{s}(t)^(-1)*alpha^(-1) and b(t)=(1/2)*dot{s}(t)^(-1)*E_alpha(pi_t,v_t).
3. Treat endpoint schedule identities, density/boundary regularity, transport/Fokker--Planck backends, LSI-to-KL/FI, DV, finite-log-mgf monotonicity, and Gronwall regularity 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 packet.
2. Do not replace the paper route derivative -> LSI -> DV -> Gronwall with Pinsker, Talagrand, Girsanov, path-space, or another entropy method.
3. Do not add endpoint, positivity, regularity, finite-log-mgf, absolute-continuity, or integrability assumptions silently to the theorem statement.
4. Do not change the discrete or general moving-target theorem statements while refining this continuous forward-KL packet.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly one interface: SALD.forwardKlEndpointScheduleContract, SALD.forwardKlMovingTargetDependencyContract, SALD.forwardKlGronwallSideConditionContract, SALD.forwardKlDerivativeSideConditionContract, or the named obligations sald.forward_kl.endpoint_schedule_identities, sald.forward_kl.moving_target_dependency_chain, and sald.forward_kl.gronwall_side_conditions.
2. Preferred lower slice: isolate endpoint schedule identities s(0)=0, S=s(T), t(s(T))=T, and tilde_pi_{s(t)}=pi_t in SALD.forwardKlEndpointScheduleContract without adding them as theorem hypotheses.
3. Alternative lower slices: transport velocity for the slowed target, density/boundary side conditions for the KL derivative, finite log-mgf/common-space witness for DV, or continuity/integrability of the Gronwall coefficients a(t) and b(t).
4. Keep the differential inequality from appendix.tex:239-241 and the terminal theorem display in main_body.tex:243-246 unchanged.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.continuousSaldContract still lists the moving-target, derivative side-condition, DV witness, coefficient-chain, Gronwall-side-condition, derivative, DV-energy, and Gronwall obligations.
2. SALD.forwardKlProofDag routes thm:forward-KL through moving_target_dependencies before derivative, DV-energy, and Gronwall proof search.
3. SALD.forwardKlEndpointScheduleContract, SALD.forwardKlMovingTargetDependencyContract, and SALD.forwardKlGronwallSideConditionContract record endpoint identities and Gronwall regularity as obligations, not hidden theorem assumptions.
4. research-wiki/source-index/SALD_original.jsonl contains thm:forward-KL, eq:LSI-KL-FI, lem:dv_variation, and lem:gronwall while excluding sald_version_2.tex.
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 cycle14ForwardKlUpperPacket : ForwardKlUpperPacket where
  objective := "Keep thm:forward-KL fixed and select the theorem-level moving-target side conditions as the next lower target: endpoint schedule identities, transport/Fokker--Planck interfaces, DV finite-log-mgf witness, and Gronwall coefficient regularity along the original derivative -> LSI -> DV -> Gronwall route."
  sourceLabels := [
    "thm:forward-KL",
    "eq:SALD",
    "eq:FP-eq",
    "eq:LSI-KL-FI",
    "def:alpha-complexity",
    "lem:dv_variation",
    "lem:gronwall"
  ]
  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, the residual alpha-complexity integral, and the scalar coefficients a(t)=dot{s}(t)*C_LSI(t)-(1/2)*dot{s}(t)^(-1)*alpha^(-1) and b(t)=(1/2)*dot{s}(t)^(-1)*E_alpha(pi_t,v_t).",
    "Treat endpoint schedule identities, density/boundary regularity, transport/Fokker--Planck backends, LSI-to-KL/FI, DV, finite-log-mgf monotonicity, and Gronwall regularity as obligations or source-cited facts until local Lean proofs replace them."
  ]
  nonGoals := [
    "Do not restate or prove thm:forward-KL in this packet.",
    "Do not replace the paper route derivative -> LSI -> DV -> Gronwall with Pinsker, Talagrand, Girsanov, path-space, or another entropy method.",
    "Do not add endpoint, positivity, regularity, finite-log-mgf, absolute-continuity, or integrability assumptions silently to the theorem statement.",
    "Do not change the discrete or general moving-target theorem statements while refining this continuous forward-KL packet."
  ]
  lowerPacket := [
    "Target exactly one interface: SALD.forwardKlEndpointScheduleContract, SALD.forwardKlMovingTargetDependencyContract, SALD.forwardKlGronwallSideConditionContract, SALD.forwardKlDerivativeSideConditionContract, or the named obligations sald.forward_kl.endpoint_schedule_identities, sald.forward_kl.moving_target_dependency_chain, and sald.forward_kl.gronwall_side_conditions.",
    "Preferred lower slice: isolate endpoint schedule identities s(0)=0, S=s(T), t(s(T))=T, and tilde_pi_{s(t)}=pi_t in SALD.forwardKlEndpointScheduleContract without adding them as theorem hypotheses.",
    "Alternative lower slices: transport velocity for the slowed target, density/boundary side conditions for the KL derivative, finite log-mgf/common-space witness for DV, or continuity/integrability of the Gronwall coefficients a(t) and b(t).",
    "Keep the differential inequality from appendix.tex:239-241 and the terminal theorem display in main_body.tex:243-246 unchanged."
  ]
  reviewerChecklist := [
    "SALD.continuousSaldContract still lists the moving-target, derivative side-condition, DV witness, coefficient-chain, Gronwall-side-condition, derivative, DV-energy, and Gronwall obligations.",
    "SALD.forwardKlProofDag routes thm:forward-KL through moving_target_dependencies before derivative, DV-energy, and Gronwall proof search.",
    "SALD.forwardKlEndpointScheduleContract, SALD.forwardKlMovingTargetDependencyContract, and SALD.forwardKlGronwallSideConditionContract record endpoint identities and Gronwall regularity as obligations, not hidden theorem assumptions.",
    "research-wiki/source-index/SALD_original.jsonl contains thm:forward-KL, eq:LSI-KL-FI, lem:dv_variation, and lem:gronwall while excluding sald_version_2.tex.",
    "No analytic dependency is marked formalized and no fake proof closure is introduced."
  ]
  status := ProofStatus.obligation