AutoSamplingTheory.SALD.cycle62GuidedGeneralSkeletonMiddleContract

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 cycle62GuidedGeneralSkeletonMiddleContract :
    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 62 middle: audit the cycle-62 upper guided/general route against appendix.tex:619-951 after the accepted cycle-61 discrete forward-KL recovery, add the middle route obligation to prop:guided_path_residual and thm:general-moving-target-SALD, and keep lower proof search narrowed to 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 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, 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)}), uses mass conservation, inserts the general moving-target Fokker-Planck equation, and evaluates the rho_s term by integration by parts.
4. appendix.tex:813-835 uses the transport equation for pi_t, rescales v_t by dot t(s), and evaluates the target-time contribution by integration by parts.
5. 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 residual-energy inequality.
6. 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).
7. appendix.tex:908-945 applies lem:gronwall with the source sigma-weighted coefficients, matches the theorem display, and proves the c_t=v_t pure-contraction clause by the zero residual alpha-complexity calculation.
8. appendix.tex:949-951 reuses the continuous general theorem for thm:unified-forward-KL by setting c_t<-u_t; this middle audit does not introduce an alternate VA-SALD proof.

leanStepMap : List String (explicit)

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

Ordered data items

1. Use SALD.cycle62GuidedGeneralSkeletonUpperPacket and SALD.cycle62GuidedGeneralSkeletonObligation as the parent route wrapper after the cycle-61 discrete recovery.
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, 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-57 residual split scalar handoff, 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: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.unifiedForwardKlSpecializationContract as downstream reuse and keep SALD.discreteForwardKlEmInterpolationSideConditionContract plus SALD.generalMovingTargetDiscreteDerivativeSideConditionContract visible only 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 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.cycle62_upper_route
2. sald.guided_general.cycle62_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. 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, expose density/law regularity, mass conservation, Fokker-Planck substitution, KL differentiation under the integral, and integration-by-parts side conditions.
3. Second lower sub-slice: appendix.tex:813-864, expose target transport by v_t, rescaled transport of pi_{t(s)}, 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, preserve the LSI handoff plus inverse-schedule and sigma-positivity side conditions without adding them to the theorem statement.
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.cycle62GuidedGeneralSkeletonMiddleObligation while remaining contractOnly.
2. SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle62_middle_route_audit between the cycle-62 upper route and the lower-packet node.
3. SALD.saldDependenciesForLabel for prop:guided_path_residual and thm:general-moving-target-SALD includes the cycle-62 middle contract, middle obligation, and sald.guided_general.cycle62_middle_route_audit.
4. No Gronwall, DV, LSI/KL/FI, Fokker-Planck/KL derivative, guided residual, 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 cycle62GuidedGeneralSkeletonMiddleContract :
    GeneralVaSaldGuidedPathMiddleContract where
  guidedResidualSource := saldGuidedResidualSource
  generalContinuousSource := saldGeneralMovingTargetSource
  unifiedSource := saldUnifiedForwardKlSource
  discreteSource := saldGeneralMovingTargetDiscreteSource
  objective := "Cycle 62 middle: audit the cycle-62 upper guided/general route against appendix.tex:619-951 after the accepted cycle-61 discrete forward-KL recovery, add the middle route obligation to prop:guided_path_residual and thm:general-moving-target-SALD, and keep lower proof search narrowed to sald.general_moving_target.kl_derivative over appendix.tex:765-884."
  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 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, 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)}), uses mass conservation, inserts the general moving-target Fokker-Planck equation, and evaluates the rho_s term by integration by parts.",
    "appendix.tex:813-835 uses the transport equation for pi_t, rescales v_t by dot t(s), and evaluates the target-time contribution by integration by parts.",
    "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 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:908-945 applies lem:gronwall with the source sigma-weighted coefficients, 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 reuses the continuous general theorem for thm:unified-forward-KL by setting c_t<-u_t; this middle audit does not introduce an alternate VA-SALD proof."
  ]
  leanStepMap := [
    "Use SALD.cycle62GuidedGeneralSkeletonUpperPacket and SALD.cycle62GuidedGeneralSkeletonObligation as the parent route wrapper after the cycle-61 discrete recovery.",
    "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, 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-57 residual split scalar handoff, 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: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.unifiedForwardKlSpecializationContract as downstream reuse and keep SALD.discreteForwardKlEmInterpolationSideConditionContract plus SALD.generalMovingTargetDiscreteDerivativeSideConditionContract visible only 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 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.cycle62_upper_route",
    "sald.guided_general.cycle62_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",
    "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, expose density/law regularity, mass conservation, Fokker-Planck substitution, KL differentiation under the integral, and integration-by-parts side conditions.",
    "Second lower sub-slice: appendix.tex:813-864, expose target transport by v_t, rescaled transport of pi_{t(s)}, 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, preserve the LSI handoff plus inverse-schedule and sigma-positivity side conditions without adding them to the theorem statement.",
    "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.cycle62GuidedGeneralSkeletonMiddleObligation while remaining contractOnly.",
    "SALD.generalVaSaldProofDag contains ASTIS.SALD.guided_general.cycle62_middle_route_audit between the cycle-62 upper route and the lower-packet node.",
    "SALD.saldDependenciesForLabel for prop:guided_path_residual and thm:general-moving-target-SALD includes the cycle-62 middle contract, middle obligation, and sald.guided_general.cycle62_middle_route_audit.",
    "No Gronwall, DV, LSI/KL/FI, Fokker-Planck/KL derivative, guided residual, 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-62 middle obligation tying the guided/general route audit to the next
lower backend. -/