AutoSamplingTheory.SALD.cycle39ForwardKlDerivativeUpperPacket

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 cycle39ForwardKlDerivativeUpperPacket : 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 before lower assignment: (1) lem:gronwall has cycle 36 local assembly progress but remains an obligation, (2) lem:dv_variation has one-sided scalar consequences while the Boucheron equality remains source-cited, (3) eq:LSI-KL-FI has cycle 38 finite-coordinate Fisher-chain progress but the vector/integral density-test backend remains an obligation, so this cycle follows the requested item (4): close theorem-specific continuous forward-KL Fokker-Planck/KL derivative lemmas for appendix.tex:168-228 before any more ledger work or the item (5) EM interpolation Fokker-Planck 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 proof route fixed: KL differentiation, SALD Fokker-Planck first term, slowed-target transport, Cauchy--Schwarz/Young, LSI, inverse-schedule time change, DV, then Gronwall.
3. Use SALD.forwardKlPreDvDerivativeBoundScalar only as a composition of supplied scalar/analytic inputs; it does not prove the Fokker-Planck, integration-by-parts, LSI density-test, or inverse-schedule backends.
4. Keep Gronwall, DV, LSI/KL/FI, the full KL derivative theorem, and EM interpolation below formalized status unless a compiled local proof for exactly that interface is added.

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, weaken, or prove thm:forward-KL in this packet.
3. Do not add smoothness, density, positivity, absolute-continuity, endpoint, boundary, LSI, inverse-function, finite-log-mgf, or interval-integrability assumptions to the theorem statement.
4. Do not replace the paper route with Girsanov, path-space comparison, the general moving-target theorem, or a PI-based route.
5. Do not start the Euler--Maruyama interpolation Fokker-Planck backend in this lower packet.

lowerPacket : List String (explicit)

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

Ordered data items

