AutoSamplingTheory.SALD.cycle63UnifiedDiscreteGeneralMiddleObligation

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 cycle63UnifiedDiscreteGeneralMiddleObligation : 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.unified_discrete_general.cycle63_middle_route_audit

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 63 middle audits the unified/discrete general route after the upper refresh: thm:unified-forward-KL remains the paper specialization of the continuous general theorem through the correction-field transport bridge, thm:general-moving-target-SALD-discrete remains the source route through EM endpoint/conditional-FP, frozen-delta, LSI, residual DV, and Gronwall, the paired Measure.map helper is only common-space endpoint-law bookkeeping, and the next lower packet is the conditional-law/Fokker-Planck backend over appendix.tex:1358-1387.

source : AutoSamplingTheory.SourceAnchor (explicit)

SourceAnchor supporting the intended requirement.

AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteDerivativeSource — 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.cycle63UnifiedDiscreteGeneralSkeletonUpperPacket
2. SALD.cycle63UnifiedDiscreteGeneralSkeletonObligation
3. SALD.cycle63UnifiedDiscreteGeneralMiddleContract
4. SALD.cycle63UnifiedDiscreteGeneralMeasureBackfillObligation
5. SALD.cycle62GuidedGeneralSkeletonMiddleObligation
6. SALD.cycle62GuidedGeneralScaledResidualLowerObligation
7. SALD.cycle61DiscreteForwardKlSkeletonMiddleObligation
8. SALD.cycle58UnifiedDiscreteGeneralMiddleObligation
9. SALD.cycle53UnifiedDiscreteGeneralMiddleObligation
10. SALD.unifiedForwardKlSpecializationContract
11. sald.unified_forward_kl.transport_velocity_bridge
12. sald.unified_forward_kl.specialization
13. SALD.generalMovingTargetStatementContract
14. SALD.generalVaSaldContract
15. sald.general_moving_target.kl_derivative
16. sald.general_moving_target.dv_m_energy
17. sald.general_moving_target.gronwall_side_conditions
18. SALD.generalMovingTargetDiscreteStatementContract
19. SALD.generalVaSaldDiscreteContract
20. SALD.generalVaSaldEulerMaruyamaContract
21. SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation
22. AutoSamplingTheory.lawMapProdEqOfAEEq
23. AutoSamplingTheory.lawMapProdFst
24. AutoSamplingTheory.lawMapProdSnd
25. SALD.generalMovingTargetDiscreteEmJointEndpointMeasureMapOfNamedInterpolation
26. SALD.generalMovingTargetDiscreteEmJointEndpointMarginalLawsOfNamedInterpolation
27. SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation
28. SALD.generalMovingTargetDiscreteDerivativeCandidateContract
29. SALD.generalMovingTargetDiscreteDerivativeSideConditionContract
30. sald.general_moving_target_discrete.em_interpolation_fp
31. sald.general_moving_target_discrete.derivative_side_conditions
32. sald.general_moving_target_discrete.kl_derivative
33. SALD.saldLsiKlFiDensityTestContract
34. probability.lsi_to_kl_fi
35. dvVariationalFormulaInterface saldDvVariationSource
36. SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract
37. sald.general_moving_target_discrete.dv_finite_log_mgf_witness
38. sald.general_moving_target_discrete.dv_m_energy
39. SALD.generalMovingTargetDiscreteGronwallInstantiationContract
40. SALD.generalMovingTargetDiscreteGronwallSideConditionContract
41. sald.general_moving_target_discrete.gronwall_application
42. sald.general_moving_target_discrete.gronwall_side_conditions
43. lem:gronwall
44. lem:dv_variation
45. eq:LSI-KL-FI

note : String (explicit)

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

This is middle source-to-Lean synchronization and lower-packet selection, not a theorem proof. It adds no hidden endpoint, density, absolute-continuity, regular conditional law, finite-log-mgf, finite-KL/FI, schedule, sigma-positivity, coefficient-regularity, or Fokker-Planck assumptions to the paper statements.

