AutoSamplingTheory.SALD.cycle34ForwardKlDerivativeUpperPacket

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 cycle34ForwardKlDerivativeUpperPacket : 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.

Proof-closure priority check: (1) lem:gronwall remains a local real-analysis obligation, (2) lem:dv_variation remains source-cited with scalar consequences, (3) eq:LSI-KL-FI remains an obligation after cycle 33 scalar density-test lemmas, so this cycle follows item (4) by narrowing the continuous forward-KL Fokker-Planck/KL derivative block to proof-producing scalar lemmas for appendix.tex:168-217 before assigning the EM interpolation backend.

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. lem:dv_variation
6. 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:168-228 from the original source root; sald_version_2.tex remains excluded.
2. Keep the theorem statement and paper route fixed: KL differentiation, SALD Fokker-Planck, slowed-target transport, Cauchy--Schwarz/Young, LSI, inverse-schedule time change, DV, then Gronwall.
3. Use SALD.forwardKlPostYoungDerivativeBoundScalar and SALD.forwardKlLsiDerivativeBoundScalar only after the analytic identities they require are supplied by the named derivative and LSI obligations.
4. Keep mass conservation, differentiation under the integral, Fokker--Planck, boundary/no-flux, target transport, LSI-to-KL/FI, inverse-schedule calculus, DV, and Gronwall below formalized status unless a compiled local proof replaces the obligation.

nonGoals : List String (explicit)

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

Ordered data items

