AutoSamplingTheory.SALD.cycle67GuidedGeneralSkeletonMiddleContract

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 cycle67GuidedGeneralSkeletonMiddleContract :
    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 67 middle: audit the post-cycle-66 guided residual and thm:general-moving-target-SALD route against appendix.tex:619-951, wire the cycle-67 upper packet to the existing guided residual, derivative/LSI/DV/Gronwall/pure-contraction interfaces, and keep lower work on SALD.cycle67GuidedGeneralResidualGronwallBridgeObligation / sald.general_moving_target.cycle67_residual_to_gronwall_bridge over appendix.tex:765-945.

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), cancelling the divergence terms, substituting dot Z_t/Z_t=-E_pi_t[g_t], and deriving the centered mean-zero residual.
2. appendix.tex:724-744 states thm:general-moving-target-SALD with the general c_t-driven SDE, residual m_t=v_t-c_t, LSI constants C_LSI(t)>=0, finite E_alpha0(pi_t,m_t), alpha in (0,alpha0], and the exact sigma-weighted terminal KL display.
3. appendix.tex:765-835 differentiates KL(rho_s||pi_{t(s)}), inserts the general moving-target Fokker-Planck equation, evaluates the rho_s term by integration by parts, rescales the target velocity tilde v_s=dot t(s)*v_{t(s)}, and exposes the residual derivative display.
4. appendix.tex:835-884 combines c_t and v_t into m_t=v_t-c_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 K'(t) inequality.
5. appendix.tex:885-907 applies lem:dv_variation with Z=alpha*||m_t||^2, uses the alpha0-to-alpha finite-log-mgf witness, divides by alpha>0, and rewrites the log-mgf quotient as mathfrak E_alpha(pi_t,m_t).
6. appendix.tex:908-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 splits the exponent to match eq:general_moving_target_KL_bound.
7. 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.
8. appendix.tex:949-951 is downstream reuse for thm:unified-forward-KL by setting c_t<-u_t; this middle audit 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.cycle67GuidedGeneralSkeletonUpperPacket and SALD.cycle67GuidedGeneralSkeletonObligation as the parent route wrapper after the accepted cycle-66 discrete forward-KL route.
2. Route appendix.tex:619-704 through SALD.guidedResidualIdentityContract, sald.guided_path_residual.normalizer_derivative, and sald.guided_path_residual.identity; positive finite normalizer, differentiation under the integral, boundary integration by parts, quotient/product differentiation, and centering stay obligations.
3. Keep SALD.generalMovingTargetStatementContract, SALD.guidedResidualContract, SALD.generalVaSaldContract, and SALD.unifiedForwardKlContract 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.generalMovingTargetKlDerivativeResidualSplitScalar, SALD.generalMovingTargetKlDerivativeScaledResidualDisplayScalar, SALD.generalMovingTargetKlDerivativePreDvBoundOfSplitScalar, SALD.saldLsiKlFiDensityTestContract, probability.lsi_to_kl_fi, and the schedule/sigma side-condition obligations.
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, sald.general_moving_target.pure_contraction, and SALD.cycle67GuidedGeneralResidualGronwallBridgeObligation.
7. Keep SALD.unifiedForwardKlSpecializationContract and sald.unified_forward_kl.specialization as downstream reuse; keep SALD.discreteForwardKlEmInterpolationSideConditionContract plus SALD.generalMovingTargetDiscreteDerivativeSideConditionContract visible only as downstream EM interfaces.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. lem:gronwall remains an obligation through endpoint-safe differentiability, FTC/order integration, coefficient regularity, endpoint rewrites, exponent splitting, residual-exponent side conditions, and pure-contraction display matching.
2. lem:dv_variation remains source-cited; the residual step still needs common-space, absolute-continuity, finite KL, selected-test measurability, finite log-mgf, alpha0-to-alpha monotonicity, and positive-alpha division 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 scalar helpers only consume analytic inputs after they are supplied.
5. The Euler-Maruyama interpolation Fokker-Planck backend remains a downstream discrete obligation and is not 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.cycle67_upper_route
2. sald.guided_general.cycle67_middle_route_audit
3. sald.guided_path_residual.normalizer_derivative
4. sald.guided_path_residual.identity
5. sald.general_moving_target.kl_derivative
6. sald.general_moving_target.cycle57_derivative_split_lower
7. sald.general_moving_target.cycle62_scaled_residual_lower
8. probability.lsi_to_kl_fi
9. sald.general_moving_target.dv_finite_log_mgf_witness
10. sald.general_moving_target.dv_positive_alpha_scaling
11. sald.general_moving_target.dv_m_energy
12. sald.general_moving_target.gronwall_application
13. sald.general_moving_target.gronwall_side_conditions
14. sald.general_moving_target.pure_contraction
15. sald.general_moving_target.cycle67_residual_to_gronwall_bridge
16. sald.unified_forward_kl.specialization
17. 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.cycle67GuidedGeneralResidualGronwallBridgeObligation / sald.general_moving_target.cycle67_residual_to_gronwall_bridge.
2. First lower sub-slice: audit appendix.tex:765-884 from the KL derivative identity through residual Young, s-to-t schedule conversion, and the LSI/KL/FI handoff, preserving sigma_t^(-2)*dot{s}(t)^(-1) on the residual energy.
3. Second lower sub-slice: audit appendix.tex:885-907 through the residual DV finite-log-mgf and positive-alpha interfaces with Z=alpha*||m_t||^2, preserving the alpha^(-1)*K(t)+E_alpha(pi_t,m_t) output.
4. Third lower sub-slice: audit appendix.tex:908-945 through the Gronwall endpoint/exponent side conditions and pure-contraction zero-residual alpha-complexity interface.
5. If blocked, sharpen only the named source-cited or obligation interface; do not change theorem statements, constants, labels, or proof route.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.guidedResidualContract, SALD.generalVaSaldContract, and SALD.unifiedForwardKlContract list SALD.cycle67GuidedGeneralSkeletonMiddleObligation while remaining contractOnly.
2. SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle67_middle_route_audit between the cycle-67 general route and the residual-to-Gronwall lower packet.
3. SALD.saldDependenciesForLabel for prop:guided_path_residual, thm:general-moving-target-SALD, and thm:unified-forward-KL includes SALD.cycle67GuidedGeneralSkeletonMiddleContract, SALD.cycle67GuidedGeneralSkeletonMiddleObligation, and sald.guided_general.cycle67_middle_route_audit.
4. No Gronwall, DV, LSI/KL/FI, continuous Fokker-Planck/KL derivative, guided residual calculus, pure contraction, EM backend, theorem status, source label, source constant, or SLT reuse 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 cycle67GuidedGeneralSkeletonMiddleContract :
    GeneralVaSaldGuidedPathMiddleContract where
  guidedResidualSource := saldGuidedResidualSource
  generalContinuousSource := saldGeneralMovingTargetSource
  unifiedSource := saldUnifiedForwardKlSource
  discreteSource := saldGeneralMovingTargetDiscreteSource
  objective := "Cycle 67 middle: audit the post-cycle-66 guided residual and thm:general-moving-target-SALD route against appendix.tex:619-951, wire the cycle-67 upper packet to the existing guided residual, derivative/LSI/DV/Gronwall/pure-contraction interfaces, and keep lower work on SALD.cycle67GuidedGeneralResidualGronwallBridgeObligation / sald.general_moving_target.cycle67_residual_to_gronwall_bridge over appendix.tex:765-945."
  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), cancelling the divergence terms, substituting dot Z_t/Z_t=-E_pi_t[g_t], and deriving the centered mean-zero residual.",
    "appendix.tex:724-744 states thm:general-moving-target-SALD with the general c_t-driven SDE, residual m_t=v_t-c_t, LSI constants C_LSI(t)>=0, finite E_alpha0(pi_t,m_t), alpha in (0,alpha0], and the exact sigma-weighted terminal KL display.",
    "appendix.tex:765-835 differentiates KL(rho_s||pi_{t(s)}), inserts the general moving-target Fokker-Planck equation, evaluates the rho_s term by integration by parts, rescales the target velocity tilde v_s=dot t(s)*v_{t(s)}, and exposes the residual derivative display.",
    "appendix.tex:835-884 combines c_t and v_t into m_t=v_t-c_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 K'(t) inequality.",
    "appendix.tex:885-907 applies lem:dv_variation with Z=alpha*||m_t||^2, uses the alpha0-to-alpha finite-log-mgf witness, divides by alpha>0, and rewrites the log-mgf quotient as mathfrak E_alpha(pi_t,m_t).",
    "appendix.tex:908-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 splits the exponent to match eq:general_moving_target_KL_bound.",
    "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 for thm:unified-forward-KL by setting c_t<-u_t; this middle audit does not introduce a direct VA-SALD proof."
  ]
  leanStepMap := [
    "Use SALD.cycle67GuidedGeneralSkeletonUpperPacket and SALD.cycle67GuidedGeneralSkeletonObligation as the parent route wrapper after the accepted cycle-66 discrete forward-KL route.",
    "Route appendix.tex:619-704 through SALD.guidedResidualIdentityContract, sald.guided_path_residual.normalizer_derivative, and sald.guided_path_residual.identity; positive finite normalizer, differentiation under the integral, boundary integration by parts, quotient/product differentiation, and centering stay obligations.",
    "Keep SALD.generalMovingTargetStatementContract, SALD.guidedResidualContract, SALD.generalVaSaldContract, and SALD.unifiedForwardKlContract 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.generalMovingTargetKlDerivativeResidualSplitScalar, SALD.generalMovingTargetKlDerivativeScaledResidualDisplayScalar, SALD.generalMovingTargetKlDerivativePreDvBoundOfSplitScalar, SALD.saldLsiKlFiDensityTestContract, probability.lsi_to_kl_fi, and the schedule/sigma side-condition obligations.",
    "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, sald.general_moving_target.pure_contraction, and SALD.cycle67GuidedGeneralResidualGronwallBridgeObligation.",
    "Keep SALD.unifiedForwardKlSpecializationContract and sald.unified_forward_kl.specialization as downstream reuse; keep SALD.discreteForwardKlEmInterpolationSideConditionContract plus SALD.generalMovingTargetDiscreteDerivativeSideConditionContract visible only as downstream EM interfaces."
  ]
  citedResultInterfaces := [
    "lem:gronwall remains an obligation through endpoint-safe differentiability, FTC/order integration, coefficient regularity, endpoint rewrites, exponent splitting, residual-exponent side conditions, and pure-contraction display matching.",
    "lem:dv_variation remains source-cited; the residual step still needs common-space, absolute-continuity, finite KL, selected-test measurability, finite log-mgf, alpha0-to-alpha monotonicity, and positive-alpha division 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 scalar helpers only consume analytic inputs after they are supplied.",
    "The Euler-Maruyama interpolation Fokker-Planck backend remains a downstream discrete obligation and is not imported into the continuous theorem statement."
  ]
  obligations := [
    "sald.guided_general.cycle67_upper_route",
    "sald.guided_general.cycle67_middle_route_audit",
    "sald.guided_path_residual.normalizer_derivative",
    "sald.guided_path_residual.identity",
    "sald.general_moving_target.kl_derivative",
    "sald.general_moving_target.cycle57_derivative_split_lower",
    "sald.general_moving_target.cycle62_scaled_residual_lower",
    "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.general_moving_target.cycle67_residual_to_gronwall_bridge",
    "sald.unified_forward_kl.specialization",
    "sald.general_moving_target_discrete.em_interpolation_fp"
  ]
  lowerPacket := [
    "Target exactly SALD.cycle67GuidedGeneralResidualGronwallBridgeObligation / sald.general_moving_target.cycle67_residual_to_gronwall_bridge.",
    "First lower sub-slice: audit appendix.tex:765-884 from the KL derivative identity through residual Young, s-to-t schedule conversion, and the LSI/KL/FI handoff, preserving sigma_t^(-2)*dot{s}(t)^(-1) on the residual energy.",
    "Second lower sub-slice: audit appendix.tex:885-907 through the residual DV finite-log-mgf and positive-alpha interfaces with Z=alpha*||m_t||^2, preserving the alpha^(-1)*K(t)+E_alpha(pi_t,m_t) output.",
    "Third lower sub-slice: audit appendix.tex:908-945 through the Gronwall endpoint/exponent side conditions and pure-contraction zero-residual alpha-complexity interface.",
    "If blocked, sharpen only the named source-cited or obligation interface; do not change theorem statements, constants, labels, or proof route."
  ]
  reviewerChecklist := [
    "SALD.guidedResidualContract, SALD.generalVaSaldContract, and SALD.unifiedForwardKlContract list SALD.cycle67GuidedGeneralSkeletonMiddleObligation while remaining contractOnly.",
    "SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle67_middle_route_audit between the cycle-67 general route and the residual-to-Gronwall lower packet.",
    "SALD.saldDependenciesForLabel for prop:guided_path_residual, thm:general-moving-target-SALD, and thm:unified-forward-KL includes SALD.cycle67GuidedGeneralSkeletonMiddleContract, SALD.cycle67GuidedGeneralSkeletonMiddleObligation, and sald.guided_general.cycle67_middle_route_audit.",
    "No Gronwall, DV, LSI/KL/FI, continuous Fokker-Planck/KL derivative, guided residual calculus, pure contraction, EM backend, theorem status, source label, source constant, or SLT reuse status is promoted.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

/-- Cycle-67 middle obligation tying the guided/general route audit to the
residual-to-Gronwall lower packet. -/