AutoSamplingTheory.SALD.cycle52GuidedGeneralSkeletonMiddleContract

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

Cycle 52 middle: verify the post-upper guided/general route against appendix.tex:619-951, keep prop:guided_path_residual and thm:general-moving-target-SALD unchanged, and select sald.general_moving_target.kl_derivative over appendix.tex:765-884 as the lower-ready backend while guided residual, LSI, residual DV, Gronwall, pure contraction, and EM reuse stay separate obligations.

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, using partial_t p_t=-div(p_t*u_t), integrating by parts, differentiating pi_t=Z_t^(-1)*p_t*exp(-f_t), canceling divergence terms, and concluding the centered mean-zero residual.
2. appendix.tex:724-744 states thm:general-moving-target-SALD with dynamics driven by c_t, diffusion sigma_t, residual m_t=v_t-c_t, finite residual alpha0-complexity, alpha in (0,alpha0], and the exact sigma-weighted KL bound.
3. appendix.tex:765-835 differentiates KL(rho_s||pi_{t(s)}), uses the general moving-target Fokker-Planck equation, and evaluates the rho_s and target-time terms by integration by parts.
4. appendix.tex:835-884 combines the c_t and v_t terms into m_t, applies Young with epsilon=2*dot t(s)/sigma_{t(s)}^2, changes from s to t, and uses eq:LSI-KL-FI to reach the pre-DV residual-energy inequality.
5. appendix.tex:885-907 applies lem:dv_variation with Z=alpha*||m_t||^2 and rewrites the log-mgf term as mathfrak E_alpha(pi_t,m_t).
6. appendix.tex:908-945 applies lem:gronwall with the source sigma-weighted coefficients, matches the theorem display, and specializes c_t=v_t so m_t=0 for pure contraction.
7. appendix.tex:949-951 is downstream reuse by thm:unified-forward-KL through the specialization c_t<-u_t; this middle packet does not introduce a direct VA-SALD proof.

leanStepMap : List String (explicit)

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

Ordered data items

1. Use SALD.cycle52GuidedGeneralSkeletonUpperPacket and SALD.cycle52GuidedGeneralSkeletonObligation as the parent route check after the cycle-50 and cycle-51 theorem-route wrappers.
2. Route appendix.tex:619-704 through SALD.guidedResidualIdentityContract, sald.guided_path_residual.normalizer_derivative, and sald.guided_path_residual.identity; keep normalizer positivity, differentiation under the integral, integration by parts, and mean-zero transport as obligations.
3. Keep SALD.generalMovingTargetStatementContract and SALD.generalVaSaldContract contractOnly; this middle audit adds no theorem hypotheses.
4. Route appendix.tex:765-884 through SALD.generalMovingTargetDerivativeCandidateContract, SALD.generalMovingTargetDerivativeObligation, sald.general_moving_target.kl_derivative, SALD.generalMovingTargetPostYoungDerivativeBoundScalar, SALD.generalMovingTargetLsiDerivativeBoundScalar, SALD.generalMovingTargetTimeChangedDerivativeBoundScalar, and SALD.generalMovingTargetPreDvDerivativeBoundScalar.
5. 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.
6. Route appendix.tex:908-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.
7. Keep SALD.discreteForwardKlEmInterpolationSideConditionContract and SALD.generalMovingTargetDiscreteDerivativeSideConditionContract visible only as downstream EM/Fokker-Planck interfaces for later discrete general reuse.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. lem:gronwall remains the endpoint-safe differentiability/FTC and coefficient-regularity obligation; cycle-52 only consumes it through the sigma-weighted general Gronwall interface.
2. lem:dv_variation remains source-cited; the general theorem must still supply common-space, absolute-continuity, finite-KL/log-likelihood, measurability, finite-log-mgf, and positive-alpha witnesses for Z=alpha*||m_t||^2.
3. eq:LSI-KL-FI remains the density, zero-set, admissible sqrt-density test, entropy identity, finite KL/FI, and Fisher chain-rule obligation.
4. The continuous general Fokker-Planck/KL derivative remains sald.general_moving_target.kl_derivative; compiled Real scalar helpers are handoffs only after analytic inputs are supplied.
5. The Euler-Maruyama interpolation Fokker-Planck backend remains a downstream discrete obligation and is not promoted or imported into the continuous theorem statement.

obligations : List String (explicit)

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

Ordered data items

