AutoSamplingTheory.SALD.cycle36GronwallUpperPacket

Data definition / provenance and workflow record

Meaning and type

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

def cycle36GronwallUpperPacket : FirstAppendixVocabularyPacket

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 assigning lower work: (1) lem:gronwall remains open after cycle 31 local derivative, order-integration, endpoint, and exponent sublemmas; (2) lem:dv_variation remains source-cited with cycle 32 scalar consequences; (3) eq:LSI-KL-FI remains open after cycle 33 density-test scalar lemmas; (4) the forward-KL Fokker-Planck/KL derivative identity still depends on analytic backends after cycle 34 scalar handoffs; and (5) the EM interpolation Fokker-Planck backend has cycle 35 endpoint/divergence algebra only. Cycle 36 therefore returns to item (1): translate appendix.tex:47-71 into a proof-producing Gronwall assembly target.

sourceLabels : List String (explicit)

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

Ordered data items

1. lem:gronwall
2. lem:dv_variation
3. eq:LSI-KL-FI
4. thm:forward-KL
5. thm:forward-KL-discrete

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper Phase 1: use only the original appendix.tex:47-71 Gronwall lemma and proof; sald_version_2.tex remains excluded.
2. Keep the source theorem fixed: continuous a_t and b_t, differentiable K_t on [0,t1], differential inequality dK/dt <= -a_t*K_t+b_t, and the exact final bound with exp(-int_0^t1 a) and exp(-int_t^t1 a).
3. Use the existing compiled local helpers as dependencies, not as permission to change the lemma statement or import an alternate Gronwall theorem.
4. If the closed-interval derivative/FTC backend is too large for the current local Mathlib state, expose a precise source-cited or Mathlib-backed theorem interface and keep lem:gronwall below formalized status.

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 unless a reviewer identifies a blocking source-anchor defect.
2. Do not work on DV, LSI/KL/FI, forward-KL derivative, EM interpolation, PI velocity-norm, guided, general VA-SALD, unified, or accumulated-error proof search in this upper packet.
3. Do not add sign assumptions on a or b, monotonicity assumptions, extra endpoint hypotheses, or theorem-level smoothness assumptions beyond an explicit calculus interface.
4. Do not mark SALD.gronwallContract, sald.gronwall.integrating_factor, sald.gronwall.endpoint_calculus, or sald.gronwall.exponent_rewrite formalized until a compiled Lean theorem closes the full source display.

lowerPacket : List String (explicit)

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

Ordered data items