1. First lower target: prove or verify a theorem-specific scalar composition around SALD.forwardKlPreDvDerivativeBoundScalar, with all analytic premises explicit and no theorem-status promotion.
2. Second lower target only after the scalar composition is stable: refine SALD.forwardKlDensityBoundaryObligation / sald.forward_kl.density_boundary_regular for appendix.tex:168-185, exposing mass conservation, KL differentiation under the integral, the SALD Fokker-Planck equation, boundary/no-flux or decay, and FI identification.
3. Third lower target if the first two are stable: refine SALD.forwardKlScheduleTimeChangeObligation / sald.forward_kl.schedule_time_change for appendix.tex:191-228, including the chain rule, velocity-square scaling, inverse derivative, and dot{s}(t) positivity/nonzero inputs used by SALD.forwardKlTimeChangedDerivativeBoundScalar.
4. Middle must keep AutoSamplingTheory/SALD.lean, conversion-windows/ASTIS-SALD-001.md, and proof-obligations/ASTIS-SALD-001.md synchronized against the same appendix.tex:168-228 source window.
5. Leave DV finite-log-mgf, coefficient-chain audit, Gronwall side conditions, endpoint rewrites, and EM interpolation work as sibling obligations.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.forwardKlPreDvDerivativeBoundScalar compiles and is only scalar Real/order composition from explicit KL derivative, first-term, Cauchy, LSI, chain-rule, velocity-scaling, and inverse-schedule premises.
2. SALD.cycle39ForwardKlDerivativeUpperPacket and sald.forward_kl.cycle39_derivative_upper are listed in the forward-KL contract, proof DAG, and saldDependenciesForLabel "thm:forward-KL".
3. sald.forward_kl.kl_derivative, sald.forward_kl.density_boundary_regular, sald.forward_kl.schedule_time_change, probability.lsi_to_kl_fi, lem:dv_variation, and lem:gronwall remain obligations or source-cited dependencies.
4. No source-index rebaseline, theorem-constant change, hidden analytic assumption, alternate proof route, or fake proof closure appears.
5. 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 cycle39ForwardKlDerivativeUpperPacket : ForwardKlUpperPacket where
  objective := "Proof-closure priority check before lower assignment: (1) lem:gronwall has cycle 36 local assembly progress but remains an obligation, (2) lem:dv_variation has one-sided scalar consequences while the Boucheron equality remains source-cited, (3) eq:LSI-KL-FI has cycle 38 finite-coordinate Fisher-chain progress but the vector/integral density-test backend remains an obligation, so this cycle follows the requested item (4): close theorem-specific continuous forward-KL Fokker-Planck/KL derivative lemmas for appendix.tex:168-228 before any more ledger work or the item (5) EM interpolation Fokker-Planck 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 proof route fixed: KL differentiation, SALD Fokker-Planck first term, slowed-target transport, Cauchy--Schwarz/Young, LSI, inverse-schedule time change, DV, then Gronwall.",
    "Use SALD.forwardKlPreDvDerivativeBoundScalar only as a composition of supplied scalar/analytic inputs; it does not prove the Fokker-Planck, integration-by-parts, LSI density-test, or inverse-schedule backends.",
    "Keep Gronwall, DV, LSI/KL/FI, the full KL derivative theorem, and EM interpolation below formalized status unless a compiled local proof for exactly that interface is added."
  ]
  nonGoals := [
    "Do not rebaseline the source index or expand transcript ledgers unless a reviewer finds a blocking source-anchor defect.",
    "Do not restate, weaken, or prove thm:forward-KL in this packet.",
    "Do not add smoothness, density, positivity, absolute-continuity, endpoint, boundary, LSI, inverse-function, finite-log-mgf, or interval-integrability assumptions to the theorem statement.",
    "Do not replace the paper route with Girsanov, path-space comparison, the general moving-target theorem, or a PI-based route.",
    "Do not start the Euler--Maruyama interpolation Fokker-Planck backend in this lower packet."
  ]
  lowerPacket := [
    "First lower target: prove or verify a theorem-specific scalar composition around SALD.forwardKlPreDvDerivativeBoundScalar, with all analytic premises explicit and no theorem-status promotion.",
    "Second lower target only after the scalar composition is stable: refine SALD.forwardKlDensityBoundaryObligation / sald.forward_kl.density_boundary_regular for appendix.tex:168-185, exposing mass conservation, KL differentiation under the integral, the SALD Fokker-Planck equation, boundary/no-flux or decay, and FI identification.",
    "Third lower target if the first two are stable: refine SALD.forwardKlScheduleTimeChangeObligation / sald.forward_kl.schedule_time_change for appendix.tex:191-228, including the chain rule, velocity-square scaling, inverse derivative, and dot{s}(t) positivity/nonzero inputs used by SALD.forwardKlTimeChangedDerivativeBoundScalar.",
    "Middle must keep AutoSamplingTheory/SALD.lean, conversion-windows/ASTIS-SALD-001.md, and proof-obligations/ASTIS-SALD-001.md synchronized against the same appendix.tex:168-228 source window.",
    "Leave DV finite-log-mgf, coefficient-chain audit, Gronwall side conditions, endpoint rewrites, and EM interpolation work as sibling obligations."
  ]
  reviewerChecklist := [
    "SALD.forwardKlPreDvDerivativeBoundScalar compiles and is only scalar Real/order composition from explicit KL derivative, first-term, Cauchy, LSI, chain-rule, velocity-scaling, and inverse-schedule premises.",
    "SALD.cycle39ForwardKlDerivativeUpperPacket and sald.forward_kl.cycle39_derivative_upper are listed in the forward-KL contract, proof DAG, and saldDependenciesForLabel \"thm:forward-KL\".",
    "sald.forward_kl.kl_derivative, sald.forward_kl.density_boundary_regular, sald.forward_kl.schedule_time_change, probability.lsi_to_kl_fi, lem:dv_variation, and lem:gronwall remain obligations or source-cited dependencies.",
    "No source-index rebaseline, theorem-constant change, hidden analytic assumption, alternate proof route, or fake proof closure appears.",
    "The mandatory ASTIS check passes."
  ]
  status := ProofStatus.obligation

/-- Cycle-39 middle map for the source-shaped derivative schedule handoff.

This translates the upper packet into proof-producing scalar targets for
`appendix.tex:191-228`: the inverse-schedule product identity, the
slowed-velocity square scaling, and the composed pre-DV derivative inequality.
It does not prove the analytic inverse-function theorem, L2 velocity scaling,
KL chain rule, Fokker--Planck equation, or LSI density-test backend.
-/