AutoSamplingTheory.SALD.cycle47GuidedGeneralSkeletonMiddleContract

Data definition / provenance and workflow record

Meaning and type

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

def cycle47GuidedGeneralSkeletonMiddleContract :
    GeneralVaSaldGuidedPathMiddleContract

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.

guidedResidualSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldGuidedResidualSource — audited data reference, not expanded and not a compiled dependency edge

generalContinuousSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldGeneralMovingTargetSource — audited data reference, not expanded and not a compiled dependency edge

unifiedSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldUnifiedForwardKlSource — audited data reference, not expanded and not a compiled dependency edge

discreteSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteSource — audited data reference, not expanded and not a compiled dependency edge

objective : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

Middle source-to-Lean audit for main skeleton sprint 4: verify that cycle47GuidedGeneralSkeletonObligation consumes the guided residual identity, continuous general KL derivative, LSI/KL/FI, residual DV, Gronwall, and pure-contraction interfaces in the exact appendix.tex:619-951 order, while prop:guided_path_residual and thm:general-moving-target-SALD remain unchanged.

sourceStepMap : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. appendix.tex:619-704 proves prop:guided_path_residual: compute dot Z_t, use partial_t p_t=-div(p_t*u_t), integrate by parts, differentiate pi_t=Z_t^(-1)*p_t*exp(-f_t), cancel divergence terms, substitute dot Z_t/Z_t, and conclude the centered mean-zero residual.
2. appendix.tex:724-744 states thm:general-moving-target-SALD with dynamics dX_s=(dot t(s)*c_{t(s)}+(sigma_{t(s)}^2/2)*nabla log pi_{t(s)})ds+sigma_{t(s)}dW_s, residual m_t=v_t-c_t, finite E_alpha0(pi_t,m_t), alpha in (0,alpha0], and the sigma-weighted KL bound.
3. appendix.tex:765-835 differentiates KL(rho_s||pi_{t(s)}), inserts the general moving-target Fokker-Planck equation, and evaluates the two integration-by-parts terms.
4. appendix.tex:835-864 combines c_t and v_t into the residual m_t=v_t-c_t and applies Young with epsilon=2*dot{t}(s)/sigma_{t(s)}^2 to get the pre-LSI inequality.
5. appendix.tex:865-884 changes from s to t and applies eq:LSI-KL-FI to get the pre-DV K'(t) inequality with coefficient sigma_t^(-2)*dot{s}(t)^(-1) on the residual energy.
6. appendix.tex:885-907 applies lem:dv_variation with Z=alpha*||m_t||^2, rewrites the log-mgf as E_alpha(pi_t,m_t), and forms the scalar differential inequality.
7. appendix.tex:909-934 applies lem:gronwall with a(t)=(sigma_t^2/2)*dot{s}(t)*C_LSI(t)-sigma_t^(-2)*dot{s}(t)^(-1)*alpha^(-1) and b(t)=sigma_t^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t), then matches the theorem display.
8. appendix.tex:936-945 specializes c_t=v_t so m_t=0 and E_alpha(pi_t,m_t)=0, yielding the pure contraction display; appendix.tex:949-951 is downstream reuse by thm:unified-forward-KL.

leanStepMap : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. Route appendix.tex:619-704 through SALD.guidedResidualIdentityContract, sald.guided_path_residual.normalizer_derivative, and sald.guided_path_residual.identity.
2. Keep SALD.generalMovingTargetStatementContract and SALD.generalVaSaldContract unchanged; the middle contract only audits the route wrapper.
3. Route appendix.tex:765-884 through SALD.generalMovingTargetDerivativeCandidateContract, sald.general_moving_target.kl_derivative, SALD.saldLsiKlFiDensityTestContract, probability.lsi_to_kl_fi, and sald.forward_kl.schedule_time_change.
4. Route appendix.tex:885-907 through SALD.generalMovingTargetDvFiniteLogMgfWitnessContract, SALD.generalMovingTargetDvPositiveAlphaScalingContract, sald.general_moving_target.dv_finite_log_mgf_witness, sald.general_moving_target.dv_positive_alpha_scaling, and sald.general_moving_target.dv_m_energy.
5. Route appendix.tex:909-945 through SALD.generalMovingTargetGronwallInstantiationContract, SALD.generalMovingTargetGronwallSideConditionContract, sald.general_moving_target.gronwall_application, sald.general_moving_target.gronwall_side_conditions, and sald.general_moving_target.pure_contraction.
6. Keep SALD.unifiedForwardKlSpecializationContract visible only as downstream reuse of appendix.tex:949-951; this cycle does not introduce a direct VA-SALD proof.
7. Select the next lower target as sald.general_moving_target.kl_derivative, because it is the theorem-level backend that feeds LSI, residual DV, and Gronwall after the skeleton route is wired.