def cycle63UnifiedDiscreteGeneralMiddleObligation : ProofObligation where
  id := "sald.unified_discrete_general.cycle63_middle_route_audit"
  statement := "Cycle 63 middle audits the unified/discrete general route after the upper refresh: thm:unified-forward-KL remains the paper specialization of the continuous general theorem through the correction-field transport bridge, thm:general-moving-target-SALD-discrete remains the source route through EM endpoint/conditional-FP, frozen-delta, LSI, residual DV, and Gronwall, the paired Measure.map helper is only common-space endpoint-law bookkeeping, and the next lower packet is the conditional-law/Fokker-Planck backend over appendix.tex:1358-1387."
  source := saldGeneralMovingTargetDiscreteDerivativeSource
  status := ProofStatus.obligation
  dependsOn := [
    "SALD.cycle63UnifiedDiscreteGeneralSkeletonUpperPacket",
    "SALD.cycle63UnifiedDiscreteGeneralSkeletonObligation",
    "SALD.cycle63UnifiedDiscreteGeneralMiddleContract",
    "SALD.cycle63UnifiedDiscreteGeneralMeasureBackfillObligation",
    "SALD.cycle62GuidedGeneralSkeletonMiddleObligation",
    "SALD.cycle62GuidedGeneralScaledResidualLowerObligation",
    "SALD.cycle61DiscreteForwardKlSkeletonMiddleObligation",
    "SALD.cycle58UnifiedDiscreteGeneralMiddleObligation",
    "SALD.cycle53UnifiedDiscreteGeneralMiddleObligation",
    "SALD.unifiedForwardKlSpecializationContract",
    "sald.unified_forward_kl.transport_velocity_bridge",
    "sald.unified_forward_kl.specialization",
    "SALD.generalMovingTargetStatementContract",
    "SALD.generalVaSaldContract",
    "sald.general_moving_target.kl_derivative",
    "sald.general_moving_target.dv_m_energy",
    "sald.general_moving_target.gronwall_side_conditions",
    "SALD.generalMovingTargetDiscreteStatementContract",
    "SALD.generalVaSaldDiscreteContract",
    "SALD.generalVaSaldEulerMaruyamaContract",
    "SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation",
    "AutoSamplingTheory.lawMapProdEqOfAEEq",
    "AutoSamplingTheory.lawMapProdFst",
    "AutoSamplingTheory.lawMapProdSnd",
    "SALD.generalMovingTargetDiscreteEmJointEndpointMeasureMapOfNamedInterpolation",
    "SALD.generalMovingTargetDiscreteEmJointEndpointMarginalLawsOfNamedInterpolation",
    "SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation",
    "SALD.generalMovingTargetDiscreteDerivativeCandidateContract",
    "SALD.generalMovingTargetDiscreteDerivativeSideConditionContract",
    "sald.general_moving_target_discrete.em_interpolation_fp",
    "sald.general_moving_target_discrete.derivative_side_conditions",
    "sald.general_moving_target_discrete.kl_derivative",
    "SALD.saldLsiKlFiDensityTestContract",
    "probability.lsi_to_kl_fi",
    "dvVariationalFormulaInterface saldDvVariationSource",
    "SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract",
    "sald.general_moving_target_discrete.dv_finite_log_mgf_witness",
    "sald.general_moving_target_discrete.dv_m_energy",
    "SALD.generalMovingTargetDiscreteGronwallInstantiationContract",
    "SALD.generalMovingTargetDiscreteGronwallSideConditionContract",
    "sald.general_moving_target_discrete.gronwall_application",
    "sald.general_moving_target_discrete.gronwall_side_conditions",
    "lem:gronwall",
    "lem:dv_variation",
    "eq:LSI-KL-FI"
  ]
  note := "This is middle source-to-Lean synchronization and lower-packet selection, not a theorem proof. It adds no hidden endpoint, density, absolute-continuity, regular conditional law, finite-log-mgf, finite-KL/FI, schedule, sigma-positivity, coefficient-regularity, or Fokker-Planck assumptions to the paper statements."

/-- Cycle-63 proof-DAG pane for the unified/discrete general route and one
narrow endpoint-law backfill. -/