AutoSamplingTheory.SALD.cycle101DiscreteForwardKlClosurePressureDag

Data definition / provenance and workflow record

Meaning and type

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

Lean statement of this data definition

The part after the colon is the output data type. This declaration takes no mathematical proof inputs.

def cycle101DiscreteForwardKlClosurePressureDag : List ProofDagBlock

Construction and field-by-field explanation

Construct an ordered list of the following data items. It is not a logical conjunction or proof DAG.

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.

Ordered data items

id : String (explicit)
Stable plan-node identifier.
ASTIS.SALD.forward_KL_discrete.cycle101_middle_pressure_sync
interface : String (explicit)
Text describing intended mathematical interface.
Pressure-test synchronization: thm:forward-KL-discrete routes through the compiled EM/KL scalar handoffs, LSI, DV, Gronwall, accumulated-error interfaces, and the cycle-100 weakGrad/inner-gradient handoffs. The route now stops at the no-boundary divergence theorem for hatRhoS * barB, with hgradNormBound carried as the smaller companion weak-test gradient estimate.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteWeakFpDriftActionMathlibSource — audited data reference, not expanded and not a compiled dependency edge
targetLean : String (explicit)
Textual planned implementation destination.
AutoSamplingTheory/SALD.lean
dependsOn : List String (explicit)
Declared input names as strings, default empty.
Ordered data items
1. SALD.cycle101DiscreteForwardKlClosurePressureMiddleObligation
2. SALD.cycle95DiscreteForwardKlClosurePressureMiddleObligation
3. SALD.cycle100GeneralMovingTargetDiscreteBarBInnerGradientBoundLowerObligation
4. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientBound
5. ASTIS.SALD.cycle100.remaining_no_boundary_after_inner_gradient
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. thm:forward-KL-discrete
2. sald.discrete_forward_kl.em_interpolation_fp
3. sald.general_moving_target_discrete.em_interpolation_fp
status : AutoSamplingTheory.ProofStatus (explicit)
Recorded workflow status, default planned.
AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
id : String (explicit)
Stable plan-node identifier.
ASTIS.SALD.forward_KL_discrete.cycle101_lower_product_rule_handoff
interface : String (explicit)
Text describing intended mathematical interface.
Compiled local handoff: replace the single hdivNoBoundary input by product-rule total divergence, the Mathlib divergence-theorem boundary-flux identity, and zero boundary flux for hatRhoS * barB. The remaining lower theorem is the Euclidean weighted-field product rule plus no-boundary flux hypotheses at appendix.tex:1379-1387; hgradNormBound is still carried separately.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteWeakFpDriftActionMathlibSource — audited data reference, not expanded and not a compiled dependency edge
targetLean : String (explicit)
Textual planned implementation destination.
AutoSamplingTheory/SALD.lean
dependsOn : List String (explicit)
Declared input names as strings, default empty.
Ordered data items
1. SALD.cycle101DiscreteForwardKlNoBoundaryProductRuleLowerObligation
2. SALD.generalMovingTargetDiscreteDriftDivNoBoundaryOfProductRule
3. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientProductRuleBoundary
4. MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable
5. Mathlib.MeasureTheory.Integral.DivergenceTheorem
6. appendix.tex:1379-1387
7. appendix.tex:1368-1377
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. cycle 101 lower packet
2. sald.general_moving_target_discrete.em_interpolation_fp
3. sald.discrete_forward_kl.em_interpolation_fp
4. thm:forward-KL-discrete
status : AutoSamplingTheory.ProofStatus (explicit)
Recorded workflow status, default planned.
AutoSamplingTheory.ProofStatus.formalized — stored label only; no proof certification
id : String (explicit)
Stable plan-node identifier.
ASTIS.SALD.forward_KL_discrete.cycle101_next_non_wrapper_blocker
interface : String (explicit)
Text describing intended mathematical interface.
Next lower packet after the product-rule handoff: prove the Euclidean weighted-field product rule for div(hatRhoS * barB * phi), instantiate the Mathlib divergence theorem to the resulting boundary-flux identity, and discharge zero boundary flux for admissible tests at appendix.tex:1379-1387. The hgradNormBound weak-test gradient estimate remains explicit. A wrapper that merely restates hdivNoBoundary or hgradNormBound is rejected-wrapper-churn.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteWeakFpDriftActionMathlibSource — audited data reference, not expanded and not a compiled dependency edge
targetLean : String (explicit)
Textual planned implementation destination.
AutoSamplingTheory/SALD.lean
dependsOn : List String (explicit)
Declared input names as strings, default empty.
Ordered data items
1. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientProductRuleBoundary
2. ASTIS.SALD.cycle100.remaining_no_boundary_after_inner_gradient
3. ASTIS.SALD.forward_KL_discrete.cycle101_lower_product_rule_handoff
4. Mathlib.MeasureTheory.Integral.DivergenceTheorem
5. Mathlib.Analysis.InnerProductSpace.Basic
6. Mathlib.MeasureTheory.Integral.Bochner.Basic
7. appendix.tex:1379-1387
8. appendix.tex:1368-1377
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. cycle 101 lower packet
2. sald.general_moving_target_discrete.em_interpolation_fp
3. sald.discrete_forward_kl.em_interpolation_fp
status : AutoSamplingTheory.ProofStatus (explicit)
Recorded workflow status, default planned.
AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

