AutoSamplingTheory.SALD.cycle12GeneralVaSaldMiddleContract

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 cycle12GeneralVaSaldMiddleContract :
    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.

Map the cycle-focus guided/general VA-SALD proof route from the guided residual identity through the continuous general theorem, the unified c_t<-u_t specialization, and the discrete general theorem while keeping all theorem statements and coefficients 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 by differentiating Z_t, differentiating pi_t=Z_t^(-1)*p_t*exp(-f_t), canceling div(p_t*u_t), and centering g_t.
2. main_body.tex:359-368 uses the residual identity and div(pi_t*w_t)=pi_t*(g_t-E_pi_t[g_t]) to state that u_t+w_t is a transport velocity for pi_t.
3. appendix.tex:765-884 derives the continuous general VA-SALD sigma-weighted KL differential inequality with residual m_t=v_t-c_t before DV.
4. appendix.tex:885-934 applies DV to Z=alpha*||m_t||^2 and then Gronwall with the sigma-weighted a(t), b(t).
5. appendix.tex:936-951 gives the pure-contraction c_t=v_t case and the one-line unified theorem proof by setting c_t<-u_t.
6. appendix.tex:1354-1600 repeats the route under the general EM interpolation, splits delta_pi^VA and dot t(s)*m_t, applies the residual DV witness, changes to t, and applies Gronwall.
7. appendix.tex:1603 specializes the discrete general theorem to discrete VA-SALD by replacing c with u.

leanStepMap : List String (explicit)

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

Ordered data items

1. Guided residual normalization and centering are tracked by SALD.guidedResidualIdentityContract, sald.guided_path_residual.normalizer_derivative, and sald.guided_path_residual.identity.
2. The continuous derivative route is tracked by SALD.generalMovingTargetDerivativeCandidateContract and sald.general_moving_target.kl_derivative.
3. The continuous residual DV step is split between SALD.generalMovingTargetDvFiniteLogMgfWitnessContract, SALD.generalMovingTargetDvPositiveAlphaScalingContract, SALD.generalMovingTargetDvEnergyCandidateContract, 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.
4. The continuous Gronwall and pure-contraction bookkeeping is tracked by SALD.generalMovingTargetGronwallInstantiationContract, SALD.generalMovingTargetGronwallSideConditionContract, sald.general_moving_target.gronwall_application, sald.general_moving_target.gronwall_side_conditions, and sald.general_moving_target.pure_contraction.
5. The unified theorem bridge is tracked by SALD.unifiedForwardKlSpecializationContract and sald.unified_forward_kl.specialization.
6. The discrete route is tracked by SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract, SALD.generalMovingTargetDiscreteGronwallSideConditionContract, and the matching sald.general_moving_target_discrete.* obligations.
7. The discrete guided specialization is tracked by sald.general_moving_target_discrete.unified_specialization.

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; residual finite-log-mgf witnesses expose theorem-specific side conditions before each DV-energy obligation.
2. eq:LSI-KL-FI remains an obligation through probability.lsi_to_kl_fi.
3. lem:gronwall remains a local real-analysis obligation through sald.gronwall.integrating_factor and the Gronwall side-condition contracts.
4. lem:frozen_delta_cross_lip is an internal appendix lemma whose proof still depends on local EM estimates and source-cited DV substeps.

obligations : List String (explicit)

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

Ordered data items

