AutoSamplingTheory.SALD.cycle102DiscreteForwardKlZeroFluxTraceBoundaryDag

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 cycle102DiscreteForwardKlZeroFluxTraceBoundaryDag :
    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.cycle102_zero_flux_trace_boundary
interface : String (explicit)
Text describing intended mathematical interface.
Compiled local handoff: replace hzeroBoundary by a concrete boundary-flux integral boundaryFlux phi = int_y testTrace phi y * normalFluxTrace y d boundaryMeasure plus the source-cited a.e. trace-product zero condition. This targets the no-boundary part of appendix.tex:1379-1387 after the cycle-101 product-rule handoff.
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.cycle102DiscreteForwardKlZeroFluxTraceBoundaryMiddleObligation
2. SALD.generalMovingTargetDiscreteZeroBoundaryFluxOfTraceProductZero
3. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientTraceBoundary
4. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientProductRuleBoundary
5. MeasureTheory.integral_congr_ae
6. appendix.tex:1379-1387
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. cycle 102 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.cycle102_test_trace_zero_lower
interface : String (explicit)
Text describing intended mathematical interface.
Compiled local lower handoff: discharge htraceProductZero from the smaller condition testTrace phi = 0 boundaryMeasure-a.e. for admissible tests. This captures the compact-support/zero-boundary-trace route while leaving the actual trace theorem and boundary-flux integral representation explicit.
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.cycle102DiscreteForwardKlTraceZeroLowerObligation
2. SALD.generalMovingTargetDiscreteTraceProductZeroOfTestTraceZero
3. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientTraceBoundaryOfTestTraceZero
4. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientTraceBoundary
5. appendix.tex:1379-1387
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. sald.general_moving_target_discrete.em_interpolation_fp
2. sald.discrete_forward_kl.em_interpolation_fp
3. 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.cycle102_next_trace_boundary_blocker
interface : String (explicit)
Text describing intended mathematical interface.
Next exact boundary: prove the boundary-flux integral representation for hatRhoS * barB from the Mathlib divergence theorem/trace setup, and prove zero boundary trace a.e. for admissible tests from compact support or decay. Keep hproductRule, hdivergenceTheorem, and hgradNormBound explicit.
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.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientTraceBoundaryOfTestTraceZero
2. SALD.generalMovingTargetDiscreteTraceProductZeroOfTestTraceZero
3. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientTraceBoundary
4. SALD.generalMovingTargetDiscreteZeroBoundaryFluxOfTraceProductZero
5. Mathlib.MeasureTheory.Integral.DivergenceTheorem
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 102 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 cycle102DiscreteForwardKlZeroFluxTraceBoundaryDag :
    List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.forward_KL_discrete.cycle102_zero_flux_trace_boundary"
      interface := "Compiled local handoff: replace hzeroBoundary by a concrete boundary-flux integral boundaryFlux phi = int_y testTrace phi y * normalFluxTrace y d boundaryMeasure plus the source-cited a.e. trace-product zero condition. This targets the no-boundary part of appendix.tex:1379-1387 after the cycle-101 product-rule handoff."
      source := saldGeneralMovingTargetDiscreteWeakFpDriftActionMathlibSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle102DiscreteForwardKlZeroFluxTraceBoundaryMiddleObligation",
        "SALD.generalMovingTargetDiscreteZeroBoundaryFluxOfTraceProductZero",
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientTraceBoundary",
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientProductRuleBoundary",
        "MeasureTheory.integral_congr_ae",
        "appendix.tex:1379-1387"
      ]
      reusedBy := [
        "cycle 102 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.cycle102_test_trace_zero_lower"
      interface := "Compiled local lower handoff: discharge htraceProductZero from the smaller condition testTrace phi = 0 boundaryMeasure-a.e. for admissible tests. This captures the compact-support/zero-boundary-trace route while leaving the actual trace theorem and boundary-flux integral representation explicit."
      source := saldGeneralMovingTargetDiscreteWeakFpDriftActionMathlibSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle102DiscreteForwardKlTraceZeroLowerObligation",
        "SALD.generalMovingTargetDiscreteTraceProductZeroOfTestTraceZero",
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientTraceBoundaryOfTestTraceZero",
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientTraceBoundary",
        "appendix.tex:1379-1387"
      ]
      reusedBy := [
        "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.cycle102_next_trace_boundary_blocker"
      interface := "Next exact boundary: prove the boundary-flux integral representation for hatRhoS * barB from the Mathlib divergence theorem/trace setup, and prove zero boundary trace a.e. for admissible tests from compact support or decay. Keep hproductRule, hdivergenceTheorem, and hgradNormBound explicit."
      source := saldGeneralMovingTargetDiscreteWeakFpDriftActionMathlibSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientTraceBoundaryOfTestTraceZero",
        "SALD.generalMovingTargetDiscreteTraceProductZeroOfTestTraceZero",
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBInnerGradientTraceBoundary",
        "SALD.generalMovingTargetDiscreteZeroBoundaryFluxOfTraceProductZero",
        "Mathlib.MeasureTheory.Integral.DivergenceTheorem",
        "Mathlib.MeasureTheory.Integral.Bochner.Basic",
        "appendix.tex:1379-1387",
        "appendix.tex:1368-1377"
      ]
      reusedBy := [
        "cycle 102 lower packet",
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.discrete_forward_kl.em_interpolation_fp"
      ]
      status := ProofStatus.obligation
    }
  ]

/-! ### Cycle 103: conditional-kernel component-version boundary -/

/-- Cycle-103 middle obligation for the `condC` conditional-kernel
component-version theorem.

This returns to the conditional drift definition at `appendix.tex:1368-1377`
and narrows the cycle-91 remaining boundary to one selected component.  The
packet deliberately does not add a theorem wrapper around `hguideComp`; it
records the exact Mathlib/local theorem still missing behind that sample-space
a.e. equality.
-/

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