citedResultInterfaces : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. lem:dv_variation remains source-cited through the residual finite-log-mgf witness; no entropy-duality theorem is imported or marked formalized.
2. lem:gronwall remains the endpoint-safe real-analysis obligation with coefficient regularity, endpoint rewrites, exponent splitting, and residual-exponent side conditions.
3. eq:LSI-KL-FI remains the density-test and Fisher-chain obligation; compiled scalar and RN-density helpers are dependencies only.
4. The continuous general Fokker-Planck/KL derivative remains a local SDE/measure-analysis obligation; it is not promoted by this middle audit.
5. The EM interpolation Fokker-Planck backend remains checked as a downstream slow interface for the later discrete general theorem, not as a continuous theorem assumption.

obligations : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. sald.guided_general.cycle47_theorem_skeleton_route
2. sald.guided_general.cycle47_middle_route_audit
3. sald.guided_path_residual.normalizer_derivative
4. sald.guided_path_residual.identity
5. sald.general_moving_target.kl_derivative
6. probability.lsi_to_kl_fi
7. sald.general_moving_target.dv_finite_log_mgf_witness
8. sald.general_moving_target.dv_positive_alpha_scaling
9. sald.general_moving_target.dv_m_energy
10. sald.general_moving_target.gronwall_application
11. sald.general_moving_target.gronwall_side_conditions
12. sald.general_moving_target.pure_contraction
13. sald.unified_forward_kl.specialization
14. sald.general_moving_target_discrete.em_interpolation_fp

lowerPacket : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. Target exactly SALD.generalMovingTargetDerivativeCandidateContract / SALD.generalMovingTargetDerivativeObligation / sald.general_moving_target.kl_derivative.
2. First lower sub-slice: expose the density/law, Fokker-Planck, mass conservation, and integration-by-parts interfaces for appendix.tex:765-812 without changing the theorem statement.
3. Second lower sub-slice: identify the target transport velocity v_t, combine the c_t and v_t terms into m_t=v_t-c_t, and preserve the Young coefficient epsilon=2*dot{t}(s)/sigma_{t(s)}^2 from appendix.tex:835-864.
4. Leave LSI density-test, residual DV finite-log-mgf, Gronwall endpoint/exponent side conditions, guided normalizer differentiation, and pure-contraction alpha-complexity as separate obligations unless exact compiled proofs are added.
5. Do not work on the discrete general theorem in this lower packet; it remains downstream reuse through the existing EM interpolation and discrete side-condition interfaces.

reviewerChecklist : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. Every source step from appendix.tex:619-951 is classified as Lean contract, cited result, or named obligation.
2. SALD.guidedResidualContract and SALD.generalVaSaldContract list SALD.cycle47GuidedGeneralSkeletonMiddleObligation while preserving contractOnly status.
3. SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle47_middle_route_audit after the cycle-47 route wrapper and before lower backend nodes.
4. SALD.saldDependenciesForLabel "prop:guided_path_residual" and "thm:general-moving-target-SALD" include SALD.cycle47GuidedGeneralSkeletonMiddleContract, SALD.cycle47GuidedGeneralSkeletonMiddleObligation, and sald.guided_general.cycle47_middle_route_audit.
5. No analytic backend status is promoted, no theorem statement or source constant changes, and no alternate proof route is introduced.

status : AutoSamplingTheory.ProofStatus (explicit)