1. Middle must keep two-way Lean/Markdown/LaTeX synchronization for appendix.tex:47-71, AutoSamplingTheory/SALD.lean, conversion-windows/ASTIS-SALD-001.md, and proof-obligations/ASTIS-SALD-001.md.
2. Target exactly SALD.saldGronwallCandidateContract, SALD.saldGronwallEndpointCalculusContract, SALD.saldGronwallExponentRewriteContract, and the obligations sald.gronwall.integrating_factor, sald.gronwall.endpoint_calculus, sald.gronwall.exponent_rewrite.
3. First proof-producing lower attempt: assemble a theorem-level Gronwall display under explicit global interval hypotheses by using SALD.gronwallIntegratingFactorDerivativeLeOfIntegral, SALD.gronwallOrderIntegrationOfHasDerivAt, SALD.gronwallEndpointEvaluationScalar, SALD.gronwallEndpointMultiplyByExpNegScalar, and SALD.gronwallExpProductRewriteIntegralCongr.
4. If endpoint-safe differentiability on [0,t1] is blocked, introduce one narrow interface for the closed-interval or absolute-continuity FTC step, with hypotheses naming the required interval-integrability of f', g, a, and b; leave that interface as obligation/source-cited rather than changing the source lemma.
5. Keep downstream theorem-specific Gronwall side conditions for forward-KL, discrete forward-KL, and general moving-target SALD as separate sibling obligations.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.gronwallContract still has ProofStatus.obligation and lists the cycle 36 upper obligation only as workflow data.
2. SALD.saldDependenciesForLabel "lem:gronwall" includes SALD.cycle36GronwallUpperPacket and sald.gronwall.cycle36_upper_packet while retaining the cycle 31 compiled helper declarations.
3. The conversion window and proof-obligation ledger identify cycle 36 as Gronwall proof-closure item (1), not source-index rebaseline or theorem-status promotion.
4. No alternate Gronwall theorem, hidden sign assumption, source-file drift, or fake proof closure is introduced.
5. The mandatory gate python3 tools/astis.py 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 cycle36GronwallUpperPacket : FirstAppendixVocabularyPacket where
  objective := "Proof-closure priority check before assigning lower work: (1) lem:gronwall remains open after cycle 31 local derivative, order-integration, endpoint, and exponent sublemmas; (2) lem:dv_variation remains source-cited with cycle 32 scalar consequences; (3) eq:LSI-KL-FI remains open after cycle 33 density-test scalar lemmas; (4) the forward-KL Fokker-Planck/KL derivative identity still depends on analytic backends after cycle 34 scalar handoffs; and (5) the EM interpolation Fokker-Planck backend has cycle 35 endpoint/divergence algebra only. Cycle 36 therefore returns to item (1): translate appendix.tex:47-71 into a proof-producing Gronwall assembly target."
  sourceLabels := [
    "lem:gronwall",
    "lem:dv_variation",
    "eq:LSI-KL-FI",
    "thm:forward-KL",
    "thm:forward-KL-discrete"
  ]
  modeDiscipline := [
    "faithfulPaper Phase 1: use only the original appendix.tex:47-71 Gronwall lemma and proof; sald_version_2.tex remains excluded.",
    "Keep the source theorem fixed: continuous a_t and b_t, differentiable K_t on [0,t1], differential inequality dK/dt <= -a_t*K_t+b_t, and the exact final bound with exp(-int_0^t1 a) and exp(-int_t^t1 a).",
    "Use the existing compiled local helpers as dependencies, not as permission to change the lemma statement or import an alternate Gronwall theorem.",
    "If the closed-interval derivative/FTC backend is too large for the current local Mathlib state, expose a precise source-cited or Mathlib-backed theorem interface and keep lem:gronwall below formalized status."
  ]
  nonGoals := [
    "Do not rebaseline the source index unless a reviewer identifies a blocking source-anchor defect.",
    "Do not work on DV, LSI/KL/FI, forward-KL derivative, EM interpolation, PI velocity-norm, guided, general VA-SALD, unified, or accumulated-error proof search in this upper packet.",
    "Do not add sign assumptions on a or b, monotonicity assumptions, extra endpoint hypotheses, or theorem-level smoothness assumptions beyond an explicit calculus interface.",
    "Do not mark SALD.gronwallContract, sald.gronwall.integrating_factor, sald.gronwall.endpoint_calculus, or sald.gronwall.exponent_rewrite formalized until a compiled Lean theorem closes the full source display."
  ]
  lowerPacket := [
    "Middle must keep two-way Lean/Markdown/LaTeX synchronization for appendix.tex:47-71, AutoSamplingTheory/SALD.lean, conversion-windows/ASTIS-SALD-001.md, and proof-obligations/ASTIS-SALD-001.md.",
    "Target exactly SALD.saldGronwallCandidateContract, SALD.saldGronwallEndpointCalculusContract, SALD.saldGronwallExponentRewriteContract, and the obligations sald.gronwall.integrating_factor, sald.gronwall.endpoint_calculus, sald.gronwall.exponent_rewrite.",
    "First proof-producing lower attempt: assemble a theorem-level Gronwall display under explicit global interval hypotheses by using SALD.gronwallIntegratingFactorDerivativeLeOfIntegral, SALD.gronwallOrderIntegrationOfHasDerivAt, SALD.gronwallEndpointEvaluationScalar, SALD.gronwallEndpointMultiplyByExpNegScalar, and SALD.gronwallExpProductRewriteIntegralCongr.",
    "If endpoint-safe differentiability on [0,t1] is blocked, introduce one narrow interface for the closed-interval or absolute-continuity FTC step, with hypotheses naming the required interval-integrability of f', g, a, and b; leave that interface as obligation/source-cited rather than changing the source lemma.",
    "Keep downstream theorem-specific Gronwall side conditions for forward-KL, discrete forward-KL, and general moving-target SALD as separate sibling obligations."
  ]
  reviewerChecklist := [
    "SALD.gronwallContract still has ProofStatus.obligation and lists the cycle 36 upper obligation only as workflow data.",
    "SALD.saldDependenciesForLabel \"lem:gronwall\" includes SALD.cycle36GronwallUpperPacket and sald.gronwall.cycle36_upper_packet while retaining the cycle 31 compiled helper declarations.",
    "The conversion window and proof-obligation ledger identify cycle 36 as Gronwall proof-closure item (1), not source-index rebaseline or theorem-status promotion.",
    "No alternate Gronwall theorem, hidden sign assumption, source-file drift, or fake proof closure is introduced.",
    "The mandatory gate python3 tools/astis.py check passes."
  ]
  status := ProofStatus.obligation

/-- Cycle-36 upper workflow obligation for the Gronwall proof-closure packet. -/