1. sald.guided_general.cycle52_upper_route
2. sald.guided_general.cycle52_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.discrete_forward_kl.em_interpolation_fp
15. 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. Preferred target: SALD.generalMovingTargetDerivativeCandidateContract / SALD.generalMovingTargetDerivativeObligation / sald.general_moving_target.kl_derivative.
2. First lower sub-slice: appendix.tex:765-812, exposing density/law regularity, mass conservation, the general Fokker-Planck equation, KL differentiation under the integral, and integration-by-parts side conditions.
3. Second lower sub-slice: appendix.tex:813-864, supplying the target transport velocity v_t, the rescaled transport equation for pi_{t(s)}, the residual identification m_t=v_t-c_t, and the paper Young coefficient epsilon=2*dot t(s)/sigma_{t(s)}^2.
4. Third lower sub-slice: appendix.tex:865-884, preserving the LSI handoff and s-to-t schedule/sigma positivity assumptions without adding them to the theorem statement.
5. Alternative target only if derivative is blocked: SALD.guidedResidualIdentityContract / sald.guided_path_residual.identity for appendix.tex:630-704, sharpening normalizer, product/quotient differentiation, divergence cancellation, and mean-zero residual obligations.
6. Leave residual DV, Gronwall endpoint/exponent, pure contraction, unified specialization, and downstream EM interpolation as separate obligations.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.guidedResidualContract and SALD.generalVaSaldContract list SALD.cycle52GuidedGeneralSkeletonMiddleObligation while remaining contractOnly.
2. SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle52_middle_route_audit after ASTIS.SALD.guided_general.cycle52_upper_route.
3. SALD.saldDependenciesForLabel for prop:guided_path_residual and thm:general-moving-target-SALD includes the cycle-52 middle contract, middle obligation, and sald.guided_general.cycle52_middle_route_audit.
4. No Gronwall, DV, LSI/KL/FI, Fokker-Planck/KL derivative, guided residual, pure-contraction, or EM backend status is promoted.
5. python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass.

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 cycle52GuidedGeneralSkeletonMiddleContract :
    GeneralVaSaldGuidedPathMiddleContract where
  guidedResidualSource := saldGuidedResidualSource
  generalContinuousSource := saldGeneralMovingTargetSource
  unifiedSource := saldUnifiedForwardKlSource
  discreteSource := saldGeneralMovingTargetDiscreteSource
  objective := "Cycle 52 middle: verify the post-upper guided/general route against appendix.tex:619-951, keep prop:guided_path_residual and thm:general-moving-target-SALD unchanged, and select sald.general_moving_target.kl_derivative over appendix.tex:765-884 as the lower-ready backend while guided residual, LSI, residual DV, Gronwall, pure contraction, and EM reuse stay separate obligations."
  sourceStepMap := [
    "appendix.tex:619-704 proves prop:guided_path_residual by differentiating Z_t, using partial_t p_t=-div(p_t*u_t), integrating by parts, differentiating pi_t=Z_t^(-1)*p_t*exp(-f_t), canceling divergence terms, and concluding the centered mean-zero residual.",
    "appendix.tex:724-744 states thm:general-moving-target-SALD with dynamics driven by c_t, diffusion sigma_t, residual m_t=v_t-c_t, finite residual alpha0-complexity, alpha in (0,alpha0], and the exact sigma-weighted KL bound.",
    "appendix.tex:765-835 differentiates KL(rho_s||pi_{t(s)}), uses the general moving-target Fokker-Planck equation, and evaluates the rho_s and target-time terms by integration by parts.",
    "appendix.tex:835-884 combines the c_t and v_t terms into m_t, applies Young with epsilon=2*dot t(s)/sigma_{t(s)}^2, changes from s to t, and uses eq:LSI-KL-FI to reach the pre-DV residual-energy inequality.",
    "appendix.tex:885-907 applies lem:dv_variation with Z=alpha*||m_t||^2 and rewrites the log-mgf term as mathfrak E_alpha(pi_t,m_t).",
    "appendix.tex:908-945 applies lem:gronwall with the source sigma-weighted coefficients, matches the theorem display, and specializes c_t=v_t so m_t=0 for pure contraction.",
    "appendix.tex:949-951 is downstream reuse by thm:unified-forward-KL through the specialization c_t<-u_t; this middle packet does not introduce a direct VA-SALD proof."
  ]
  leanStepMap := [
    "Use SALD.cycle52GuidedGeneralSkeletonUpperPacket and SALD.cycle52GuidedGeneralSkeletonObligation as the parent route check after the cycle-50 and cycle-51 theorem-route wrappers.",
    "Route appendix.tex:619-704 through SALD.guidedResidualIdentityContract, sald.guided_path_residual.normalizer_derivative, and sald.guided_path_residual.identity; keep normalizer positivity, differentiation under the integral, integration by parts, and mean-zero transport as obligations.",
    "Keep SALD.generalMovingTargetStatementContract and SALD.generalVaSaldContract contractOnly; this middle audit adds no theorem hypotheses.",
    "Route appendix.tex:765-884 through SALD.generalMovingTargetDerivativeCandidateContract, SALD.generalMovingTargetDerivativeObligation, sald.general_moving_target.kl_derivative, SALD.generalMovingTargetPostYoungDerivativeBoundScalar, SALD.generalMovingTargetLsiDerivativeBoundScalar, SALD.generalMovingTargetTimeChangedDerivativeBoundScalar, and SALD.generalMovingTargetPreDvDerivativeBoundScalar.",
    "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:908-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.discreteForwardKlEmInterpolationSideConditionContract and SALD.generalMovingTargetDiscreteDerivativeSideConditionContract visible only as downstream EM/Fokker-Planck interfaces for later discrete general reuse."
  ]
  citedResultInterfaces := [
    "lem:gronwall remains the endpoint-safe differentiability/FTC and coefficient-regularity obligation; cycle-52 only consumes it through the sigma-weighted general Gronwall interface.",
    "lem:dv_variation remains source-cited; the general theorem must still supply common-space, absolute-continuity, finite-KL/log-likelihood, measurability, finite-log-mgf, and positive-alpha witnesses for Z=alpha*||m_t||^2.",
    "eq:LSI-KL-FI remains the density, zero-set, admissible sqrt-density test, entropy identity, finite KL/FI, and Fisher chain-rule obligation.",
    "The continuous general Fokker-Planck/KL derivative remains sald.general_moving_target.kl_derivative; compiled Real scalar helpers are handoffs only after analytic inputs are supplied.",
    "The Euler-Maruyama interpolation Fokker-Planck backend remains a downstream discrete obligation and is not promoted or imported into the continuous theorem statement."
  ]
  obligations := [
    "sald.guided_general.cycle52_upper_route",
    "sald.guided_general.cycle52_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.discrete_forward_kl.em_interpolation_fp",
    "sald.general_moving_target_discrete.em_interpolation_fp"
  ]
  lowerPacket := [
    "Preferred target: SALD.generalMovingTargetDerivativeCandidateContract / SALD.generalMovingTargetDerivativeObligation / sald.general_moving_target.kl_derivative.",
    "First lower sub-slice: appendix.tex:765-812, exposing density/law regularity, mass conservation, the general Fokker-Planck equation, KL differentiation under the integral, and integration-by-parts side conditions.",
    "Second lower sub-slice: appendix.tex:813-864, supplying the target transport velocity v_t, the rescaled transport equation for pi_{t(s)}, the residual identification m_t=v_t-c_t, and the paper Young coefficient epsilon=2*dot t(s)/sigma_{t(s)}^2.",
    "Third lower sub-slice: appendix.tex:865-884, preserving the LSI handoff and s-to-t schedule/sigma positivity assumptions without adding them to the theorem statement.",
    "Alternative target only if derivative is blocked: SALD.guidedResidualIdentityContract / sald.guided_path_residual.identity for appendix.tex:630-704, sharpening normalizer, product/quotient differentiation, divergence cancellation, and mean-zero residual obligations.",
    "Leave residual DV, Gronwall endpoint/exponent, pure contraction, unified specialization, and downstream EM interpolation as separate obligations."
  ]
  reviewerChecklist := [
    "SALD.guidedResidualContract and SALD.generalVaSaldContract list SALD.cycle52GuidedGeneralSkeletonMiddleObligation while remaining contractOnly.",
    "SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle52_middle_route_audit after ASTIS.SALD.guided_general.cycle52_upper_route.",
    "SALD.saldDependenciesForLabel for prop:guided_path_residual and thm:general-moving-target-SALD includes the cycle-52 middle contract, middle obligation, and sald.guided_general.cycle52_middle_route_audit.",
    "No Gronwall, DV, LSI/KL/FI, Fokker-Planck/KL derivative, guided residual, pure-contraction, or EM backend status is promoted.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

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