Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

AutoSamplingTheory.SALD.forwardKlProofDag

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 forwardKlProofDag : List ProofDagBlock

Construction and field-by-field explanation

Concatenate the shown data expressions in source order. They remain symbolic and are not evaluated.

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.

Concatenate these expressions without evaluating them

  1. Concatenate these expressions without evaluating them

    1. Concatenate these expressions without evaluating them

      1. Concatenate these expressions without evaluating them

        1. Concatenate these expressions without evaluating them

          1. Concatenate these expressions without evaluating them

            1. Concatenate these expressions without evaluating them

              1. Concatenate these expressions without evaluating them

                1. Concatenate these expressions without evaluating them

                  1. AutoSamplingTheory.SALD.cycle49MainSkeletonAnalyticReadinessDag — audited data reference, not expanded and not a compiled dependency edge
                  2. AutoSamplingTheory.SALD.cycle54MainSkeletonAnalyticInterfaceDag — audited data reference, not expanded and not a compiled dependency edge
                2. AutoSamplingTheory.SALD.cycle59MainSkeletonAnalyticInterfaceDag — audited data reference, not expanded and not a compiled dependency edge
              2. AutoSamplingTheory.SALD.cycle64MainSkeletonAnalyticInterfaceDag — audited data reference, not expanded and not a compiled dependency edge
            2. AutoSamplingTheory.SALD.cycle69MainSkeletonAnalyticInterfaceDag — audited data reference, not expanded and not a compiled dependency edge
          2. AutoSamplingTheory.SALD.cycle50ForwardKlSkeletonDag — audited data reference, not expanded and not a compiled dependency edge
        2. AutoSamplingTheory.SALD.cycle55ForwardKlSkeletonDag — audited data reference, not expanded and not a compiled dependency edge
      2. AutoSamplingTheory.SALD.cycle60ForwardKlSkeletonDag — audited data reference, not expanded and not a compiled dependency edge
    2. AutoSamplingTheory.SALD.cycle65ForwardKlSkeletonDag — audited data reference, not expanded and not a compiled dependency edge

  2. Ordered data items

    1. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.middle_source_to_lean_map
      interface : String (explicit)

      Text describing intended mathematical interface.

      Classify appendix lines 168-252 and main_body lines 218-248 as Lean contracts, cited results, or named obligations, and hand off the current cycle's selected lower slice.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlProofSource — 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.cycle14ForwardKlUpperPacket
      2. SALD.cycle14ForwardKlMiddleContract
      3. SALD.cycle18ForwardKlUpperPacket
      4. SALD.cycle18ForwardKlMiddleContract
      5. SALD.cycle22ForwardKlUpperPacket
      6. SALD.cycle22ForwardKlMiddleContract
      7. SALD.cycle26ForwardKlUpperPacket
      8. SALD.cycle26ForwardKlMiddleContract
      9. SALD.cycle30ForwardKlUpperPacket
      10. SALD.cycle30ForwardKlMiddleContract
      11. SALD.cycle34ForwardKlDerivativeUpperPacket
      12. SALD.cycle34ForwardKlDerivativeMiddleContract
      13. SALD.cycle39ForwardKlDerivativeUpperPacket
      14. SALD.cycle39ForwardKlDerivativeMiddleContract
      15. SALD.cycle45ForwardKlSkeletonUpperPacket
      16. SALD.cycle45ForwardKlSkeletonObligation
      17. SALD.cycle45ForwardKlSkeletonMiddleContract
      18. SALD.cycle45ForwardKlSkeletonMiddleObligation
      19. ASTIS.SALD.forward_KL.cycle45_theorem_skeleton_route
      20. sald.forward_kl.cycle45_middle_route_audit
      21. SALD.cycle50ForwardKlSkeletonUpperPacket
      22. SALD.cycle50ForwardKlSkeletonObligation
      23. SALD.cycle50ForwardKlSkeletonMiddleContract
      24. SALD.cycle50ForwardKlSkeletonMiddleObligation
      25. ASTIS.SALD.forward_KL.cycle50_theorem_skeleton_route
      26. ASTIS.SALD.forward_KL.cycle50_middle_route_audit
      27. sald.forward_kl.cycle50_theorem_skeleton_route
      28. sald.forward_kl.cycle50_middle_route_audit
      29. SALD.continuousForwardKlStatementContract
      30. sald.forward_kl.endpoint_schedule_identities
      31. sald.forward_kl.moving_target_dependency_chain
      32. sald.forward_kl.cycle30_derivative_side_upper
      33. sald.forward_kl.cycle30_derivative_side_middle
      34. sald.forward_kl.density_boundary_regular
      35. sald.forward_kl.cycle34_derivative_scalar
      36. sald.forward_kl.cycle34_derivative_middle
      37. sald.forward_kl.cycle39_derivative_upper
      38. sald.forward_kl.cycle39_derivative_middle
      39. SALD.forwardKlInverseScheduleDerivativeScalar
      40. SALD.forwardKlTimeChangeSquareCoefficientRewriteOfProductScalar
      41. SALD.forwardKlVelocitySquareScalingScalar
      42. SALD.forwardKlTimeChangedDerivativeBoundOfProductScalar
      43. SALD.forwardKlPreDvDerivativeBoundOfProductScalar
      44. SALD.forwardKlPreDvDerivativeBoundOfVelocityScalingScalar
      45. SALD.forwardKlLsiDerivativeBoundOfKlFiScalar
      46. SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar
      47. sald.forward_kl.schedule_time_change
      48. sald.forward_kl.kl_derivative
      49. probability.lsi_to_kl_fi
      50. sald.forward_kl.cycle26_dv_witness_middle
      51. sald.forward_kl.dv_finite_log_mgf_witness
      52. sald.forward_kl.coefficient_chain_audit
      53. sald.forward_kl.gronwall_side_conditions
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. cycle14/cycle18/cycle22/cycle26/cycle30 lower packets
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    2. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.cycle45_theorem_skeleton_route
      interface : String (explicit)

      Text describing intended mathematical interface.

      Wire the five slow analytic interfaces into the continuous forward-KL theorem skeleton: derivative/Fokker-Planck, LSI/KL/FI, DV finite-log-mgf, Gronwall endpoint/exponent side conditions, and downstream EM interpolation visibility.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlProofSource — 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.cycle44MainSkeletonAnalyticInterfaceObligation
      2. SALD.cycle45ForwardKlSkeletonUpperPacket
      3. SALD.cycle45ForwardKlSkeletonObligation
      4. SALD.cycle45ForwardKlSkeletonDag
      5. SALD.cycle45ForwardKlSkeletonMiddleContract
      6. SALD.cycle45ForwardKlSkeletonMiddleObligation
      7. SALD.continuousForwardKlStatementContract
      8. sald.forward_kl.middle_source_to_lean_map
      9. sald.forward_kl.cycle45_middle_route_audit
      10. sald.forward_kl.moving_target_dependency_chain
      11. sald.forward_kl.kl_derivative
      12. probability.lsi_to_kl_fi
      13. sald.forward_kl.dv_finite_log_mgf_witness
      14. sald.forward_kl.dv_energy_bound
      15. sald.forward_kl.gronwall_application
      16. sald.forward_kl.gronwall_side_conditions
      17. sald.discrete_forward_kl.em_interpolation_fp
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. ASTIS-SALD-001 main skeleton sprint 2
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    3. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.cycle45_middle_route_audit
      interface : String (explicit)

      Text describing intended mathematical interface.

      Middle source-to-Lean audit for the continuous forward-KL skeleton: verify the exact main_body.tex:238-247 statement and appendix.tex:168-252 route, then select the theorem-level Gronwall side-condition backend for lower work.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlProofSource — 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.cycle45ForwardKlSkeletonMiddleContract
      2. SALD.cycle45ForwardKlSkeletonMiddleObligation
      3. SALD.cycle45ForwardKlSkeletonObligation
      4. SALD.continuousForwardKlStatementContract
      5. SALD.forwardKlDerivativeCandidateContract
      6. SALD.forwardKlDerivativeSideConditionContract
      7. SALD.saldLsiKlFiDensityTestContract
      8. SALD.forwardKlDvFiniteLogMgfWitnessContract
      9. SALD.forwardKlGronwallInstantiationContract
      10. SALD.forwardKlGronwallSideConditionContract
      11. sald.forward_kl.gronwall_side_conditions
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. cycle 45 lower Gronwall-side-condition packet
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    4. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.moving_target_dependencies
      interface : String (explicit)

      Text describing intended mathematical interface.

      Audit the theorem-level moving-target assumptions and wire them to the derivative, LSI, DV, and Gronwall proof blocks without changing thm:forward-KL.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlSource — 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.forward_kl.middle_source_to_lean_map
      2. sald.forward_kl.endpoint_schedule_identities
      3. eq:SALD
      4. eq:FP-eq
      5. TransportVelocityContract
      6. eq:LSI-KL-FI
      7. def:alpha-complexity
      8. lem:dv_variation
      9. lem:gronwall
      10. sald.forward_kl.schedule_time_change
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. thm:forward-KL-discrete
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    5. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.endpoint_schedule_identities
      interface : String (explicit)

      Text describing intended mathematical interface.

      Isolate the inverse-schedule endpoint rewrites s(0)=0, S=s(T), t(s(T))=T, tilde_pi_{s(t)}=pi_t, and the K(0)/K(T) identifications used after Gronwall.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlEndpointScheduleSource — 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.forwardKlEndpointScheduleContract
      2. sald.forward_kl.moving_target_dependency_chain
      3. sald.forward_kl.schedule_time_change
      4. sald.forward_kl.gronwall_side_conditions
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. cycle14 lower packet
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    6. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.cycle30_derivative_side_upper
      interface : String (explicit)

      Text describing intended mathematical interface.

      Upper-role lower packet for the derivative-side interface: mass conservation, KL differentiation, SALD and target integration by parts, slowed-target transport, Young 1/2 coefficients, and the time-change handoff.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlDerivativeSource — 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.cycle30ForwardKlUpperPacket
      2. SALD.forwardKlDerivativeCandidateContract
      3. SALD.forwardKlDerivativeSideConditionContract
      4. SALD.forwardKlMovingTargetDependencyContract
      5. sald.forward_kl.density_boundary_regular
      6. sald.forward_kl.schedule_time_change
      7. eq:SALD
      8. eq:FP-eq
      9. eq:LSI-KL-FI
      10. TransportVelocityContract
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. cycle30 lower derivative-side packet
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    7. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.cycle30_derivative_side_middle
      interface : String (explicit)

      Text describing intended mathematical interface.

      Middle source-to-Lean map for appendix.tex:168-208, selecting appendix.tex:168-185 density/boundary/FI identification as the first lower sub-slice and leaving target transport, LSI, time-change, DV, and Gronwall as separate obligations.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlDerivativeSource — 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.cycle30ForwardKlUpperPacket
      2. SALD.cycle30ForwardKlMiddleContract
      3. SALD.forwardKlDerivativeSideConditionContract
      4. SALD.forwardKlDensityBoundaryObligation
      5. sald.forward_kl.cycle30_derivative_side_upper
      6. sald.forward_kl.density_boundary_regular
      7. sald.forward_kl.kl_derivative
      8. eq:SALD
      9. eq:FP-eq
      10. KLContract
      11. FIContract
      12. FokkerPlanckContract
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. cycle30 lower density-boundary packet
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    8. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.cycle30_density_boundary_lower
      interface : String (explicit)

      Text describing intended mathematical interface.

      Lower scalar handoff for appendix.tex:168-185: substitute the supplied first-term identity firstTerm=-FI into the KL derivative display, while keeping mass conservation, Fokker-Planck, integration by parts, and FI identification as obligations.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlDerivativeSource — 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.cycle30ForwardKlMiddleContract
      2. SALD.forwardKlDerivativeSideConditionContract
      3. SALD.forwardKlDensityBoundaryObligation
      4. SALD.forwardKlFirstTermFisherSubstitutionScalar
      5. sald.forward_kl.cycle30_derivative_side_middle
      6. sald.forward_kl.density_boundary_regular
      7. eq:FP-eq
      8. KLContract
      9. FIContract
      10. FokkerPlanckContract
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. sald.forward_kl.kl_derivative
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    9. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.cycle34_derivative_scalar
      interface : String (explicit)

      Text describing intended mathematical interface.

      Proof-producing scalar derivative handoff for appendix.tex:168-228: combine the first-term Fisher substitution, target-side Young bound, supplied LSI half-Fisher comparison, and scalar inverse-schedule coefficient handoff while leaving analytic time-change inputs open.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlDerivativeSource — 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.cycle34ForwardKlDerivativeUpperPacket
      2. SALD.cycle34ForwardKlDerivativeMiddleContract
      3. SALD.forwardKlTargetTransportYoungBoundScalar
      4. SALD.forwardKlPostYoungDerivativeBoundScalar
      5. SALD.forwardKlPostYoungDerivativeBoundOfCauchyScalar
      6. SALD.forwardKlLsiDerivativeBoundScalar
      7. SALD.forwardKlLsiDerivativeBoundOfKlFiScalar
      8. SALD.forwardKlTimeChangedDerivativeBoundScalar
      9. SALD.forwardKlFirstTermFisherSubstitutionScalar
      10. sald.forward_kl.cycle34_target_young_lower
      11. sald.forward_kl.cycle30_density_boundary_lower
      12. sald.forward_kl.density_boundary_regular
      13. probability.lsi_to_kl_fi
      14. sald.forward_kl.schedule_time_change
      15. sald.forward_kl.kl_derivative
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. sald.forward_kl.kl_derivative
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    10. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.cycle39_derivative_upper
      interface : String (explicit)

      Text describing intended mathematical interface.

      Upper proof-closure packet for appendix.tex:168-228: use the compiled pre-DV scalar pipeline and assign lower work to the remaining density/boundary and schedule-time-change inputs before any ledger expansion or EM interpolation work.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlDerivativeSource — 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.cycle39ForwardKlDerivativeUpperPacket
      2. SALD.cycle39ForwardKlDerivativeMiddleContract
      3. SALD.cycle39ForwardKlDerivativeUpperObligation
      4. SALD.forwardKlPreDvDerivativeBoundScalar
      5. SALD.forwardKlPreDvDerivativeBoundOfProductScalar
      6. SALD.forwardKlPreDvDerivativeBoundOfVelocityScalingScalar
      7. SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar
      8. SALD.forwardKlInverseScheduleDerivativeScalar
      9. SALD.forwardKlTimeChangeSquareCoefficientRewriteOfProductScalar
      10. SALD.forwardKlVelocitySquareScalingScalar
      11. SALD.forwardKlTimeChangedDerivativeBoundOfProductScalar
      12. SALD.forwardKlFirstTermFisherSubstitutionScalar
      13. SALD.forwardKlTargetTransportYoungBoundScalar
      14. SALD.forwardKlPostYoungDerivativeBoundScalar
      15. SALD.forwardKlPostYoungDerivativeBoundOfCauchyScalar
      16. SALD.forwardKlLsiDerivativeBoundScalar
      17. SALD.forwardKlTimeChangedDerivativeBoundScalar
      18. sald.forward_kl.density_boundary_regular
      19. sald.forward_kl.schedule_time_change
      20. probability.lsi_to_kl_fi
      21. sald.forward_kl.kl_derivative
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. sald.forward_kl.kl_derivative
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    11. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.cycle39_derivative_middle
      interface : String (explicit)

      Text describing intended mathematical interface.

      Middle source-to-Lean map for appendix.tex:191-228: expose source-shaped inverse-schedule product and slowed-velocity norm-square scalar lemmas feeding the pre-DV derivative pipeline.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlDerivativeSource — 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.cycle39ForwardKlDerivativeMiddleContract
      2. SALD.cycle39ForwardKlDerivativeMiddleObligation
      3. SALD.forwardKlInverseScheduleDerivativeScalar
      4. SALD.forwardKlTimeChangeSquareCoefficientRewriteOfProductScalar
      5. SALD.forwardKlVelocitySquareScalingScalar
      6. SALD.forwardKlTimeChangedDerivativeBoundOfProductScalar
      7. SALD.forwardKlPreDvDerivativeBoundOfProductScalar
      8. SALD.forwardKlPreDvDerivativeBoundOfVelocityScalingScalar
      9. SALD.forwardKlLsiDerivativeBoundOfKlFiScalar
      10. SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar
      11. SALD.forwardKlPreDvDerivativeBoundScalar
      12. sald.forward_kl.cycle39_derivative_upper
      13. sald.forward_kl.schedule_time_change
      14. sald.forward_kl.density_boundary_regular
      15. probability.lsi_to_kl_fi
      16. sald.forward_kl.kl_derivative
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. sald.forward_kl.kl_derivative
      3. sald.forward_kl.schedule_time_change
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    12. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.coefficient_chain_audit
      interface : String (explicit)

      Text describing intended mathematical interface.

      Preserve the source LSI, DV, and Gronwall coefficient flow from appendix lines 210-252, including the source-line ledger, scalar side conditions, and final exponent split in the theorem statement.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlDependencyChainSource — 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. eq:LSI-KL-FI
      2. def:alpha-complexity
      3. lem:dv_variation
      4. lem:gronwall
      5. sald.forward_kl.kl_derivative
      6. sald.forward_kl.dv_energy_bound
      7. sald.forward_kl.gronwall_application
      8. sald.forward_kl.gronwall_side_conditions
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. thm:forward-KL-discrete
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    13. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.gronwall_side_conditions
      interface : String (explicit)

      Text describing intended mathematical interface.

      Expose endpoint K(0)/K(T) identifications, coefficient regularity, exponent splitting, and residual-exponent sign facts for the final Gronwall display.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlGronwallSource — 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.cycle18ForwardKlUpperPacket
      2. SALD.cycle18ForwardKlMiddleContract
      3. SALD.cycle22ForwardKlUpperPacket
      4. SALD.cycle22ForwardKlMiddleContract
      5. sald.forward_kl.moving_target_dependency_chain
      6. sald.forward_kl.endpoint_schedule_identities
      7. sald.forward_kl.schedule_time_change
      8. sald.forward_kl.kl_derivative
      9. sald.forward_kl.dv_energy_bound
      10. sald.gronwall.integrating_factor
      11. sald.gronwall.exponent_rewrite
      12. SALD.gronwallNegIntegralRewriteScalar
      13. SALD.gronwallExpProductRewriteScalar
      14. SALD.gronwallExpProductRewriteIntervalIntegral
      15. SALD.gronwallExpProductRewriteIntegralCongr
      16. SALD.forwardKlGronwallCoeffIntervalIntegrable
      17. SALD.forwardKlGronwallCoeffAdjacentIntervalIntegrable
      18. SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces
      19. SALD.forwardKlGronwallCoeffIntegralSub
      20. SALD.forwardKlGronwallInitialExponentSplitScalar
      21. SALD.forwardKlGronwallInitialExponentSplitOfPieces
      22. SALD.forwardKlGronwallResidualExponentDropScalar
      23. SALD.forwardKlGronwallResidualExponentDropIntegral
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    14. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.alpha_complexity
      interface : String (explicit)

      Text describing intended mathematical interface.

      Define E_alpha(pi_t,v_t) and A_alpha(pi,v); expose finite log-mgf obligations for alpha in (0, alpha0].
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldAlphaComplexitySource — 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. exponential moment vocabulary
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. thm:forward-KL-discrete
      3. thm:general-moving-target-SALD
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.contractOnly — stored label only; no proof certification
    15. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.dv_alpha_mgf_monotonicity
      interface : String (explicit)

      Text describing intended mathematical interface.

      Derive the theorem-specific finite log-mgf at alpha from the source alpha0-complexity assumption for Z=alpha*||v_t||^2 before applying DV.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlDvEnergySource — 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. def:alpha-complexity
      2. SALD.saldDvFiniteLogMgfContract
      3. sald.dv_variation.finite_log_mgf_interface
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. sald.forward_kl.dv_finite_log_mgf_witness
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    16. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.cycle26_middle_dv_witness
      interface : String (explicit)

      Text describing intended mathematical interface.

      Middle source-dependency map for the DV witness: common-space/absolute-continuity, measurability of Z=alpha*||v_t||^2, alpha0-to-alpha finite log-mgf, and positive-alpha division.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlDvEnergySource — 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.cycle26ForwardKlUpperPacket
      2. SALD.cycle26ForwardKlMiddleContract
      3. SALD.forwardKlDvFiniteLogMgfWitnessContract
      4. SALD.forwardKlDvAlphaMonotonicityContract
      5. SALD.saldDvFiniteLogMgfContract
      6. probability.dv_variational_formula
      7. sald.dv_variation.finite_log_mgf_interface
      8. sald.forward_kl.dv_alpha_mgf_monotonicity
      9. SALD.forwardKlDvPositiveAlphaScalingScalar
      10. SALD.forwardKlDvPositiveAlphaCoefficientScalar
      11. sald.forward_kl.moving_target_dependency_chain
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. sald.forward_kl.dv_finite_log_mgf_witness
      2. thm:forward-KL
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    17. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.derivative
      interface : String (explicit)

      Text describing intended mathematical interface.

      Derive the source differential inequality before DV: dK/dt <= -dot{s}*C_LSI*K + (1/2)*dot{s}^(-1)*||v_t||^2_{L2(rho)}.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlDerivativeSource — 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.cycle30ForwardKlUpperPacket
      2. SALD.cycle30ForwardKlMiddleContract
      3. SALD.cycle39ForwardKlDerivativeUpperPacket
      4. SALD.cycle39ForwardKlDerivativeMiddleContract
      5. sald.forward_kl.cycle30_derivative_side_upper
      6. sald.forward_kl.cycle30_derivative_side_middle
      7. sald.forward_kl.cycle30_density_boundary_lower
      8. sald.forward_kl.cycle39_derivative_upper
      9. sald.forward_kl.cycle39_derivative_middle
      10. eq:SALD
      11. eq:FP-eq
      12. eq:LSI-KL-FI
      13. TransportVelocityContract
      14. SALD.forwardKlFirstTermFisherSubstitutionScalar
      15. SALD.forwardKlPostYoungDerivativeBoundScalar
      16. SALD.forwardKlLsiDerivativeBoundScalar
      17. sald.forward_kl.cycle34_derivative_scalar
      18. SALD.forwardKlPreDvDerivativeBoundScalar
      19. SALD.forwardKlPreDvDerivativeBoundOfProductScalar
      20. SALD.forwardKlPreDvDerivativeBoundOfVelocityScalingScalar
      21. SALD.forwardKlInverseScheduleDerivativeScalar
      22. SALD.forwardKlVelocitySquareScalingScalar
      23. sald.forward_kl.density_boundary_regular
      24. sald.forward_kl.schedule_time_change
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. thm:forward-KL-discrete
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    18. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.dv_finite_log_mgf_witness
      interface : String (explicit)

      Text describing intended mathematical interface.

      Provide the theorem-specific DV finite-log-mgf and common-space witness for Z=alpha*||v_t||^2 from the alpha0-complexity assumption before the DV-energy inequality is used.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlDvEnergySource — 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.cycle26ForwardKlUpperPacket
      2. SALD.cycle26ForwardKlMiddleContract
      3. ASTIS.SALD.forward_KL.cycle26_middle_dv_witness
      4. sald.forward_kl.cycle26_dv_witness_middle
      5. lem:dv_variation
      6. def:alpha-complexity
      7. SALD.saldDvFiniteLogMgfContract
      8. sald.dv_variation.finite_log_mgf_interface
      9. sald.forward_kl.dv_alpha_mgf_monotonicity
      10. SALD.forwardKlDvPositiveAlphaScalingScalar
      11. SALD.forwardKlDvPositiveAlphaCoefficientScalar
      12. sald.forward_kl.cycle26_dv_positive_alpha_lower
      13. sald.forward_kl.moving_target_dependency_chain
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. thm:forward-KL-discrete DV pattern
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    19. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.dv_energy
      interface : String (explicit)

      Text describing intended mathematical interface.

      Instantiate DV with Z=alpha*||v_t||^2 and rewrite the log-mgf term as E_alpha(pi_t,v_t).
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlDvEnergySource — 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. lem:dv_variation
      2. def:alpha-complexity
      3. SALD.cycle26ForwardKlMiddleContract
      4. sald.forward_kl.cycle26_dv_witness_middle
      5. sald.forward_kl.dv_alpha_mgf_monotonicity
      6. sald.forward_kl.dv_finite_log_mgf_witness
      7. SALD.forwardKlDvPositiveAlphaScalingScalar
      8. SALD.forwardKlDvPositiveAlphaCoefficientScalar
      9. sald.forward_kl.cycle26_dv_positive_alpha_lower
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. thm:forward-KL-discrete
      3. thm:general-moving-target-SALD
      status : AutoSamplingTheory.ProofStatus (explicit)

      Recorded workflow status, default planned.

      AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification
    20. id : String (explicit)

      Stable plan-node identifier.

      ASTIS.SALD.forward_KL.gronwall_application
      interface : String (explicit)

      Text describing intended mathematical interface.

      Apply lem:gronwall with the paper's a(t), b(t), then split the exponent exactly as in the theorem statement.
      source : AutoSamplingTheory.SourceAnchor (explicit)

      Source pointer.

      AutoSamplingTheory.SALD.saldForwardKlGronwallSource — 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. lem:gronwall
      2. sald.forward_kl.kl_derivative
      3. sald.forward_kl.dv_energy_bound
      reusedBy : List String (explicit)

      Declared consumers as strings, default empty.

      Ordered data items

      1. thm:forward-KL
      2. thm:forward-KL-discrete
      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 forwardKlProofDag : List ProofDagBlock :=
  cycle49MainSkeletonAnalyticReadinessDag ++
  cycle54MainSkeletonAnalyticInterfaceDag ++
  cycle59MainSkeletonAnalyticInterfaceDag ++
  cycle64MainSkeletonAnalyticInterfaceDag ++
  cycle69MainSkeletonAnalyticInterfaceDag ++
  cycle50ForwardKlSkeletonDag ++
  cycle55ForwardKlSkeletonDag ++
  cycle60ForwardKlSkeletonDag ++
  cycle65ForwardKlSkeletonDag ++
  [
    {
      id := "ASTIS.SALD.forward_KL.middle_source_to_lean_map"
      interface := "Classify appendix lines 168-252 and main_body lines 218-248 as Lean contracts, cited results, or named obligations, and hand off the current cycle's selected lower slice."
      source := saldForwardKlProofSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle14ForwardKlUpperPacket",
        "SALD.cycle14ForwardKlMiddleContract",
        "SALD.cycle18ForwardKlUpperPacket",
        "SALD.cycle18ForwardKlMiddleContract",
        "SALD.cycle22ForwardKlUpperPacket",
        "SALD.cycle22ForwardKlMiddleContract",
        "SALD.cycle26ForwardKlUpperPacket",
        "SALD.cycle26ForwardKlMiddleContract",
        "SALD.cycle30ForwardKlUpperPacket",
        "SALD.cycle30ForwardKlMiddleContract",
        "SALD.cycle34ForwardKlDerivativeUpperPacket",
        "SALD.cycle34ForwardKlDerivativeMiddleContract",
        "SALD.cycle39ForwardKlDerivativeUpperPacket",
        "SALD.cycle39ForwardKlDerivativeMiddleContract",
        "SALD.cycle45ForwardKlSkeletonUpperPacket",
          "SALD.cycle45ForwardKlSkeletonObligation",
          "SALD.cycle45ForwardKlSkeletonMiddleContract",
          "SALD.cycle45ForwardKlSkeletonMiddleObligation",
          "ASTIS.SALD.forward_KL.cycle45_theorem_skeleton_route",
          "sald.forward_kl.cycle45_middle_route_audit",
          "SALD.cycle50ForwardKlSkeletonUpperPacket",
          "SALD.cycle50ForwardKlSkeletonObligation",
          "SALD.cycle50ForwardKlSkeletonMiddleContract",
          "SALD.cycle50ForwardKlSkeletonMiddleObligation",
          "ASTIS.SALD.forward_KL.cycle50_theorem_skeleton_route",
          "ASTIS.SALD.forward_KL.cycle50_middle_route_audit",
          "sald.forward_kl.cycle50_theorem_skeleton_route",
          "sald.forward_kl.cycle50_middle_route_audit",
          "SALD.continuousForwardKlStatementContract",
          "sald.forward_kl.endpoint_schedule_identities",
          "sald.forward_kl.moving_target_dependency_chain",
        "sald.forward_kl.cycle30_derivative_side_upper",
        "sald.forward_kl.cycle30_derivative_side_middle",
        "sald.forward_kl.density_boundary_regular",
        "sald.forward_kl.cycle34_derivative_scalar",
        "sald.forward_kl.cycle34_derivative_middle",
        "sald.forward_kl.cycle39_derivative_upper",
        "sald.forward_kl.cycle39_derivative_middle",
        "SALD.forwardKlInverseScheduleDerivativeScalar",
        "SALD.forwardKlTimeChangeSquareCoefficientRewriteOfProductScalar",
        "SALD.forwardKlVelocitySquareScalingScalar",
        "SALD.forwardKlTimeChangedDerivativeBoundOfProductScalar",
        "SALD.forwardKlPreDvDerivativeBoundOfProductScalar",
        "SALD.forwardKlPreDvDerivativeBoundOfVelocityScalingScalar",
        "SALD.forwardKlLsiDerivativeBoundOfKlFiScalar",
        "SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar",
        "sald.forward_kl.schedule_time_change",
        "sald.forward_kl.kl_derivative",
        "probability.lsi_to_kl_fi",
        "sald.forward_kl.cycle26_dv_witness_middle",
        "sald.forward_kl.dv_finite_log_mgf_witness",
        "sald.forward_kl.coefficient_chain_audit",
        "sald.forward_kl.gronwall_side_conditions"
      ]
      reusedBy := ["thm:forward-KL", "cycle14/cycle18/cycle22/cycle26/cycle30 lower packets"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle45_theorem_skeleton_route"
      interface := "Wire the five slow analytic interfaces into the continuous forward-KL theorem skeleton: derivative/Fokker-Planck, LSI/KL/FI, DV finite-log-mgf, Gronwall endpoint/exponent side conditions, and downstream EM interpolation visibility."
      source := saldForwardKlProofSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle44MainSkeletonAnalyticInterfaceObligation",
        "SALD.cycle45ForwardKlSkeletonUpperPacket",
        "SALD.cycle45ForwardKlSkeletonObligation",
        "SALD.cycle45ForwardKlSkeletonDag",
        "SALD.cycle45ForwardKlSkeletonMiddleContract",
        "SALD.cycle45ForwardKlSkeletonMiddleObligation",
        "SALD.continuousForwardKlStatementContract",
        "sald.forward_kl.middle_source_to_lean_map",
        "sald.forward_kl.cycle45_middle_route_audit",
        "sald.forward_kl.moving_target_dependency_chain",
        "sald.forward_kl.kl_derivative",
        "probability.lsi_to_kl_fi",
        "sald.forward_kl.dv_finite_log_mgf_witness",
        "sald.forward_kl.dv_energy_bound",
        "sald.forward_kl.gronwall_application",
        "sald.forward_kl.gronwall_side_conditions",
        "sald.discrete_forward_kl.em_interpolation_fp"
      ]
      reusedBy := ["thm:forward-KL", "ASTIS-SALD-001 main skeleton sprint 2"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle45_middle_route_audit"
      interface := "Middle source-to-Lean audit for the continuous forward-KL skeleton: verify the exact main_body.tex:238-247 statement and appendix.tex:168-252 route, then select the theorem-level Gronwall side-condition backend for lower work."
      source := saldForwardKlProofSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle45ForwardKlSkeletonMiddleContract",
        "SALD.cycle45ForwardKlSkeletonMiddleObligation",
        "SALD.cycle45ForwardKlSkeletonObligation",
        "SALD.continuousForwardKlStatementContract",
        "SALD.forwardKlDerivativeCandidateContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.saldLsiKlFiDensityTestContract",
        "SALD.forwardKlDvFiniteLogMgfWitnessContract",
        "SALD.forwardKlGronwallInstantiationContract",
        "SALD.forwardKlGronwallSideConditionContract",
        "sald.forward_kl.gronwall_side_conditions"
      ]
      reusedBy := ["thm:forward-KL", "cycle 45 lower Gronwall-side-condition packet"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.moving_target_dependencies"
      interface := "Audit the theorem-level moving-target assumptions and wire them to the derivative, LSI, DV, and Gronwall proof blocks without changing thm:forward-KL."
      source := saldForwardKlSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "sald.forward_kl.middle_source_to_lean_map",
        "sald.forward_kl.endpoint_schedule_identities",
        "eq:SALD",
        "eq:FP-eq",
        "TransportVelocityContract",
        "eq:LSI-KL-FI",
        "def:alpha-complexity",
        "lem:dv_variation",
        "lem:gronwall",
        "sald.forward_kl.schedule_time_change"
      ]
      reusedBy := ["thm:forward-KL", "thm:forward-KL-discrete"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.endpoint_schedule_identities"
      interface := "Isolate the inverse-schedule endpoint rewrites s(0)=0, S=s(T), t(s(T))=T, tilde_pi_{s(t)}=pi_t, and the K(0)/K(T) identifications used after Gronwall."
      source := saldForwardKlEndpointScheduleSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.forwardKlEndpointScheduleContract",
        "sald.forward_kl.moving_target_dependency_chain",
        "sald.forward_kl.schedule_time_change",
        "sald.forward_kl.gronwall_side_conditions"
      ]
      reusedBy := ["thm:forward-KL", "cycle14 lower packet"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle30_derivative_side_upper"
      interface := "Upper-role lower packet for the derivative-side interface: mass conservation, KL differentiation, SALD and target integration by parts, slowed-target transport, Young 1/2 coefficients, and the time-change handoff."
      source := saldForwardKlDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle30ForwardKlUpperPacket",
        "SALD.forwardKlDerivativeCandidateContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.forwardKlMovingTargetDependencyContract",
        "sald.forward_kl.density_boundary_regular",
        "sald.forward_kl.schedule_time_change",
        "eq:SALD",
        "eq:FP-eq",
        "eq:LSI-KL-FI",
        "TransportVelocityContract"
      ]
      reusedBy := ["thm:forward-KL", "cycle30 lower derivative-side packet"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle30_derivative_side_middle"
      interface := "Middle source-to-Lean map for appendix.tex:168-208, selecting appendix.tex:168-185 density/boundary/FI identification as the first lower sub-slice and leaving target transport, LSI, time-change, DV, and Gronwall as separate obligations."
      source := saldForwardKlDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle30ForwardKlUpperPacket",
        "SALD.cycle30ForwardKlMiddleContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.forwardKlDensityBoundaryObligation",
        "sald.forward_kl.cycle30_derivative_side_upper",
        "sald.forward_kl.density_boundary_regular",
        "sald.forward_kl.kl_derivative",
        "eq:SALD",
        "eq:FP-eq",
        "KLContract",
        "FIContract",
        "FokkerPlanckContract"
      ]
      reusedBy := ["thm:forward-KL", "cycle30 lower density-boundary packet"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle30_density_boundary_lower"
      interface := "Lower scalar handoff for appendix.tex:168-185: substitute the supplied first-term identity firstTerm=-FI into the KL derivative display, while keeping mass conservation, Fokker-Planck, integration by parts, and FI identification as obligations."
      source := saldForwardKlDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle30ForwardKlMiddleContract",
        "SALD.forwardKlDerivativeSideConditionContract",
        "SALD.forwardKlDensityBoundaryObligation",
        "SALD.forwardKlFirstTermFisherSubstitutionScalar",
        "sald.forward_kl.cycle30_derivative_side_middle",
        "sald.forward_kl.density_boundary_regular",
        "eq:FP-eq",
        "KLContract",
        "FIContract",
        "FokkerPlanckContract"
      ]
      reusedBy := ["thm:forward-KL", "sald.forward_kl.kl_derivative"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle34_derivative_scalar"
      interface := "Proof-producing scalar derivative handoff for appendix.tex:168-228: combine the first-term Fisher substitution, target-side Young bound, supplied LSI half-Fisher comparison, and scalar inverse-schedule coefficient handoff while leaving analytic time-change inputs open."
      source := saldForwardKlDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle34ForwardKlDerivativeUpperPacket",
        "SALD.cycle34ForwardKlDerivativeMiddleContract",
        "SALD.forwardKlTargetTransportYoungBoundScalar",
        "SALD.forwardKlPostYoungDerivativeBoundScalar",
        "SALD.forwardKlPostYoungDerivativeBoundOfCauchyScalar",
        "SALD.forwardKlLsiDerivativeBoundScalar",
        "SALD.forwardKlLsiDerivativeBoundOfKlFiScalar",
        "SALD.forwardKlTimeChangedDerivativeBoundScalar",
        "SALD.forwardKlFirstTermFisherSubstitutionScalar",
        "sald.forward_kl.cycle34_target_young_lower",
        "sald.forward_kl.cycle30_density_boundary_lower",
        "sald.forward_kl.density_boundary_regular",
        "probability.lsi_to_kl_fi",
        "sald.forward_kl.schedule_time_change",
        "sald.forward_kl.kl_derivative"
      ]
      reusedBy := ["thm:forward-KL", "sald.forward_kl.kl_derivative"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle39_derivative_upper"
      interface := "Upper proof-closure packet for appendix.tex:168-228: use the compiled pre-DV scalar pipeline and assign lower work to the remaining density/boundary and schedule-time-change inputs before any ledger expansion or EM interpolation work."
      source := saldForwardKlDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle39ForwardKlDerivativeUpperPacket",
        "SALD.cycle39ForwardKlDerivativeMiddleContract",
        "SALD.cycle39ForwardKlDerivativeUpperObligation",
        "SALD.forwardKlPreDvDerivativeBoundScalar",
        "SALD.forwardKlPreDvDerivativeBoundOfProductScalar",
        "SALD.forwardKlPreDvDerivativeBoundOfVelocityScalingScalar",
        "SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar",
        "SALD.forwardKlInverseScheduleDerivativeScalar",
        "SALD.forwardKlTimeChangeSquareCoefficientRewriteOfProductScalar",
        "SALD.forwardKlVelocitySquareScalingScalar",
        "SALD.forwardKlTimeChangedDerivativeBoundOfProductScalar",
        "SALD.forwardKlFirstTermFisherSubstitutionScalar",
        "SALD.forwardKlTargetTransportYoungBoundScalar",
        "SALD.forwardKlPostYoungDerivativeBoundScalar",
        "SALD.forwardKlPostYoungDerivativeBoundOfCauchyScalar",
        "SALD.forwardKlLsiDerivativeBoundScalar",
        "SALD.forwardKlTimeChangedDerivativeBoundScalar",
        "sald.forward_kl.density_boundary_regular",
        "sald.forward_kl.schedule_time_change",
        "probability.lsi_to_kl_fi",
        "sald.forward_kl.kl_derivative"
      ]
      reusedBy := ["thm:forward-KL", "sald.forward_kl.kl_derivative"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle39_derivative_middle"
      interface := "Middle source-to-Lean map for appendix.tex:191-228: expose source-shaped inverse-schedule product and slowed-velocity norm-square scalar lemmas feeding the pre-DV derivative pipeline."
      source := saldForwardKlDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle39ForwardKlDerivativeMiddleContract",
        "SALD.cycle39ForwardKlDerivativeMiddleObligation",
        "SALD.forwardKlInverseScheduleDerivativeScalar",
        "SALD.forwardKlTimeChangeSquareCoefficientRewriteOfProductScalar",
        "SALD.forwardKlVelocitySquareScalingScalar",
        "SALD.forwardKlTimeChangedDerivativeBoundOfProductScalar",
        "SALD.forwardKlPreDvDerivativeBoundOfProductScalar",
        "SALD.forwardKlPreDvDerivativeBoundOfVelocityScalingScalar",
        "SALD.forwardKlLsiDerivativeBoundOfKlFiScalar",
        "SALD.forwardKlPreDvDerivativeBoundOfKlFiVelocityScalingScalar",
        "SALD.forwardKlPreDvDerivativeBoundScalar",
        "sald.forward_kl.cycle39_derivative_upper",
        "sald.forward_kl.schedule_time_change",
        "sald.forward_kl.density_boundary_regular",
        "probability.lsi_to_kl_fi",
        "sald.forward_kl.kl_derivative"
      ]
      reusedBy := ["thm:forward-KL", "sald.forward_kl.kl_derivative", "sald.forward_kl.schedule_time_change"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.coefficient_chain_audit"
      interface := "Preserve the source LSI, DV, and Gronwall coefficient flow from appendix lines 210-252, including the source-line ledger, scalar side conditions, and final exponent split in the theorem statement."
      source := saldForwardKlDependencyChainSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "eq:LSI-KL-FI",
        "def:alpha-complexity",
        "lem:dv_variation",
        "lem:gronwall",
        "sald.forward_kl.kl_derivative",
        "sald.forward_kl.dv_energy_bound",
        "sald.forward_kl.gronwall_application",
        "sald.forward_kl.gronwall_side_conditions"
      ]
      reusedBy := ["thm:forward-KL", "thm:forward-KL-discrete"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.gronwall_side_conditions"
      interface := "Expose endpoint K(0)/K(T) identifications, coefficient regularity, exponent splitting, and residual-exponent sign facts for the final Gronwall display."
      source := saldForwardKlGronwallSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle18ForwardKlUpperPacket",
        "SALD.cycle18ForwardKlMiddleContract",
        "SALD.cycle22ForwardKlUpperPacket",
        "SALD.cycle22ForwardKlMiddleContract",
        "sald.forward_kl.moving_target_dependency_chain",
        "sald.forward_kl.endpoint_schedule_identities",
        "sald.forward_kl.schedule_time_change",
        "sald.forward_kl.kl_derivative",
        "sald.forward_kl.dv_energy_bound",
        "sald.gronwall.integrating_factor",
        "sald.gronwall.exponent_rewrite",
        "SALD.gronwallNegIntegralRewriteScalar",
        "SALD.gronwallExpProductRewriteScalar",
        "SALD.gronwallExpProductRewriteIntervalIntegral",
        "SALD.gronwallExpProductRewriteIntegralCongr",
        "SALD.forwardKlGronwallCoeffIntervalIntegrable",
        "SALD.forwardKlGronwallCoeffAdjacentIntervalIntegrable",
        "SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces",
        "SALD.forwardKlGronwallCoeffIntegralSub",
        "SALD.forwardKlGronwallInitialExponentSplitScalar",
        "SALD.forwardKlGronwallInitialExponentSplitOfPieces",
        "SALD.forwardKlGronwallResidualExponentDropScalar",
        "SALD.forwardKlGronwallResidualExponentDropIntegral"
      ]
      reusedBy := ["thm:forward-KL"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.alpha_complexity"
      interface := "Define E_alpha(pi_t,v_t) and A_alpha(pi,v); expose finite log-mgf obligations for alpha in (0, alpha0]."
      source := saldAlphaComplexitySource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := ["exponential moment vocabulary"]
      reusedBy := ["thm:forward-KL", "thm:forward-KL-discrete", "thm:general-moving-target-SALD"]
      status := ProofStatus.contractOnly
    },
    {
      id := "ASTIS.SALD.forward_KL.dv_alpha_mgf_monotonicity"
      interface := "Derive the theorem-specific finite log-mgf at alpha from the source alpha0-complexity assumption for Z=alpha*||v_t||^2 before applying DV."
      source := saldForwardKlDvEnergySource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "def:alpha-complexity",
        "SALD.saldDvFiniteLogMgfContract",
        "sald.dv_variation.finite_log_mgf_interface"
      ]
      reusedBy := ["thm:forward-KL", "sald.forward_kl.dv_finite_log_mgf_witness"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.cycle26_middle_dv_witness"
      interface := "Middle source-dependency map for the DV witness: common-space/absolute-continuity, measurability of Z=alpha*||v_t||^2, alpha0-to-alpha finite log-mgf, and positive-alpha division."
      source := saldForwardKlDvEnergySource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle26ForwardKlUpperPacket",
        "SALD.cycle26ForwardKlMiddleContract",
        "SALD.forwardKlDvFiniteLogMgfWitnessContract",
        "SALD.forwardKlDvAlphaMonotonicityContract",
        "SALD.saldDvFiniteLogMgfContract",
        "probability.dv_variational_formula",
        "sald.dv_variation.finite_log_mgf_interface",
        "sald.forward_kl.dv_alpha_mgf_monotonicity",
        "SALD.forwardKlDvPositiveAlphaScalingScalar",
        "SALD.forwardKlDvPositiveAlphaCoefficientScalar",
        "sald.forward_kl.moving_target_dependency_chain"
      ]
      reusedBy := ["sald.forward_kl.dv_finite_log_mgf_witness", "thm:forward-KL"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.derivative"
      interface := "Derive the source differential inequality before DV: dK/dt <= -dot{s}*C_LSI*K + (1/2)*dot{s}^(-1)*||v_t||^2_{L2(rho)}."
      source := saldForwardKlDerivativeSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle30ForwardKlUpperPacket",
        "SALD.cycle30ForwardKlMiddleContract",
          "SALD.cycle39ForwardKlDerivativeUpperPacket",
          "SALD.cycle39ForwardKlDerivativeMiddleContract",
          "sald.forward_kl.cycle30_derivative_side_upper",
          "sald.forward_kl.cycle30_derivative_side_middle",
          "sald.forward_kl.cycle30_density_boundary_lower",
          "sald.forward_kl.cycle39_derivative_upper",
          "sald.forward_kl.cycle39_derivative_middle",
          "eq:SALD",
          "eq:FP-eq",
          "eq:LSI-KL-FI",
          "TransportVelocityContract",
          "SALD.forwardKlFirstTermFisherSubstitutionScalar",
          "SALD.forwardKlPostYoungDerivativeBoundScalar",
          "SALD.forwardKlLsiDerivativeBoundScalar",
          "sald.forward_kl.cycle34_derivative_scalar",
          "SALD.forwardKlPreDvDerivativeBoundScalar",
          "SALD.forwardKlPreDvDerivativeBoundOfProductScalar",
          "SALD.forwardKlPreDvDerivativeBoundOfVelocityScalingScalar",
          "SALD.forwardKlInverseScheduleDerivativeScalar",
          "SALD.forwardKlVelocitySquareScalingScalar",
          "sald.forward_kl.density_boundary_regular",
          "sald.forward_kl.schedule_time_change"
        ]
      reusedBy := ["thm:forward-KL", "thm:forward-KL-discrete"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.dv_finite_log_mgf_witness"
      interface := "Provide the theorem-specific DV finite-log-mgf and common-space witness for Z=alpha*||v_t||^2 from the alpha0-complexity assumption before the DV-energy inequality is used."
      source := saldForwardKlDvEnergySource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.cycle26ForwardKlUpperPacket",
        "SALD.cycle26ForwardKlMiddleContract",
        "ASTIS.SALD.forward_KL.cycle26_middle_dv_witness",
        "sald.forward_kl.cycle26_dv_witness_middle",
        "lem:dv_variation",
        "def:alpha-complexity",
        "SALD.saldDvFiniteLogMgfContract",
        "sald.dv_variation.finite_log_mgf_interface",
        "sald.forward_kl.dv_alpha_mgf_monotonicity",
        "SALD.forwardKlDvPositiveAlphaScalingScalar",
        "SALD.forwardKlDvPositiveAlphaCoefficientScalar",
        "sald.forward_kl.cycle26_dv_positive_alpha_lower",
        "sald.forward_kl.moving_target_dependency_chain"
      ]
      reusedBy := ["thm:forward-KL", "thm:forward-KL-discrete DV pattern"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.dv_energy"
      interface := "Instantiate DV with Z=alpha*||v_t||^2 and rewrite the log-mgf term as E_alpha(pi_t,v_t)."
      source := saldForwardKlDvEnergySource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "lem:dv_variation",
        "def:alpha-complexity",
        "SALD.cycle26ForwardKlMiddleContract",
        "sald.forward_kl.cycle26_dv_witness_middle",
        "sald.forward_kl.dv_alpha_mgf_monotonicity",
        "sald.forward_kl.dv_finite_log_mgf_witness",
        "SALD.forwardKlDvPositiveAlphaScalingScalar",
        "SALD.forwardKlDvPositiveAlphaCoefficientScalar",
        "sald.forward_kl.cycle26_dv_positive_alpha_lower"
      ]
      reusedBy := ["thm:forward-KL", "thm:forward-KL-discrete", "thm:general-moving-target-SALD"]
      status := ProofStatus.obligation
    },
    {
      id := "ASTIS.SALD.forward_KL.gronwall_application"
      interface := "Apply lem:gronwall with the paper's a(t), b(t), then split the exponent exactly as in the theorem statement."
      source := saldForwardKlGronwallSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := ["lem:gronwall", "sald.forward_kl.kl_derivative", "sald.forward_kl.dv_energy_bound"]
      reusedBy := ["thm:forward-KL", "thm:forward-KL-discrete"]
      status := ProofStatus.obligation
    }
  ]

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