AutoSamplingTheory.SALD.cycle95DiscreteForwardKlClosurePressureDag

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 cycle95DiscreteForwardKlClosurePressureDag : 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.cycle95.global_phase_judgment
interface : String (explicit)
Text describing intended mathematical interface.
Cycle 95 judgment: cycle 94 passed reviewer/build and needs no recovery; Phase 1 theorem-skeleton translation is stable enough for cited-theory backfill; the single lower packet is the barB conditional-expectation generator and divergence/no-boundary theorem behind the active EM weak-FP backend.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldForwardKlDiscreteProofSource — 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.cycle94GeneralMovingTargetDiscreteWeakFpDriftActionLowerObligation
2. SALD.cycle95DiscreteForwardKlClosurePressureUpperPacket
3. sald.general_moving_target_discrete.em_interpolation_fp
4. sald.discrete_forward_kl.em_interpolation_fp
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. thm:forward-KL-discrete
2. thm:general-moving-target-SALD-discrete
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.cycle95_pressure_route
interface : String (explicit)
Text describing intended mathematical interface.
Pressure-test route: thm:forward-KL-discrete can be routed through the current EM, KL/log-ratio mass, LSI, DV, Gronwall, and accumulated-error wrappers only under the shared weak-FP source-sign input; after cycle 94, that source-sign input is blocked by the barB divergence boundary, not by another scalar theorem wrapper.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldForwardKlDiscreteProofSource — 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.cycle95DiscreteForwardKlClosurePressureUpperObligation
2. SALD.cycle89DiscreteForwardKlClosurePressureLowerObligation
3. SALD.cycle90DiscreteForwardKlMassConservationLowerObligation
4. SALD.cycle93GeneralMovingTargetDiscreteKlMassDerivativeLowerObligation
5. SALD.cycle94GeneralMovingTargetDiscreteWeakFpDriftActionLowerObligation
6. SALD.discreteForwardKlPostLsiDerivativeBoundOfLawConstantTestMassScalar
7. SALD.discreteForwardKlPostDvTimeChangedDerivativeScalar
8. SALD.discreteForwardKlMainDisplayBoundScalar
9. sald.discrete_forward_kl.dv_velocity_bound
10. sald.discrete_forward_kl.gronwall_accumulation
11. sald.discrete_forward_kl.accumulated_error_bridge
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. thm:forward-KL-discrete
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.cycle95_middle_route_audit
interface : String (explicit)
Text describing intended mathematical interface.
Middle route audit: synchronize the pressure test after cycle 94. Current compiled wrappers carry thm:forward-KL-discrete to the shared weak-FP source-sign input, and the first non-wrapper blocker is the barB conditional-expectation generator pairing plus divergence/no-boundary theorem, not a new KL, LSI, DV, Gronwall, or display wrapper.
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.cycle95DiscreteForwardKlClosurePressureMiddleObligation
2. SALD.cycle95DiscreteForwardKlClosurePressureUpperObligation
3. SALD.cycle94GeneralMovingTargetDiscreteWeakFpDriftActionLowerObligation
4. SALD.cycle93GeneralMovingTargetDiscreteKlMassDerivativeLowerObligation
5. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBWeakAction
6. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfSampleSplitGeneratorBarBActionHandoff
7. SALD.discreteForwardKlPostLsiDerivativeBoundOfLawConstantTestMassScalar
8. SALD.discreteForwardKlPostDvTimeChangedDerivativeScalar
9. SALD.discreteForwardKlMainDisplayBoundScalar
10. ASTIS.SALD.cycle94.remaining_barB_divergence_boundary
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. sald.discrete_forward_kl.em_interpolation_fp
2. thm:forward-KL-discrete
3. thm:general-moving-target-SALD-discrete
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.cycle95_lower_barB_component_pairing
interface : String (explicit)
Text describing intended mathematical interface.
Lower proof-producing reduction: SALD.generalMovingTargetDiscreteWeakConditionalFpDriftActionOfBarBComponentPairings proves driftAction phi = weakGradPairing barB phi from the component formula barB = dotTk*condC + sigmaCoeff*condScore, weak-pairing additivity/smul/congruence, and component drift pairings. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBComponentPairings then feeds that into the cycle-94 drift-source handoff. Remaining blocker is the component condDistrib/condexp generator pairing plus the divergence/no-boundary theorem.
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.cycle95DiscreteForwardKlClosurePressureLowerObligation
2. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftActionOfBarBComponentPairings
3. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBComponentPairings
4. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBWeakAction
5. SALD.generalMovingTargetDiscreteNamedConditionalDriftComponents
6. SALD.generalMovingTargetDiscreteCondDistribNamedDriftRegularityOfSampleVersions
7. ASTIS.SALD.cycle94.remaining_barB_divergence_boundary
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
4. thm:general-moving-target-SALD-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.cycle95_next_blocker
interface : String (explicit)
Text describing intended mathematical interface.
Next non-wrapper blocker after the lower component-pairing reduction: prove the component conditional-expectation generator pairings for condC and condScore using the source definition of bar b_{k,s}, and prove weakGradPairing barB phi = -(driftDiv phi) by divergence/integration-by-parts/no-boundary for hatRhoS * barB.
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.generalMovingTargetDiscreteWeakConditionalFpDriftActionOfBarBComponentPairings
2. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBComponentPairings
3. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBWeakAction
4. SALD.generalMovingTargetDiscreteCondDistribNamedDriftRegularityOfSampleVersions
5. Mathlib.Probability.Kernel.CondDistrib
6. Mathlib.Probability.Kernel.Condexp
7. Mathlib.MeasureTheory.Integral.DivergenceTheorem
8. appendix.tex:1368-1377
9. 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
4. thm:general-moving-target-SALD-discrete
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.cycle95.reviewer_pressure_check
interface : String (explicit)
Text describing intended mathematical interface.
Reviewer check: accept only a proof-producing discharge of one barB weak-action input or a strictly smaller theorem boundary with source lines and imports. Reject wrapper churn around hdriftSource, source signs, KL mass/log-ratio inputs, LSI/DV/Gronwall, or display algebra.
source : AutoSamplingTheory.SourceAnchor (explicit)
Source pointer.
AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteWeakFpSource — 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.cycle95DiscreteForwardKlClosurePressureUpperObligation
2. ASTIS.SALD.cycle94.remaining_barB_divergence_boundary
3. sald.general_moving_target_discrete.em_interpolation_fp
reusedBy : List String (explicit)
Declared consumers as strings, default empty.
Ordered data items
1. cycle 95 reviewer
2. cycle 96 lower packet
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 cycle95DiscreteForwardKlClosurePressureDag : List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.cycle95.global_phase_judgment"
      interface := "Cycle 95 judgment: cycle 94 passed reviewer/build and needs no recovery; Phase 1 theorem-skeleton translation is stable enough for cited-theory backfill; the single lower packet is the barB conditional-expectation generator and divergence/no-boundary theorem behind the active EM weak-FP backend."
      source := saldForwardKlDiscreteProofSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle94GeneralMovingTargetDiscreteWeakFpDriftActionLowerObligation",
        "SALD.cycle95DiscreteForwardKlClosurePressureUpperPacket",
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.discrete_forward_kl.em_interpolation_fp"
      ]
      reusedBy := ["thm:forward-KL-discrete", "thm:general-moving-target-SALD-discrete"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL_discrete.cycle95_pressure_route"
      interface := "Pressure-test route: thm:forward-KL-discrete can be routed through the current EM, KL/log-ratio mass, LSI, DV, Gronwall, and accumulated-error wrappers only under the shared weak-FP source-sign input; after cycle 94, that source-sign input is blocked by the barB divergence boundary, not by another scalar theorem wrapper."
      source := saldForwardKlDiscreteProofSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle95DiscreteForwardKlClosurePressureUpperObligation",
        "SALD.cycle89DiscreteForwardKlClosurePressureLowerObligation",
        "SALD.cycle90DiscreteForwardKlMassConservationLowerObligation",
        "SALD.cycle93GeneralMovingTargetDiscreteKlMassDerivativeLowerObligation",
        "SALD.cycle94GeneralMovingTargetDiscreteWeakFpDriftActionLowerObligation",
        "SALD.discreteForwardKlPostLsiDerivativeBoundOfLawConstantTestMassScalar",
        "SALD.discreteForwardKlPostDvTimeChangedDerivativeScalar",
        "SALD.discreteForwardKlMainDisplayBoundScalar",
        "sald.discrete_forward_kl.dv_velocity_bound",
        "sald.discrete_forward_kl.gronwall_accumulation",
        "sald.discrete_forward_kl.accumulated_error_bridge"
      ]
      reusedBy := ["thm:forward-KL-discrete"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL_discrete.cycle95_middle_route_audit"
      interface := "Middle route audit: synchronize the pressure test after cycle 94. Current compiled wrappers carry thm:forward-KL-discrete to the shared weak-FP source-sign input, and the first non-wrapper blocker is the barB conditional-expectation generator pairing plus divergence/no-boundary theorem, not a new KL, LSI, DV, Gronwall, or display wrapper."
      source := saldGeneralMovingTargetDiscreteWeakFpDriftActionMathlibSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle95DiscreteForwardKlClosurePressureMiddleObligation",
        "SALD.cycle95DiscreteForwardKlClosurePressureUpperObligation",
        "SALD.cycle94GeneralMovingTargetDiscreteWeakFpDriftActionLowerObligation",
        "SALD.cycle93GeneralMovingTargetDiscreteKlMassDerivativeLowerObligation",
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBWeakAction",
        "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfSampleSplitGeneratorBarBActionHandoff",
        "SALD.discreteForwardKlPostLsiDerivativeBoundOfLawConstantTestMassScalar",
        "SALD.discreteForwardKlPostDvTimeChangedDerivativeScalar",
        "SALD.discreteForwardKlMainDisplayBoundScalar",
        "ASTIS.SALD.cycle94.remaining_barB_divergence_boundary"
      ]
      reusedBy := [
        "sald.discrete_forward_kl.em_interpolation_fp",
        "thm:forward-KL-discrete",
        "thm:general-moving-target-SALD-discrete"
      ]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL_discrete.cycle95_lower_barB_component_pairing"
      interface := "Lower proof-producing reduction: SALD.generalMovingTargetDiscreteWeakConditionalFpDriftActionOfBarBComponentPairings proves driftAction phi = weakGradPairing barB phi from the component formula barB = dotTk*condC + sigmaCoeff*condScore, weak-pairing additivity/smul/congruence, and component drift pairings. SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBComponentPairings then feeds that into the cycle-94 drift-source handoff. Remaining blocker is the component condDistrib/condexp generator pairing plus the divergence/no-boundary theorem."
      source := saldGeneralMovingTargetDiscreteWeakFpDriftActionMathlibSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle95DiscreteForwardKlClosurePressureLowerObligation",
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftActionOfBarBComponentPairings",
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBComponentPairings",
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBWeakAction",
        "SALD.generalMovingTargetDiscreteNamedConditionalDriftComponents",
        "SALD.generalMovingTargetDiscreteCondDistribNamedDriftRegularityOfSampleVersions",
        "ASTIS.SALD.cycle94.remaining_barB_divergence_boundary"
      ]
      reusedBy := [
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.discrete_forward_kl.em_interpolation_fp",
        "thm:forward-KL-discrete",
        "thm:general-moving-target-SALD-discrete"
      ]
      status := ProofStatus.formalized
    },
    {
      id := "ASTIS.SALD.forward_KL_discrete.cycle95_next_blocker"
      interface := "Next non-wrapper blocker after the lower component-pairing reduction: prove the component conditional-expectation generator pairings for condC and condScore using the source definition of bar b_{k,s}, and prove weakGradPairing barB phi = -(driftDiv phi) by divergence/integration-by-parts/no-boundary for hatRhoS * barB."
      source := saldGeneralMovingTargetDiscreteWeakFpDriftActionMathlibSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftActionOfBarBComponentPairings",
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBComponentPairings",
        "SALD.generalMovingTargetDiscreteWeakConditionalFpDriftSourceOfBarBWeakAction",
        "SALD.generalMovingTargetDiscreteCondDistribNamedDriftRegularityOfSampleVersions",
        "Mathlib.Probability.Kernel.CondDistrib",
        "Mathlib.Probability.Kernel.Condexp",
        "Mathlib.MeasureTheory.Integral.DivergenceTheorem",
        "appendix.tex:1368-1377",
        "appendix.tex:1379-1387"
      ]
      reusedBy := [
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.discrete_forward_kl.em_interpolation_fp",
        "thm:forward-KL-discrete",
        "thm:general-moving-target-SALD-discrete"
      ]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.cycle95.reviewer_pressure_check"
      interface := "Reviewer check: accept only a proof-producing discharge of one barB weak-action input or a strictly smaller theorem boundary with source lines and imports. Reject wrapper churn around hdriftSource, source signs, KL mass/log-ratio inputs, LSI/DV/Gronwall, or display algebra."
      source := saldGeneralMovingTargetDiscreteWeakFpSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle95DiscreteForwardKlClosurePressureUpperObligation",
        "ASTIS.SALD.cycle94.remaining_barB_divergence_boundary",
        "sald.general_moving_target_discrete.em_interpolation_fp"
      ]
      reusedBy := ["cycle 95 reviewer", "cycle 96 lower packet"]
      status := ProofStatus.obligation
    }
  ]

/-! ### Cycle 96: middle packet for `condDistrib`/`condexp` generator pairings -/

/-- Cycle-96 middle obligation for the active EM conditional-law backend.

The upper packet rejected the non-EM LSI/DV/Gronwall fallback because the EM
backend still has named work at `appendix.tex:1368-1387`.  This middle record
therefore keeps lower work on the conditional-law side: turn the Mathlib
`condDistrib`/`condexp` representation of the source conditional drift
components into the generator weak-action pairings consumed by the cycle-95
`barB` component theorem.
-/

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