1. Do not rebaseline the source index or expand transcript ledgers unless a reviewer finds a blocking source-anchor defect.
2. Do not restate or prove thm:forward-KL in this packet.
3. Do not add smoothness, density, absolute-continuity, endpoint, positivity, boundary, LSI, inverse-function, finite-log-mgf, or interval-integrability assumptions to the theorem statement.
4. Do not replace the source route with Girsanov, Pinsker, Talagrand, path-space comparison, PI-to-LSI, or the general moving-target theorem.
5. Do not promote the KL derivative, Fokker--Planck backend, integration by parts, LSI-to-KL/FI, schedule time change, DV, or Gronwall.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.forwardKlPostYoungDerivativeBoundScalar and SALD.forwardKlLsiDerivativeBoundScalar as the first proof-producing lower slice, registered by SALD.cycle34ForwardKlDerivativeScalarObligation / sald.forward_kl.cycle34_derivative_scalar.
2. Middle must keep the source-to-Lean map synchronized for appendix.tex:168-217: first-term identity from cycle 30, target-side Young bound, and LSI half-Fisher comparison.
3. If lower continues beyond the compiled scalar lemmas, the next sub-slice is appendix.tex:187-208 target-side transport/integration-by-parts and the exact Young 1/2 split, still as inputs to the scalar lemma.
4. For appendix.tex:218-228, use SALD.forwardKlTimeChangedDerivativeBoundScalar only after sald.forward_kl.schedule_time_change supplies the analytic chain-rule, velocity-square scaling, inverse-derivative, and positivity inputs.
5. Keep DV, coefficient-chain audit, Gronwall side conditions, endpoint rewrites, and EM interpolation work out of this lower attempt.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.forwardKlPostYoungDerivativeBoundScalar proves only the Real arithmetic from firstTerm=-FI and targetTerm <= (1/2)*FI+(1/2)*velocitySq to the post-Young derivative bound.
2. SALD.forwardKlLsiDerivativeBoundScalar proves only the Real-order LSI substitution from C_LSI*K <= (1/2)*FI to the post-LSI derivative bound.
3. SALD.forwardKlTimeChangedDerivativeBoundScalar proves only the Real-order inverse-schedule handoff after the analytic chain rule, velocity scaling, and inverse-derivative identities are supplied.
4. SALD.forwardKlProofDag routes the cycle-34 derivative scalar block before ASTIS.SALD.forward_KL.derivative and keeps sald.forward_kl.kl_derivative as an obligation.
5. SALD.saldDependenciesForLabel "thm:forward-KL" includes the cycle-34 packet, obligation, and scalar lemmas without removing cycle-30 derivative-side obligations.
6. No source-cited analytic theorem is marked formalized and the mandatory ASTIS check passes.

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 cycle34ForwardKlDerivativeUpperPacket : ForwardKlUpperPacket where
  objective := "Proof-closure priority check: (1) lem:gronwall remains a local real-analysis obligation, (2) lem:dv_variation remains source-cited with scalar consequences, (3) eq:LSI-KL-FI remains an obligation after cycle 33 scalar density-test lemmas, so this cycle follows item (4) by narrowing the continuous forward-KL Fokker-Planck/KL derivative block to proof-producing scalar lemmas for appendix.tex:168-217 before assigning the EM interpolation backend."
  sourceLabels := [
    "thm:forward-KL",
    "eq:SALD",
    "eq:FP-eq",
    "eq:LSI-KL-FI",
    "lem:dv_variation",
    "lem:gronwall"
  ]
  modeDiscipline := [
    "faithfulPaper: use main_body.tex:238-247 and appendix.tex:168-228 from the original source root; sald_version_2.tex remains excluded.",
    "Keep the theorem statement and paper route fixed: KL differentiation, SALD Fokker-Planck, slowed-target transport, Cauchy--Schwarz/Young, LSI, inverse-schedule time change, DV, then Gronwall.",
    "Use SALD.forwardKlPostYoungDerivativeBoundScalar and SALD.forwardKlLsiDerivativeBoundScalar only after the analytic identities they require are supplied by the named derivative and LSI obligations.",
    "Keep mass conservation, differentiation under the integral, Fokker--Planck, boundary/no-flux, target transport, LSI-to-KL/FI, inverse-schedule calculus, DV, and Gronwall below formalized status unless a compiled local proof replaces the obligation."
  ]
  nonGoals := [
    "Do not rebaseline the source index or expand transcript ledgers unless a reviewer finds a blocking source-anchor defect.",
    "Do not restate or prove thm:forward-KL in this packet.",
    "Do not add smoothness, density, absolute-continuity, endpoint, positivity, boundary, LSI, inverse-function, finite-log-mgf, or interval-integrability assumptions to the theorem statement.",
    "Do not replace the source route with Girsanov, Pinsker, Talagrand, path-space comparison, PI-to-LSI, or the general moving-target theorem.",
    "Do not promote the KL derivative, Fokker--Planck backend, integration by parts, LSI-to-KL/FI, schedule time change, DV, or Gronwall."
  ]
  lowerPacket := [
    "Target exactly SALD.forwardKlPostYoungDerivativeBoundScalar and SALD.forwardKlLsiDerivativeBoundScalar as the first proof-producing lower slice, registered by SALD.cycle34ForwardKlDerivativeScalarObligation / sald.forward_kl.cycle34_derivative_scalar.",
    "Middle must keep the source-to-Lean map synchronized for appendix.tex:168-217: first-term identity from cycle 30, target-side Young bound, and LSI half-Fisher comparison.",
    "If lower continues beyond the compiled scalar lemmas, the next sub-slice is appendix.tex:187-208 target-side transport/integration-by-parts and the exact Young 1/2 split, still as inputs to the scalar lemma.",
    "For appendix.tex:218-228, use SALD.forwardKlTimeChangedDerivativeBoundScalar only after sald.forward_kl.schedule_time_change supplies the analytic chain-rule, velocity-square scaling, inverse-derivative, and positivity inputs.",
    "Keep DV, coefficient-chain audit, Gronwall side conditions, endpoint rewrites, and EM interpolation work out of this lower attempt."
  ]
  reviewerChecklist := [
    "SALD.forwardKlPostYoungDerivativeBoundScalar proves only the Real arithmetic from firstTerm=-FI and targetTerm <= (1/2)*FI+(1/2)*velocitySq to the post-Young derivative bound.",
    "SALD.forwardKlLsiDerivativeBoundScalar proves only the Real-order LSI substitution from C_LSI*K <= (1/2)*FI to the post-LSI derivative bound.",
    "SALD.forwardKlTimeChangedDerivativeBoundScalar proves only the Real-order inverse-schedule handoff after the analytic chain rule, velocity scaling, and inverse-derivative identities are supplied.",
    "SALD.forwardKlProofDag routes the cycle-34 derivative scalar block before ASTIS.SALD.forward_KL.derivative and keeps sald.forward_kl.kl_derivative as an obligation.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes the cycle-34 packet, obligation, and scalar lemmas without removing cycle-30 derivative-side obligations.",
    "No source-cited analytic theorem is marked formalized and the mandatory ASTIS check passes."
  ]
  status := ProofStatus.obligation

/-- Cycle-34 middle map for the continuous forward-KL derivative scalar closure.

This translates the upper packet into the specific Lean handoff for
`appendix.tex:218-228`.  The compiled theorem is pure real arithmetic; the chain
rule, inverse-function identity, velocity scaling, and positivity facts remain
in `sald.forward_kl.schedule_time_change`.
-/