AutoSamplingTheory.SALD.cycle101DiscreteForwardKlClosurePressureMiddleObligation

Data definition / provenance and workflow record

Meaning and type

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

def cycle101DiscreteForwardKlClosurePressureMiddleObligation :
    ProofObligation

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.

id : String (explicit)

Stable obligation identifier.

sald.discrete_forward_kl.cycle101_closure_pressure_middle

statement : String (explicit)

Desired mathematical or workflow content as String; it is not a proposition in Prop and the def does not prove it.

Cycle 101 middle pressure-tests thm:forward-KL-discrete through the currently compiled EM wrappers and existing LSI/DV/Gronwall/accumulated-error interfaces. Classification: narrows-source-cited-boundary. No new theorem-route wrapper is needed: cycles 89 and 95 already carry the theorem route, and cycle 100 compiles the weakGrad law-integral definition alignment plus the Cauchy-Schwarz inner-gradient contraction. The exact next non-wrapper blocker is ASTIS.SALD.cycle100.remaining_no_boundary_after_inner_gradient, equivalently the hgradNormBound and hdivNoBoundary premises of SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientBound. The source anchor is appendix.tex lines 1379-1387, with barB supplied by appendix.tex lines 1368-1377. Lower should prove hdivNoBoundary from a precise no-boundary divergence theorem for hatRhoS * barB, or strictly narrow it to one Mathlib/local theorem with imports and hypotheses, while carrying hgradNormBound explicitly.

source : AutoSamplingTheory.SourceAnchor (explicit)

SourceAnchor supporting the intended requirement.

AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteWeakFpDriftActionMathlibSource — audited data reference, not expanded and not a compiled dependency edge

status : AutoSamplingTheory.ProofStatus (explicit)

Stored ProofStatus, default obligation; even an explicitly stored formalized does not independently certify a Lean theorem.

AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

dependsOn : List String (explicit)

List of declared dependency names as strings; may mix theorem names, obligations, source labels, or descriptions. Not the compiled dependency DAG.

Ordered data items

1. SALD.cycle95DiscreteForwardKlClosurePressureMiddleObligation
2. SALD.cycle100GeneralMovingTargetDiscreteBarBWeakGradDefLowerObligation
3. SALD.cycle100GeneralMovingTargetDiscreteBarBInnerGradientBoundLowerObligation
4. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientBound
5. ASTIS.SALD.cycle100.remaining_no_boundary_after_inner_gradient
6. sald.general_moving_target_discrete.em_interpolation_fp
7. sald.discrete_forward_kl.em_interpolation_fp
8. sald.discrete_forward_kl.kl_derivative
9. probability.lsi_to_kl_fi
10. lem:dv_variation
11. lem:gronwall
12. Mathlib.MeasureTheory.Integral.DivergenceTheorem
13. Mathlib.Analysis.InnerProductSpace.Basic
14. Mathlib.MeasureTheory.Integral.Bochner.Basic
15. main_body.tex:301-323
16. appendix.tex:260-592
17. appendix.tex:1379-1387
18. appendix.tex:1368-1377

note : String (explicit)

Recorded evidence/caveats; may distinguish a compiled scalar helper from still-open source analysis.

Middle pressure-test synchronization only. It identifies the next exact non-wrapper blocker after the compiled EM wrappers, LSI/DV/Gronwall interfaces, and cycle-100 handoffs; it does not prove weak FP, KL differentiation, no-boundary IBP, the weak-test gradient estimate, theorem closure, SLT import, or any Lake dependency.

def cycle101DiscreteForwardKlClosurePressureMiddleObligation :
    ProofObligation where
  id := "sald.discrete_forward_kl.cycle101_closure_pressure_middle"
  statement := "Cycle 101 middle pressure-tests thm:forward-KL-discrete through the currently compiled EM wrappers and existing LSI/DV/Gronwall/accumulated-error interfaces. Classification: narrows-source-cited-boundary. No new theorem-route wrapper is needed: cycles 89 and 95 already carry the theorem route, and cycle 100 compiles the weakGrad law-integral definition alignment plus the Cauchy-Schwarz inner-gradient contraction. The exact next non-wrapper blocker is ASTIS.SALD.cycle100.remaining_no_boundary_after_inner_gradient, equivalently the hgradNormBound and hdivNoBoundary premises of SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientBound. The source anchor is appendix.tex lines 1379-1387, with barB supplied by appendix.tex lines 1368-1377. Lower should prove hdivNoBoundary from a precise no-boundary divergence theorem for hatRhoS * barB, or strictly narrow it to one Mathlib/local theorem with imports and hypotheses, while carrying hgradNormBound explicitly."
  source := saldGeneralMovingTargetDiscreteWeakFpDriftActionMathlibSource
  status := ProofStatus.obligation
  dependsOn := [
    "SALD.cycle95DiscreteForwardKlClosurePressureMiddleObligation",
    "SALD.cycle100GeneralMovingTargetDiscreteBarBWeakGradDefLowerObligation",
    "SALD.cycle100GeneralMovingTargetDiscreteBarBInnerGradientBoundLowerObligation",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientBound",
    "ASTIS.SALD.cycle100.remaining_no_boundary_after_inner_gradient",
    "sald.general_moving_target_discrete.em_interpolation_fp",
    "sald.discrete_forward_kl.em_interpolation_fp",
    "sald.discrete_forward_kl.kl_derivative",
    "probability.lsi_to_kl_fi",
    "lem:dv_variation",
    "lem:gronwall",
    "Mathlib.MeasureTheory.Integral.DivergenceTheorem",
    "Mathlib.Analysis.InnerProductSpace.Basic",
    "Mathlib.MeasureTheory.Integral.Bochner.Basic",
    "main_body.tex:301-323",
    "appendix.tex:260-592",
    "appendix.tex:1379-1387",
    "appendix.tex:1368-1377"
  ]
  note := "Middle pressure-test synchronization only. It identifies the next exact non-wrapper blocker after the compiled EM wrappers, LSI/DV/Gronwall interfaces, and cycle-100 handoffs; it does not prove weak FP, KL differentiation, no-boundary IBP, the weak-test gradient estimate, theorem closure, SLT import, or any Lake dependency."

/-- Cycle-101 lower product-rule handoff for the no-boundary `barB` drift
boundary. -/