1. sald.guided_path_residual.normalizer_derivative
2. sald.guided_path_residual.identity
3. sald.general_moving_target.kl_derivative
4. sald.general_moving_target.dv_finite_log_mgf_witness
5. sald.general_moving_target.dv_positive_alpha_scaling
6. sald.general_moving_target.dv_m_energy
7. sald.general_moving_target.gronwall_application
8. sald.general_moving_target.gronwall_side_conditions
9. sald.general_moving_target.pure_contraction
10. sald.unified_forward_kl.specialization
11. sald.general_moving_target_discrete.em_interpolation_fp
12. sald.general_moving_target_discrete.derivative_side_conditions
13. sald.general_moving_target_discrete.kl_derivative
14. sald.general_moving_target_discrete.dv_finite_log_mgf_witness
15. sald.general_moving_target_discrete.dv_m_energy
16. sald.general_moving_target_discrete.gronwall_application
17. sald.general_moving_target_discrete.gronwall_side_conditions
18. sald.general_moving_target_discrete.unified_specialization

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly one existing backend obligation from this map; preferred next targets are sald.unified_forward_kl.specialization or sald.general_moving_target_discrete.derivative_side_conditions.
2. If working on the unified specialization, prove only the transport-velocity bridge from prop:guided_path_residual plus eq:poisson-eq to v_t=u_t+w_t and m_t=w_t.
3. If working on the discrete derivative side conditions, preserve the two sigma_eta^2/8 Young splits, the residual coefficient 2*sigma_eta^(-2)*dot t(s)^2 before time change, and the frozen-delta Gamma/Delta coefficients.
4. Do not add correction-field existence, density regularity, finite-log-mgf, endpoint, or schedule assumptions silently to any theorem statement.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. The guided residual, general continuous, unified, and discrete theorem contracts all remain contract-only with named obligations.
2. The residual DV witness obligations remain before the residual DV-energy obligations in both continuous and discrete DAGs.
3. The unified theorem uses only the source specialization c_t<-u_t and does not introduce a direct VA-SALD proof route.
4. The discrete theorem display keeps the doubled residual coefficient and the Gamma/Delta terms from appendix.tex:1316-1347.
5. No analytic dependency is marked formalized and no fake proof closure 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 cycle12GeneralVaSaldMiddleContract :
    GeneralVaSaldGuidedPathMiddleContract where
  guidedResidualSource := saldGuidedResidualSource
  generalContinuousSource := saldGeneralMovingTargetSource
  unifiedSource := saldUnifiedForwardKlSource
  discreteSource := saldGeneralMovingTargetDiscreteSource
  objective := "Map the cycle-focus guided/general VA-SALD proof route from the guided residual identity through the continuous general theorem, the unified c_t<-u_t specialization, and the discrete general theorem while keeping all theorem statements and coefficients unchanged."
  sourceStepMap := [
    "appendix.tex:619-704 proves prop:guided_path_residual by differentiating Z_t, differentiating pi_t=Z_t^(-1)*p_t*exp(-f_t), canceling div(p_t*u_t), and centering g_t.",
    "main_body.tex:359-368 uses the residual identity and div(pi_t*w_t)=pi_t*(g_t-E_pi_t[g_t]) to state that u_t+w_t is a transport velocity for pi_t.",
    "appendix.tex:765-884 derives the continuous general VA-SALD sigma-weighted KL differential inequality with residual m_t=v_t-c_t before DV.",
    "appendix.tex:885-934 applies DV to Z=alpha*||m_t||^2 and then Gronwall with the sigma-weighted a(t), b(t).",
    "appendix.tex:936-951 gives the pure-contraction c_t=v_t case and the one-line unified theorem proof by setting c_t<-u_t.",
    "appendix.tex:1354-1600 repeats the route under the general EM interpolation, splits delta_pi^VA and dot t(s)*m_t, applies the residual DV witness, changes to t, and applies Gronwall.",
    "appendix.tex:1603 specializes the discrete general theorem to discrete VA-SALD by replacing c with u."
  ]
  leanStepMap := [
    "Guided residual normalization and centering are tracked by SALD.guidedResidualIdentityContract, sald.guided_path_residual.normalizer_derivative, and sald.guided_path_residual.identity.",
    "The continuous derivative route is tracked by SALD.generalMovingTargetDerivativeCandidateContract and sald.general_moving_target.kl_derivative.",
    "The continuous residual DV step is split between SALD.generalMovingTargetDvFiniteLogMgfWitnessContract, SALD.generalMovingTargetDvPositiveAlphaScalingContract, SALD.generalMovingTargetDvEnergyCandidateContract, 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.",
    "The continuous Gronwall and pure-contraction bookkeeping is tracked by SALD.generalMovingTargetGronwallInstantiationContract, SALD.generalMovingTargetGronwallSideConditionContract, sald.general_moving_target.gronwall_application, sald.general_moving_target.gronwall_side_conditions, and sald.general_moving_target.pure_contraction.",
    "The unified theorem bridge is tracked by SALD.unifiedForwardKlSpecializationContract and sald.unified_forward_kl.specialization.",
    "The discrete route is tracked by SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract, SALD.generalMovingTargetDiscreteGronwallSideConditionContract, and the matching sald.general_moving_target_discrete.* obligations.",
    "The discrete guided specialization is tracked by sald.general_moving_target_discrete.unified_specialization."
  ]
  citedResultInterfaces := [
    "lem:dv_variation remains source-cited; residual finite-log-mgf witnesses expose theorem-specific side conditions before each DV-energy obligation.",
    "eq:LSI-KL-FI remains an obligation through probability.lsi_to_kl_fi.",
    "lem:gronwall remains a local real-analysis obligation through sald.gronwall.integrating_factor and the Gronwall side-condition contracts.",
    "lem:frozen_delta_cross_lip is an internal appendix lemma whose proof still depends on local EM estimates and source-cited DV substeps."
  ]
  obligations := [
    "sald.guided_path_residual.normalizer_derivative",
    "sald.guided_path_residual.identity",
    "sald.general_moving_target.kl_derivative",
    "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",
    "sald.general_moving_target_discrete.derivative_side_conditions",
    "sald.general_moving_target_discrete.kl_derivative",
    "sald.general_moving_target_discrete.dv_finite_log_mgf_witness",
    "sald.general_moving_target_discrete.dv_m_energy",
    "sald.general_moving_target_discrete.gronwall_application",
    "sald.general_moving_target_discrete.gronwall_side_conditions",
    "sald.general_moving_target_discrete.unified_specialization"
  ]
  lowerPacket := [
    "Target exactly one existing backend obligation from this map; preferred next targets are sald.unified_forward_kl.specialization or sald.general_moving_target_discrete.derivative_side_conditions.",
    "If working on the unified specialization, prove only the transport-velocity bridge from prop:guided_path_residual plus eq:poisson-eq to v_t=u_t+w_t and m_t=w_t.",
    "If working on the discrete derivative side conditions, preserve the two sigma_eta^2/8 Young splits, the residual coefficient 2*sigma_eta^(-2)*dot t(s)^2 before time change, and the frozen-delta Gamma/Delta coefficients.",
    "Do not add correction-field existence, density regularity, finite-log-mgf, endpoint, or schedule assumptions silently to any theorem statement."
  ]
  reviewerChecklist := [
    "The guided residual, general continuous, unified, and discrete theorem contracts all remain contract-only with named obligations.",
    "The residual DV witness obligations remain before the residual DV-energy obligations in both continuous and discrete DAGs.",
    "The unified theorem uses only the source specialization c_t<-u_t and does not introduce a direct VA-SALD proof route.",
    "The discrete theorem display keeps the doubled residual coefficient and the Gamma/Delta terms from appendix.tex:1316-1347.",
    "No analytic dependency is marked formalized and no fake proof closure is introduced."
  ]
  status := ProofStatus.obligation