AutoSamplingTheory.SALD.cycle30ForwardKlUpperPacket

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

Return to continuous thm:forward-KL and select the derivative-side moving-target interface as the next faithful lower target: mass conservation, differentiation under the KL integral, SALD and target integration by parts, slowed-target transport, Young's inequality, and inverse-schedule time change before the existing LSI, DV, and Gronwall blocks are used.

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:168-228 from the original source root; sald_version_2.tex remains excluded.
2. Keep the theorem statement fixed: no new smoothness, absolute-continuity, endpoint, positivity, boundary, or integrability hypotheses are added to thm:forward-KL.
3. Preserve the source derivative route: differentiate KL(rho_s||tilde_pi_s), use eq:FP-eq for SALD, transport tilde_pi_s by tilde_v_s=dot{t}(s)*v_{t(s)}, apply Cauchy--Schwarz/Young, then use eq:LSI-KL-FI and the inverse-schedule identity to reach the pre-DV t-inequality.
4. Treat density regularity, boundary decay, differentiation-under-integral, inverse-function calculus, LSI-to-KL/FI, DV, and Gronwall 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 Girsanov, Pinsker, Talagrand, path-space comparison, the general moving-target theorem, or a PI-based route.
3. Do not reopen the cycle-26 DV finite-log-mgf witness or cycle-29 LSI density-test lower work except as dependencies of the derivative handoff.
4. Do not change the Young coefficient 1/2, the LSI coefficient C_LSI(t), the time-change coefficient (1/2)*dot{s}(t)^(-1), or the terminal display in main_body.tex:243-246.
5. Do not mark the KL derivative, Fokker--Planck backend, integration by parts, LSI-to-KL/FI, DV, Gronwall, or endpoint schedule identities formalized.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.forwardKlDerivativeSideConditionContract / SALD.forwardKlDensityBoundaryObligation / sald.forward_kl.density_boundary_regular as the first lower slice.
2. First sub-slice: appendix.tex:168-185, expose mass conservation, differentiation under the KL integral, the SALD Fokker--Planck equation, and the integration-by-parts conditions that identify the first derivative term as -FI(rho_s||tilde_pi_s).
3. Second sub-slice if the first is blocked: appendix.tex:187-208, expose common state-space/density assumptions, the slowed-target transport identity for tilde_v_s, target-side integration by parts, and Cauchy--Schwarz/Young with the exact 1/2 coefficients.
4. Leave appendix.tex:218-228 time-change identities in SALD.forwardKlScheduleTimeChangeObligation unless the lower attempt finishes the density/boundary slice and explicitly records the handoff.
5. Keep DV, final coefficient-chain audit, Gronwall side conditions, and theorem-level endpoint rewrites in their existing obligations.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.forwardKlProofDag contains a cycle-30 derivative-side block before ASTIS.SALD.forward_KL.derivative and before DV/Gronwall blocks.
2. SALD.saldDependenciesForLabel "thm:forward-KL" includes SALD.cycle30ForwardKlUpperPacket and sald.forward_kl.cycle30_derivative_side_upper while retaining cycle-14, cycle-18, cycle-22, and cycle-26 packets.
3. SALD.forwardKlDerivativeSideConditionContract still classifies mass conservation, differentiation-under-integral, SALD/target integration by parts, Young, and inverse-schedule time change as obligations, not theorem assumptions.
4. Conversion window, proof-obligation ledger, and SLT audit identify cycle 30 as derivative-side source-to-Lean routing, not a proof of thm:forward-KL.
5. SALD_original.jsonl indexes thm:forward-KL, eq:SALD, eq:FP-eq, eq:LSI-KL-FI, lem:dv_variation, and lem:gronwall from the original files while excluding sald_version_2.tex.
6. No fake proof closure appears and no analytic dependency is promoted beyond obligation or source-cited status.

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 cycle30ForwardKlUpperPacket : ForwardKlUpperPacket where
  objective := "Return to continuous thm:forward-KL and select the derivative-side moving-target interface as the next faithful lower target: mass conservation, differentiation under the KL integral, SALD and target integration by parts, slowed-target transport, Young's inequality, and inverse-schedule time change before the existing LSI, DV, and Gronwall blocks are used."
  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:168-228 from the original source root; sald_version_2.tex remains excluded.",
    "Keep the theorem statement fixed: no new smoothness, absolute-continuity, endpoint, positivity, boundary, or integrability hypotheses are added to thm:forward-KL.",
    "Preserve the source derivative route: differentiate KL(rho_s||tilde_pi_s), use eq:FP-eq for SALD, transport tilde_pi_s by tilde_v_s=dot{t}(s)*v_{t(s)}, apply Cauchy--Schwarz/Young, then use eq:LSI-KL-FI and the inverse-schedule identity to reach the pre-DV t-inequality.",
    "Treat density regularity, boundary decay, differentiation-under-integral, inverse-function calculus, LSI-to-KL/FI, DV, and Gronwall 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 Girsanov, Pinsker, Talagrand, path-space comparison, the general moving-target theorem, or a PI-based route.",
    "Do not reopen the cycle-26 DV finite-log-mgf witness or cycle-29 LSI density-test lower work except as dependencies of the derivative handoff.",
    "Do not change the Young coefficient 1/2, the LSI coefficient C_LSI(t), the time-change coefficient (1/2)*dot{s}(t)^(-1), or the terminal display in main_body.tex:243-246.",
    "Do not mark the KL derivative, Fokker--Planck backend, integration by parts, LSI-to-KL/FI, DV, Gronwall, or endpoint schedule identities formalized."
  ]
  lowerPacket := [
    "Target exactly SALD.forwardKlDerivativeSideConditionContract / SALD.forwardKlDensityBoundaryObligation / sald.forward_kl.density_boundary_regular as the first lower slice.",
    "First sub-slice: appendix.tex:168-185, expose mass conservation, differentiation under the KL integral, the SALD Fokker--Planck equation, and the integration-by-parts conditions that identify the first derivative term as -FI(rho_s||tilde_pi_s).",
    "Second sub-slice if the first is blocked: appendix.tex:187-208, expose common state-space/density assumptions, the slowed-target transport identity for tilde_v_s, target-side integration by parts, and Cauchy--Schwarz/Young with the exact 1/2 coefficients.",
    "Leave appendix.tex:218-228 time-change identities in SALD.forwardKlScheduleTimeChangeObligation unless the lower attempt finishes the density/boundary slice and explicitly records the handoff.",
    "Keep DV, final coefficient-chain audit, Gronwall side conditions, and theorem-level endpoint rewrites in their existing obligations."
  ]
  reviewerChecklist := [
    "SALD.forwardKlProofDag contains a cycle-30 derivative-side block before ASTIS.SALD.forward_KL.derivative and before DV/Gronwall blocks.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes SALD.cycle30ForwardKlUpperPacket and sald.forward_kl.cycle30_derivative_side_upper while retaining cycle-14, cycle-18, cycle-22, and cycle-26 packets.",
    "SALD.forwardKlDerivativeSideConditionContract still classifies mass conservation, differentiation-under-integral, SALD/target integration by parts, Young, and inverse-schedule time change as obligations, not theorem assumptions.",
    "Conversion window, proof-obligation ledger, and SLT audit identify cycle 30 as derivative-side source-to-Lean routing, not a proof of thm:forward-KL.",
    "SALD_original.jsonl indexes thm:forward-KL, eq:SALD, eq:FP-eq, eq:LSI-KL-FI, lem:dv_variation, and lem:gronwall from the original files while excluding sald_version_2.tex.",
    "No fake proof closure appears and no analytic dependency is promoted beyond obligation or source-cited status."
  ]
  status := ProofStatus.obligation

/-- Cycle-30 middle packet for the continuous forward-KL derivative side.

This translates the upper-selected derivative-side target into a lower-ready
source-to-Lean map.  The first lower slice is only `appendix.tex:168-185`:
mass conservation, KL differentiation, the SALD Fokker-Planck equation, and the
integration-by-parts identification of the first derivative term with `-FI`.
Target-side transport, LSI, inverse-schedule calculus, DV, and Gronwall remain
separate obligations.
-/