AutoSamplingTheory.SALD.cycle38LsiKlFiUpperPacket

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 cycle38LsiKlFiUpperPacket : 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 was advanced in cycle 36 but remains an obligation pending endpoint-safe differentiability/derivative witnesses; (2) lem:dv_variation was advanced in cycle 37 by a Mathlib-backed one-sided tilted-measure backend while the Boucheron supremum equality remains sourceCited; (3) cycle 38 therefore selects eq:LSI-KL-FI; (4) the forward-KL Fokker-Planck/KL derivative identity and (5) the EM interpolation Fokker-Planck backend remain later closure targets.

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 main_body.tex:202-215 LSI, KL, and FI bridge; sald_version_2.tex remains excluded.
2. Keep the paper statement fixed: pi satisfies LSI with constant C_LSI > 0, rho << pi, phi=sqrt(rho/pi), and the final comparison is KL(rho||pi) <= FI(rho||pi)/(2*C_LSI).
3. Use the cycle 29 and cycle 33 compiled scalar helpers only after the source density-test inputs are supplied; they do not prove Radon-Nikodym construction, smooth/admissible sqrt tests, entropy integrability, or the Fisher-information chain rule.
4. If the Sobolev or measure-theoretic chain rule is too large for the local Mathlib state, create a precise source-cited theorem interface with explicit density, positivity/zero-set, differentiability or approximation, and finite KL/FI hypotheses, and keep its status below formalized.

nonGoals : List String (explicit)

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

Ordered data items