Stored workflow tag; honor the exact default but do not infer mathematical certification.

AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

def cycle47GuidedGeneralSkeletonMiddleContract :
    GeneralVaSaldGuidedPathMiddleContract where
  guidedResidualSource := saldGuidedResidualSource
  generalContinuousSource := saldGeneralMovingTargetSource
  unifiedSource := saldUnifiedForwardKlSource
  discreteSource := saldGeneralMovingTargetDiscreteSource
  objective := "Middle source-to-Lean audit for main skeleton sprint 4: verify that cycle47GuidedGeneralSkeletonObligation consumes the guided residual identity, continuous general KL derivative, LSI/KL/FI, residual DV, Gronwall, and pure-contraction interfaces in the exact appendix.tex:619-951 order, while prop:guided_path_residual and thm:general-moving-target-SALD remain unchanged."
  sourceStepMap := [
    "appendix.tex:619-704 proves prop:guided_path_residual: compute dot Z_t, use partial_t p_t=-div(p_t*u_t), integrate by parts, differentiate pi_t=Z_t^(-1)*p_t*exp(-f_t), cancel divergence terms, substitute dot Z_t/Z_t, and conclude the centered mean-zero residual.",
    "appendix.tex:724-744 states thm:general-moving-target-SALD with dynamics dX_s=(dot t(s)*c_{t(s)}+(sigma_{t(s)}^2/2)*nabla log pi_{t(s)})ds+sigma_{t(s)}dW_s, residual m_t=v_t-c_t, finite E_alpha0(pi_t,m_t), alpha in (0,alpha0], and the sigma-weighted KL bound.",
    "appendix.tex:765-835 differentiates KL(rho_s||pi_{t(s)}), inserts the general moving-target Fokker-Planck equation, and evaluates the two integration-by-parts terms.",
    "appendix.tex:835-864 combines c_t and v_t into the residual m_t=v_t-c_t and applies Young with epsilon=2*dot{t}(s)/sigma_{t(s)}^2 to get the pre-LSI inequality.",
    "appendix.tex:865-884 changes from s to t and applies eq:LSI-KL-FI to get the pre-DV K'(t) inequality with coefficient sigma_t^(-2)*dot{s}(t)^(-1) on the residual energy.",
    "appendix.tex:885-907 applies lem:dv_variation with Z=alpha*||m_t||^2, rewrites the log-mgf as E_alpha(pi_t,m_t), and forms the scalar differential inequality.",
    "appendix.tex:909-934 applies lem:gronwall with a(t)=(sigma_t^2/2)*dot{s}(t)*C_LSI(t)-sigma_t^(-2)*dot{s}(t)^(-1)*alpha^(-1) and b(t)=sigma_t^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t), then matches the theorem display.",
    "appendix.tex:936-945 specializes c_t=v_t so m_t=0 and E_alpha(pi_t,m_t)=0, yielding the pure contraction display; appendix.tex:949-951 is downstream reuse by thm:unified-forward-KL."
  ]
  leanStepMap := [
    "Route appendix.tex:619-704 through SALD.guidedResidualIdentityContract, sald.guided_path_residual.normalizer_derivative, and sald.guided_path_residual.identity.",
    "Keep SALD.generalMovingTargetStatementContract and SALD.generalVaSaldContract unchanged; the middle contract only audits the route wrapper.",
    "Route appendix.tex:765-884 through SALD.generalMovingTargetDerivativeCandidateContract, sald.general_moving_target.kl_derivative, SALD.saldLsiKlFiDensityTestContract, probability.lsi_to_kl_fi, and sald.forward_kl.schedule_time_change.",
    "Route appendix.tex:885-907 through SALD.generalMovingTargetDvFiniteLogMgfWitnessContract, SALD.generalMovingTargetDvPositiveAlphaScalingContract, sald.general_moving_target.dv_finite_log_mgf_witness, sald.general_moving_target.dv_positive_alpha_scaling, and sald.general_moving_target.dv_m_energy.",
    "Route appendix.tex:909-945 through SALD.generalMovingTargetGronwallInstantiationContract, SALD.generalMovingTargetGronwallSideConditionContract, sald.general_moving_target.gronwall_application, sald.general_moving_target.gronwall_side_conditions, and sald.general_moving_target.pure_contraction.",
    "Keep SALD.unifiedForwardKlSpecializationContract visible only as downstream reuse of appendix.tex:949-951; this cycle does not introduce a direct VA-SALD proof.",
    "Select the next lower target as sald.general_moving_target.kl_derivative, because it is the theorem-level backend that feeds LSI, residual DV, and Gronwall after the skeleton route is wired."
  ]
  citedResultInterfaces := [
    "lem:dv_variation remains source-cited through the residual finite-log-mgf witness; no entropy-duality theorem is imported or marked formalized.",
    "lem:gronwall remains the endpoint-safe real-analysis obligation with coefficient regularity, endpoint rewrites, exponent splitting, and residual-exponent side conditions.",
    "eq:LSI-KL-FI remains the density-test and Fisher-chain obligation; compiled scalar and RN-density helpers are dependencies only.",
    "The continuous general Fokker-Planck/KL derivative remains a local SDE/measure-analysis obligation; it is not promoted by this middle audit.",
    "The EM interpolation Fokker-Planck backend remains checked as a downstream slow interface for the later discrete general theorem, not as a continuous theorem assumption."
  ]
  obligations := [
    "sald.guided_general.cycle47_theorem_skeleton_route",
    "sald.guided_general.cycle47_middle_route_audit",
    "sald.guided_path_residual.normalizer_derivative",
    "sald.guided_path_residual.identity",
    "sald.general_moving_target.kl_derivative",
    "probability.lsi_to_kl_fi",
    "sald.general_moving_target.dv_finite_log_mgf_witness",
    "sald.general_moving_target.dv_positive_alpha_scaling",
    "sald.general_moving_target.dv_m_energy",
    "sald.general_moving_target.gronwall_application",
    "sald.general_moving_target.gronwall_side_conditions",
    "sald.general_moving_target.pure_contraction",
    "sald.unified_forward_kl.specialization",
    "sald.general_moving_target_discrete.em_interpolation_fp"
  ]
  lowerPacket := [
    "Target exactly SALD.generalMovingTargetDerivativeCandidateContract / SALD.generalMovingTargetDerivativeObligation / sald.general_moving_target.kl_derivative.",
    "First lower sub-slice: expose the density/law, Fokker-Planck, mass conservation, and integration-by-parts interfaces for appendix.tex:765-812 without changing the theorem statement.",
    "Second lower sub-slice: identify the target transport velocity v_t, combine the c_t and v_t terms into m_t=v_t-c_t, and preserve the Young coefficient epsilon=2*dot{t}(s)/sigma_{t(s)}^2 from appendix.tex:835-864.",
    "Leave LSI density-test, residual DV finite-log-mgf, Gronwall endpoint/exponent side conditions, guided normalizer differentiation, and pure-contraction alpha-complexity as separate obligations unless exact compiled proofs are added.",
    "Do not work on the discrete general theorem in this lower packet; it remains downstream reuse through the existing EM interpolation and discrete side-condition interfaces."
  ]
  reviewerChecklist := [
    "Every source step from appendix.tex:619-951 is classified as Lean contract, cited result, or named obligation.",
    "SALD.guidedResidualContract and SALD.generalVaSaldContract list SALD.cycle47GuidedGeneralSkeletonMiddleObligation while preserving contractOnly status.",
    "SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle47_middle_route_audit after the cycle-47 route wrapper and before lower backend nodes.",
    "SALD.saldDependenciesForLabel \"prop:guided_path_residual\" and \"thm:general-moving-target-SALD\" include SALD.cycle47GuidedGeneralSkeletonMiddleContract, SALD.cycle47GuidedGeneralSkeletonMiddleObligation, and sald.guided_general.cycle47_middle_route_audit.",
    "No analytic backend status is promoted, no theorem statement or source constant changes, and no alternate proof route is introduced."
  ]
  status := ProofStatus.obligation

/-- Cycle-47 middle obligation tying the guided/general route audit to lower
work. -/