Exact Lean data construction

Each field assignment stores the corresponding value shown above. Omitted fields use the explicitly identified schema defaults. Strings that name theorems remain strings; they do not call those theorems.

def cycle101DiscreteForwardKlClosurePressureDag : List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.forward_KL_discrete.cycle101_middle_pressure_sync"
      interface := "Pressure-test synchronization: thm:forward-KL-discrete routes through the compiled EM/KL scalar handoffs, LSI, DV, Gronwall, accumulated-error interfaces, and the cycle-100 weakGrad/inner-gradient handoffs. The route now stops at the no-boundary divergence theorem for hatRhoS * barB, with hgradNormBound carried as the smaller companion weak-test gradient estimate."
      source := saldGeneralMovingTargetDiscreteWeakFpDriftActionMathlibSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle101DiscreteForwardKlClosurePressureMiddleObligation",
        "SALD.cycle95DiscreteForwardKlClosurePressureMiddleObligation",
        "SALD.cycle100GeneralMovingTargetDiscreteBarBInnerGradientBoundLowerObligation",
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientBound",
        "ASTIS.SALD.cycle100.remaining_no_boundary_after_inner_gradient"
      ]
      reusedBy := [
        "thm:forward-KL-discrete",
        "sald.discrete_forward_kl.em_interpolation_fp",
        "sald.general_moving_target_discrete.em_interpolation_fp"
      ]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL_discrete.cycle101_lower_product_rule_handoff"
      interface := "Compiled local handoff: replace the single hdivNoBoundary input by product-rule total divergence, the Mathlib divergence-theorem boundary-flux identity, and zero boundary flux for hatRhoS * barB. The remaining lower theorem is the Euclidean weighted-field product rule plus no-boundary flux hypotheses at appendix.tex:1379-1387; hgradNormBound is still carried separately."
      source := saldGeneralMovingTargetDiscreteWeakFpDriftActionMathlibSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle101DiscreteForwardKlNoBoundaryProductRuleLowerObligation",
        "SALD.generalMovingTargetDiscreteDriftDivNoBoundaryOfProductRule",
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientProductRuleBoundary",
        "MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable",
        "Mathlib.MeasureTheory.Integral.DivergenceTheorem",
        "appendix.tex:1379-1387",
        "appendix.tex:1368-1377"
      ]
      reusedBy := [
        "cycle 101 lower packet",
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.discrete_forward_kl.em_interpolation_fp",
        "thm:forward-KL-discrete"
      ]
      status := ProofStatus.formalized
    },
    {
      id := "ASTIS.SALD.forward_KL_discrete.cycle101_next_non_wrapper_blocker"
      interface := "Next lower packet after the product-rule handoff: prove the Euclidean weighted-field product rule for div(hatRhoS * barB * phi), instantiate the Mathlib divergence theorem to the resulting boundary-flux identity, and discharge zero boundary flux for admissible tests at appendix.tex:1379-1387. The hgradNormBound weak-test gradient estimate remains explicit. A wrapper that merely restates hdivNoBoundary or hgradNormBound is rejected-wrapper-churn."
      source := saldGeneralMovingTargetDiscreteWeakFpDriftActionMathlibSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientProductRuleBoundary",
        "ASTIS.SALD.cycle100.remaining_no_boundary_after_inner_gradient",
        "ASTIS.SALD.forward_KL_discrete.cycle101_lower_product_rule_handoff",
        "Mathlib.MeasureTheory.Integral.DivergenceTheorem",
        "Mathlib.Analysis.InnerProductSpace.Basic",
        "Mathlib.MeasureTheory.Integral.Bochner.Basic",
        "appendix.tex:1379-1387",
        "appendix.tex:1368-1377"
      ]
      reusedBy := [
        "cycle 101 lower packet",
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.discrete_forward_kl.em_interpolation_fp"
      ]
      status := ProofStatus.obligation
    }
  ]

/-! ### Cycle 102: zero boundary flux narrowed to trace product -/

/-- Cycle-102 middle/lower-ready handoff for the remaining zero-boundary-flux
piece of the `hatRhoS * barB` no-boundary theorem.

The cycle stays on the active EM backend and does not open the non-EM
LSI/DV/Gronwall fallback.  It narrows the cycle-101 raw
`hzeroBoundary : boundaryFlux phi = 0` input to a boundary-integral
representation plus an a.e. zero trace-product condition.
-/

Existing module entry · Audited data-reader index · All teaching coverage