1. Do not run a source-index rebaseline unless a reviewer identifies a blocking source-anchor defect.
2. Do not reopen Gronwall, Donsker--Varadhan, 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 replace the source LSI route with PI, Pinsker, Talagrand, transport, or theorem-level forward-KL reasoning.
4. Do not add hidden smoothness, positivity, finite-KL, finite-FI, boundedness, or approximation assumptions to thm:forward-KL or any downstream theorem statement.
5. Do not mark probability.lsi_to_kl_fi, SALD.lsiKlFiDensityTestObligation, or SALD.saldStatusForLabel "eq:LSI-KL-FI" formalized.

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 main_body.tex:202-215, AutoSamplingTheory/Probability.lean, AutoSamplingTheory/SALD.lean, conversion-windows/ASTIS-SALD-001.md, and proof-obligations/ASTIS-SALD-001.md.
2. Target exactly SALD.saldLsiKlFiDensityTestContract, SALD.lsiKlFiDensityTestObligation, and sald.lsi_kl_fi.density_test_interface.
3. First lower attempt should be proof-producing: after the cycle 33 sqrt-density square, entropy-integrand, normalization, and normalized-test scalar bridge, prove one narrow pointwise or vector-norm handoff for the Fisher chain rule, or a theorem-independent scalar integral bridge that turns a supplied Dirichlet=(1/4)*FI identity into the existing SALD.lsiKlFiDensityTestBridgeScalar input.
4. If the full chain rule for sqrt(rho/pi) is blocked, introduce a precise source-cited or obligation interface naming the Radon-Nikodym density, positivity or zero-density convention, smooth/admissible sqrt test or approximation theorem, finite KL/FI requirements, and the identity integral ||nabla sqrt(r)||^2 d pi = (1/4)*FI(rho||pi).
5. Do not consume SALD.lsiKlFiCoefficientAuditScalar or SALD.lsiKlFiDensityTestBridgeScalar until the entropy-to-KL and Fisher-chain inputs are explicit assumptions, compiled lemmas, or source-cited interfaces.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. The cycle explicitly chooses proof-closure item (3), eq:LSI-KL-FI, after recording current Gronwall and DV statuses.
2. Any new Lean proof is tied to main_body.tex:202-215 and is only a density/test-function, entropy, Fisher-chain, or scalar coefficient sublemma; no downstream theorem receives hidden assumptions.
3. SALD.lsiKlFiVocabularyContract, SALD.lsiKlFiDensityTestObligation, probability.lsi_to_kl_fi, and SALD.saldStatusForLabel "eq:LSI-KL-FI" remain ProofStatus.obligation.
4. No axiom, sorry, admit, Prop := True, := trivial, source-file drift, SLT import, or alternate non-LSI proof route 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 cycle38LsiKlFiUpperPacket : FirstAppendixVocabularyPacket where
  objective := "Proof-closure priority check before assigning lower work: (1) lem:gronwall was advanced in cycle 36 but remains an obligation pending endpoint-safe differentiability/derivative witnesses; (2) lem:dv_variation was advanced in cycle 37 by a Mathlib-backed one-sided tilted-measure backend while the Boucheron supremum equality remains sourceCited; (3) cycle 38 therefore selects eq:LSI-KL-FI; (4) the forward-KL Fokker-Planck/KL derivative identity and (5) the EM interpolation Fokker-Planck backend remain later closure targets."
  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 main_body.tex:202-215 LSI, KL, and FI bridge; sald_version_2.tex remains excluded.",
    "Keep the paper statement fixed: pi satisfies LSI with constant C_LSI > 0, rho << pi, phi=sqrt(rho/pi), and the final comparison is KL(rho||pi) <= FI(rho||pi)/(2*C_LSI).",
    "Use the cycle 29 and cycle 33 compiled scalar helpers only after the source density-test inputs are supplied; they do not prove Radon-Nikodym construction, smooth/admissible sqrt tests, entropy integrability, or the Fisher-information chain rule.",
    "If the Sobolev or measure-theoretic chain rule is too large for the local Mathlib state, create a precise source-cited theorem interface with explicit density, positivity/zero-set, differentiability or approximation, and finite KL/FI hypotheses, and keep its status below formalized."
  ]
  nonGoals := [
    "Do not run a source-index rebaseline unless a reviewer identifies a blocking source-anchor defect.",
    "Do not reopen Gronwall, Donsker--Varadhan, forward-KL derivative, EM interpolation, PI velocity-norm, guided, general VA-SALD, unified, or accumulated-error proof search in this upper packet.",
    "Do not replace the source LSI route with PI, Pinsker, Talagrand, transport, or theorem-level forward-KL reasoning.",
    "Do not add hidden smoothness, positivity, finite-KL, finite-FI, boundedness, or approximation assumptions to thm:forward-KL or any downstream theorem statement.",
    "Do not mark probability.lsi_to_kl_fi, SALD.lsiKlFiDensityTestObligation, or SALD.saldStatusForLabel \"eq:LSI-KL-FI\" formalized."
  ]
  lowerPacket := [
    "Middle must keep two-way Lean/Markdown/LaTeX synchronization for main_body.tex:202-215, AutoSamplingTheory/Probability.lean, AutoSamplingTheory/SALD.lean, conversion-windows/ASTIS-SALD-001.md, and proof-obligations/ASTIS-SALD-001.md.",
    "Target exactly SALD.saldLsiKlFiDensityTestContract, SALD.lsiKlFiDensityTestObligation, and sald.lsi_kl_fi.density_test_interface.",
    "First lower attempt should be proof-producing: after the cycle 33 sqrt-density square, entropy-integrand, normalization, and normalized-test scalar bridge, prove one narrow pointwise or vector-norm handoff for the Fisher chain rule, or a theorem-independent scalar integral bridge that turns a supplied Dirichlet=(1/4)*FI identity into the existing SALD.lsiKlFiDensityTestBridgeScalar input.",
    "If the full chain rule for sqrt(rho/pi) is blocked, introduce a precise source-cited or obligation interface naming the Radon-Nikodym density, positivity or zero-density convention, smooth/admissible sqrt test or approximation theorem, finite KL/FI requirements, and the identity integral ||nabla sqrt(r)||^2 d pi = (1/4)*FI(rho||pi).",
    "Do not consume SALD.lsiKlFiCoefficientAuditScalar or SALD.lsiKlFiDensityTestBridgeScalar until the entropy-to-KL and Fisher-chain inputs are explicit assumptions, compiled lemmas, or source-cited interfaces."
  ]
  reviewerChecklist := [
    "The cycle explicitly chooses proof-closure item (3), eq:LSI-KL-FI, after recording current Gronwall and DV statuses.",
    "Any new Lean proof is tied to main_body.tex:202-215 and is only a density/test-function, entropy, Fisher-chain, or scalar coefficient sublemma; no downstream theorem receives hidden assumptions.",
    "SALD.lsiKlFiVocabularyContract, SALD.lsiKlFiDensityTestObligation, probability.lsi_to_kl_fi, and SALD.saldStatusForLabel \"eq:LSI-KL-FI\" remain ProofStatus.obligation.",
    "No axiom, sorry, admit, Prop := True, := trivial, source-file drift, SLT import, or alternate non-LSI proof route is introduced.",
    "The mandatory gate python3 tools/astis.py check passes."
  ]
  status := ProofStatus.obligation

/-- Cycle-38 upper workflow obligation for the LSI/KL/FI density-test bridge. -/