AutoSamplingTheory.SALD.cycle57GuidedGeneralSkeletonMiddleContract

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 cycle57GuidedGeneralSkeletonMiddleContract :
    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 57 middle: audit the upper guided/general route against appendix.tex:619-951 after the clean cycle-56 recovery, add the middle route obligation to prop:guided_path_residual and thm:general-moving-target-SALD, and keep lower work focused on sald.general_moving_target.kl_derivative over appendix.tex:765-884.

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 the normalizer 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 divergence terms, substituting dot Z_t/Z_t, and deriving 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-812 differentiates KL(rho_s||pi_{t(s)}), drops the mass term, inserts the general moving-target Fokker-Planck equation, and evaluates the rho_s term as a c_t transport contribution minus sigma^2/2 times FI.
4. appendix.tex:814-835 uses that v_t transports pi_t, so dot t(s)*v_{t(s)} transports pi_{t(s)}, and evaluates the target-time term by integration by parts.
5. appendix.tex:835-864 combines c_t and v_t into m_t=v_t-c_t and applies Young with epsilon=2*dot t(s)/sigma_{t(s)}^2, preserving the sigma_t^(-2)*dot t(s)^2 residual-energy coefficient.
6. appendix.tex:865-884 changes to K(t)=KL(rho_{s(t)}||pi_t), uses dot t(s(t))=dot s(t)^(-1), and applies eq:LSI-KL-FI to produce the pre-DV residual-energy inequality.
7. appendix.tex:885-907 applies lem:dv_variation with Z=alpha*||m_t||^2 and rewrites the log-mgf quotient as mathfrak E_alpha(pi_t,m_t).
8. appendix.tex:909-945 applies lem:gronwall with the source sigma-weighted a(t) and b(t), matches the theorem display, and proves the c_t=v_t pure-contraction clause by the zero residual alpha-complexity calculation.
9. 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.cycle57GuidedGeneralSkeletonUpperPacket and SALD.cycle57GuidedGeneralSkeletonObligation as the parent route check after cycle 56.
2. Route appendix.tex:619-704 through SALD.guidedResidualIdentityContract, sald.guided_path_residual.normalizer_derivative, and sald.guided_path_residual.identity.
3. Keep SALD.generalMovingTargetStatementContract, SALD.guidedResidualContract, 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, the cycle-52 scalar handoffs, SALD.saldLsiKlFiDensityTestContract, probability.lsi_to_kl_fi, and sald.forward_kl.schedule_time_change.
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: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.
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 an obligation through endpoint-safe differentiability, FTC/order integration, coefficient regularity, endpoint rewrites, exponent splitting, and residual-exponent side conditions.
2. lem:dv_variation remains source-cited; the continuous general theorem still needs 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 is the selected lower backend; compiled real 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.cycle57_upper_route
2. sald.guided_general.cycle57_middle_route_audit
3. sald.general_moving_target.cycle57_derivative_split_lower
4. sald.guided_path_residual.normalizer_derivative
5. sald.guided_path_residual.identity
6. sald.general_moving_target.kl_derivative
7. probability.lsi_to_kl_fi
8. sald.general_moving_target.dv_finite_log_mgf_witness
9. sald.general_moving_target.dv_positive_alpha_scaling
10. sald.general_moving_target.dv_m_energy
11. sald.general_moving_target.gronwall_application
12. sald.general_moving_target.gronwall_side_conditions
13. sald.general_moving_target.pure_contraction
14. sald.unified_forward_kl.specialization
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. Target exactly SALD.generalMovingTargetDerivativeCandidateContract / SALD.generalMovingTargetDerivativeObligation / sald.general_moving_target.kl_derivative.
2. First lower sub-slice: appendix.tex:765-812, exposing law regularity, mass conservation, Fokker-Planck substitution, KL differentiation under the integral, and integration-by-parts side conditions; SALD.generalMovingTargetKlDerivativeResidualSplitScalar compiles only the scalar residual split after those analytic inputs are supplied.
3. Second lower sub-slice: appendix.tex:813-864, exposing target transport by v_t, the rescaled pi_{t(s)} transport equation, residual identification m_t=v_t-c_t, and the Young coefficient epsilon=2*dot t(s)/sigma_{t(s)}^2.
4. Third lower sub-slice: appendix.tex:865-884, preserving the LSI handoff plus inverse-schedule and sigma-positivity side conditions without adding them to the theorem statement; SALD.generalMovingTargetKlDerivativePreDvBoundOfSplitScalar composes the split with the existing pre-DV scalar pipeline.
5. Leave guided residual calculus, residual DV, Gronwall endpoint/exponent, pure contraction, unified specialization, and downstream EM interpolation as separate obligations unless exact compiled proofs are added.

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.cycle57GuidedGeneralSkeletonMiddleObligation while remaining contractOnly.
2. SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle57_middle_route_audit between the cycle-57 upper route and the lower derivative packet.
3. SALD.saldDependenciesForLabel for prop:guided_path_residual and thm:general-moving-target-SALD includes the cycle-57 middle contract, middle obligation, and sald.guided_general.cycle57_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 cycle57GuidedGeneralSkeletonMiddleContract :
    GeneralVaSaldGuidedPathMiddleContract where
  guidedResidualSource := saldGuidedResidualSource
  generalContinuousSource := saldGeneralMovingTargetSource
  unifiedSource := saldUnifiedForwardKlSource
  discreteSource := saldGeneralMovingTargetDiscreteSource
  objective := "Cycle 57 middle: audit the upper guided/general route against appendix.tex:619-951 after the clean cycle-56 recovery, add the middle route obligation to prop:guided_path_residual and thm:general-moving-target-SALD, and keep lower work focused on sald.general_moving_target.kl_derivative over appendix.tex:765-884."
  sourceStepMap := [
    "appendix.tex:619-704 proves prop:guided_path_residual by differentiating the normalizer 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 divergence terms, substituting dot Z_t/Z_t, and deriving 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-812 differentiates KL(rho_s||pi_{t(s)}), drops the mass term, inserts the general moving-target Fokker-Planck equation, and evaluates the rho_s term as a c_t transport contribution minus sigma^2/2 times FI.",
    "appendix.tex:814-835 uses that v_t transports pi_t, so dot t(s)*v_{t(s)} transports pi_{t(s)}, and evaluates the target-time term by integration by parts.",
    "appendix.tex:835-864 combines c_t and v_t into m_t=v_t-c_t and applies Young with epsilon=2*dot t(s)/sigma_{t(s)}^2, preserving the sigma_t^(-2)*dot t(s)^2 residual-energy coefficient.",
    "appendix.tex:865-884 changes to K(t)=KL(rho_{s(t)}||pi_t), uses dot t(s(t))=dot s(t)^(-1), and applies eq:LSI-KL-FI to produce 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 quotient as mathfrak E_alpha(pi_t,m_t).",
    "appendix.tex:909-945 applies lem:gronwall with the source sigma-weighted a(t) and b(t), matches the theorem display, and proves the c_t=v_t pure-contraction clause by the zero residual alpha-complexity calculation.",
    "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.cycle57GuidedGeneralSkeletonUpperPacket and SALD.cycle57GuidedGeneralSkeletonObligation as the parent route check after cycle 56.",
    "Route appendix.tex:619-704 through SALD.guidedResidualIdentityContract, sald.guided_path_residual.normalizer_derivative, and sald.guided_path_residual.identity.",
    "Keep SALD.generalMovingTargetStatementContract, SALD.guidedResidualContract, 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, the cycle-52 scalar handoffs, 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.discreteForwardKlEmInterpolationSideConditionContract and SALD.generalMovingTargetDiscreteDerivativeSideConditionContract visible only as downstream EM/Fokker-Planck interfaces for later discrete general reuse."
  ]
  citedResultInterfaces := [
    "lem:gronwall remains an obligation through endpoint-safe differentiability, FTC/order integration, coefficient regularity, endpoint rewrites, exponent splitting, and residual-exponent side conditions.",
    "lem:dv_variation remains source-cited; the continuous general theorem still needs 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 is the selected lower backend; compiled real 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.cycle57_upper_route",
    "sald.guided_general.cycle57_middle_route_audit",
    "sald.general_moving_target.cycle57_derivative_split_lower",
    "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: appendix.tex:765-812, exposing law regularity, mass conservation, Fokker-Planck substitution, KL differentiation under the integral, and integration-by-parts side conditions; SALD.generalMovingTargetKlDerivativeResidualSplitScalar compiles only the scalar residual split after those analytic inputs are supplied.",
    "Second lower sub-slice: appendix.tex:813-864, exposing target transport by v_t, the rescaled pi_{t(s)} transport equation, residual identification m_t=v_t-c_t, and the Young coefficient epsilon=2*dot t(s)/sigma_{t(s)}^2.",
    "Third lower sub-slice: appendix.tex:865-884, preserving the LSI handoff plus inverse-schedule and sigma-positivity side conditions without adding them to the theorem statement; SALD.generalMovingTargetKlDerivativePreDvBoundOfSplitScalar composes the split with the existing pre-DV scalar pipeline.",
    "Leave guided residual calculus, residual DV, Gronwall endpoint/exponent, pure contraction, unified specialization, and downstream EM interpolation as separate obligations unless exact compiled proofs are added."
  ]
  reviewerChecklist := [
    "SALD.guidedResidualContract and SALD.generalVaSaldContract list SALD.cycle57GuidedGeneralSkeletonMiddleObligation while remaining contractOnly.",
    "SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle57_middle_route_audit between the cycle-57 upper route and the lower derivative packet.",
    "SALD.saldDependenciesForLabel for prop:guided_path_residual and thm:general-moving-target-SALD includes the cycle-57 middle contract, middle obligation, and sald.guided_general.cycle57_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-57 middle obligation tying the guided/general route audit to lower
work. -/