AutoSamplingTheory.SALD.cycle63UnifiedDiscreteGeneralMiddleContract

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 cycle63UnifiedDiscreteGeneralMiddleContract :
    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 63 middle: audit the upper unified/discrete-general route in paper order, confirm that thm:unified-forward-KL remains only the continuous general specialization with c_t=u_t and m_t=w_t, confirm that thm:general-moving-target-SALD-discrete consumes the general EM endpoint/conditional-FP, frozen-delta, LSI, residual DV, and Gronwall interfaces, and keep the next lower packet on the conditional-law/Fokker-Planck half of appendix.tex:1354-1387 after the paired endpoint-law Measure.map helper.

sourceStepMap : List String (explicit)

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

Ordered data items

1. main_body.tex:359-368 uses prop:guided_path_residual and eq:poisson-eq to make u_t+w_t a transport velocity for pi_t.
2. main_body.tex:372-395 states thm:unified-forward-KL with correction-field complexity E_alpha(pi_t,w_t) and the source sigma_t^{-2} dot{s}(t)^{-1} coefficients.
3. appendix.tex:949-951 proves thm:unified-forward-KL by specializing thm:general-moving-target-SALD with c_t=u_t and m_t=w_t.
4. appendix.tex:1313-1347 states thm:general-moving-target-SALD-discrete with the doubled residual coefficient, Gamma/Delta terms, sigma_eta factors, alpha ranges, and constant inverse-schedule assumption.
5. appendix.tex:1354-1357 fixes k and records the endpoint laws hat rho_{s_k}=rho_k^eta and hat rho_{s_{k+1}}=rho_{k+1}^eta.
6. appendix.tex:1358-1387 differentiates KL, defines the frozen conditional drift bar b_{k,s}, invokes the conditional Fokker-Planck equation, and starts the derivative route.
7. appendix.tex:1389-1511 splits the Laplacian, identifies delta_pi^VA+dot t(s)m_t, and applies the two sigma_eta^2/8 Young splits plus the frozen-delta bound.
8. appendix.tex:1513-1570 applies eq:LSI-KL-FI and lem:dv_variation to the residual m_t under the EM interpolation law.
9. appendix.tex:1573-1600 changes variables to K(t), uses dot t(s(t))=dot s(t)^{-1}, and applies lem:gronwall to match the theorem display.
10. appendix.tex:1603 records the discrete guided VA-SALD specialization c_t=u_t.

leanStepMap : List String (explicit)

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

Ordered data items

1. Use SALD.cycle63UnifiedDiscreteGeneralSkeletonUpperPacket and SALD.cycle63UnifiedDiscreteGeneralSkeletonObligation as parent route data; do not replace the cycle-62 continuous/general route.
2. Route thm:unified-forward-KL through SALD.unifiedForwardKlSpecializationContract, sald.unified_forward_kl.transport_velocity_bridge, sald.unified_forward_kl.specialization, SALD.generalVaSaldContract, and the accepted cycle-62 guided/general obligations.
3. Route appendix.tex:1313-1347 through SALD.generalMovingTargetDiscreteStatementContract and SALD.generalVaSaldDiscreteContract; both remain contractOnly.
4. Route appendix.tex:1354-1357 through SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation, AutoSamplingTheory.lawMapProdEqOfAEEq, AutoSamplingTheory.lawMapProdFst/Snd, SALD.generalMovingTargetDiscreteEmJointEndpointMeasureMapOfNamedInterpolation, and SALD.generalMovingTargetDiscreteEmJointEndpointMarginalLawsOfNamedInterpolation as endpoint-law bookkeeping only.
5. Route appendix.tex:1358-1387 through SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, and sald.general_moving_target_discrete.em_interpolation_fp for common-space, density/AC, regular conditional drift, weak conditional-FP, and KL differentiation obligations.
6. Route appendix.tex:1389-1511 through SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, SALD.generalMovingTargetDiscreteFrozenResidualAlgebraVector, the cycle-28 Young/Fisher scalar bookkeeping helpers, and sald.general_moving_target_discrete.derivative_side_conditions.
7. Route appendix.tex:1513-1570 through SALD.saldLsiKlFiDensityTestContract, probability.lsi_to_kl_fi, dvVariationalFormulaInterface saldDvVariationSource, SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract, and sald.general_moving_target_discrete.dv_m_energy.
8. Route appendix.tex:1573-1600 through SALD.generalMovingTargetDiscreteGronwallInstantiationContract, SALD.generalMovingTargetDiscreteGronwallSideConditionContract, cycle-58/cycle-59 Gronwall display handoffs, sald.general_moving_target_discrete.gronwall_application, and sald.general_moving_target_discrete.gronwall_side_conditions.
9. Select lower work exactly at sald.general_moving_target_discrete.em_interpolation_fp / sald.general_moving_target_discrete.cycle48_em_endpoint_conditional_fp_audit for the conditional-law Fokker-Planck backend after the endpoint Measure.map layer.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. lem:gronwall remains an endpoint-safe differentiability, FTC, coefficient-regularity, endpoint-stitching, and display-matching obligation.
2. lem:dv_variation remains source-cited through common-space, absolute-continuity, finite-KL, selected-test measurability, finite-log-mgf, and alpha-scaling witnesses.
3. eq:LSI-KL-FI remains the density, zero-set convention, admissible sqrt-density test or approximation, entropy identity, finite KL/FI, and Fisher-chain obligation.
4. The continuous Fokker-Planck/KL derivative is consumed upstream through sald.general_moving_target.kl_derivative and the cycle-62 scaled residual scalar handoff, not reproved for the unified theorem.
5. The EM interpolation backend remains sald.general_moving_target_discrete.em_interpolation_fp; AutoSamplingTheory.lawMapProdEqOfAEEq, AutoSamplingTheory.lawMapProdFst/Snd, and the two SALD joint endpoint wrappers prove only paired endpoint-law congruence and marginal extraction on a common space.
6. Local SLT material is reference-only for Measure.map and a.e.-equality style; no SLT theorem is imported or marked formalized.

obligations : List String (explicit)

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

Ordered data items

1. sald.unified_discrete_general.cycle63_upper_route
2. sald.unified_discrete_general.cycle63_middle_route_audit
3. sald.general_moving_target_discrete.cycle63_joint_endpoint_law_backfill
4. sald.guided_general.cycle62_middle_route_audit
5. sald.general_moving_target.cycle62_scaled_residual_lower
6. sald.unified_forward_kl.transport_velocity_bridge
7. sald.unified_forward_kl.specialization
8. sald.general_moving_target_discrete.cycle48_em_endpoint_conditional_fp_audit
9. sald.general_moving_target_discrete.em_interpolation_fp
10. sald.general_moving_target_discrete.derivative_side_conditions
11. sald.general_moving_target_discrete.kl_derivative
12. sald.general_moving_target_discrete.dv_finite_log_mgf_witness
13. sald.general_moving_target_discrete.dv_m_energy
14. sald.general_moving_target_discrete.gronwall_application
15. sald.general_moving_target_discrete.gronwall_side_conditions

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation / SALD.generalMovingTargetDiscreteDerivativeSideConditionContract / sald.general_moving_target_discrete.em_interpolation_fp.
2. First sub-slice: after the paired endpoint-law helper, expose common probability space data, hat rho_s and tilde pi_s density/absolute-continuity, and endpoint-law stitching assumptions needed before KL is differentiated.
3. Second sub-slice: define and typecheck the regular conditional drift bar b_{k,s}(x), including measurability and integrability hypotheses for the conditional expectation in appendix.tex:1364-1371.
4. Third sub-slice: state the weak conditional Fokker-Planck equation from appendix.tex:1372-1387 with conditional drift and Laplacian terms in the exact source signs.
5. Do not restate either theorem, change coefficients, or promote endpoint Measure.map bookkeeping into conditional drift, density, weak Fokker-Planck, KL derivative, DV, LSI/KL/FI, or Gronwall formalization.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.unifiedForwardKlContract and SALD.generalVaSaldDiscreteContract list SALD.cycle63UnifiedDiscreteGeneralMiddleObligation while remaining contractOnly.
2. SALD.generalVaSaldProofDag and SALD.generalVaSaldDiscreteProofDag contain ASTIS.SALD.unified_discrete_general.cycle63_middle_route_audit and the paired endpoint-law backfill row.
3. SALD.saldDependenciesForLabel entries for thm:unified-forward-KL and thm:general-moving-target-SALD-discrete include the cycle-63 middle contract, middle obligation, and route-audit node.
4. Only AutoSamplingTheory.lawMapProdEqOfAEEq, AutoSamplingTheory.lawMapProdFst/Snd, SALD.generalMovingTargetDiscreteEmJointEndpointMeasureMapOfNamedInterpolation, and SALD.generalMovingTargetDiscreteEmJointEndpointMarginalLawsOfNamedInterpolation are added as formalized local endpoint-law bookkeeping in this cycle; analytic backends remain sourceCited or obligation-level.
5. The lower packet is the conditional-law/Fokker-Planck backend over appendix.tex:1358-1387, not a new theorem statement or broad SLT/SDE port.
6. 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 cycle63UnifiedDiscreteGeneralMiddleContract :
    GeneralVaSaldGuidedPathMiddleContract where
  guidedResidualSource := saldGuidedResidualSource
  generalContinuousSource := saldGeneralMovingTargetSource
  unifiedSource := saldUnifiedForwardKlSource
  discreteSource := saldGeneralMovingTargetDiscreteSource
  objective := "Cycle 63 middle: audit the upper unified/discrete-general route in paper order, confirm that thm:unified-forward-KL remains only the continuous general specialization with c_t=u_t and m_t=w_t, confirm that thm:general-moving-target-SALD-discrete consumes the general EM endpoint/conditional-FP, frozen-delta, LSI, residual DV, and Gronwall interfaces, and keep the next lower packet on the conditional-law/Fokker-Planck half of appendix.tex:1354-1387 after the paired endpoint-law Measure.map helper."
  sourceStepMap := [
    "main_body.tex:359-368 uses prop:guided_path_residual and eq:poisson-eq to make u_t+w_t a transport velocity for pi_t.",
    "main_body.tex:372-395 states thm:unified-forward-KL with correction-field complexity E_alpha(pi_t,w_t) and the source sigma_t^{-2} dot{s}(t)^{-1} coefficients.",
    "appendix.tex:949-951 proves thm:unified-forward-KL by specializing thm:general-moving-target-SALD with c_t=u_t and m_t=w_t.",
    "appendix.tex:1313-1347 states thm:general-moving-target-SALD-discrete with the doubled residual coefficient, Gamma/Delta terms, sigma_eta factors, alpha ranges, and constant inverse-schedule assumption.",
    "appendix.tex:1354-1357 fixes k and records the endpoint laws hat rho_{s_k}=rho_k^eta and hat rho_{s_{k+1}}=rho_{k+1}^eta.",
    "appendix.tex:1358-1387 differentiates KL, defines the frozen conditional drift bar b_{k,s}, invokes the conditional Fokker-Planck equation, and starts the derivative route.",
    "appendix.tex:1389-1511 splits the Laplacian, identifies delta_pi^VA+dot t(s)m_t, and applies the two sigma_eta^2/8 Young splits plus the frozen-delta bound.",
    "appendix.tex:1513-1570 applies eq:LSI-KL-FI and lem:dv_variation to the residual m_t under the EM interpolation law.",
    "appendix.tex:1573-1600 changes variables to K(t), uses dot t(s(t))=dot s(t)^{-1}, and applies lem:gronwall to match the theorem display.",
    "appendix.tex:1603 records the discrete guided VA-SALD specialization c_t=u_t."
  ]
  leanStepMap := [
    "Use SALD.cycle63UnifiedDiscreteGeneralSkeletonUpperPacket and SALD.cycle63UnifiedDiscreteGeneralSkeletonObligation as parent route data; do not replace the cycle-62 continuous/general route.",
    "Route thm:unified-forward-KL through SALD.unifiedForwardKlSpecializationContract, sald.unified_forward_kl.transport_velocity_bridge, sald.unified_forward_kl.specialization, SALD.generalVaSaldContract, and the accepted cycle-62 guided/general obligations.",
    "Route appendix.tex:1313-1347 through SALD.generalMovingTargetDiscreteStatementContract and SALD.generalVaSaldDiscreteContract; both remain contractOnly.",
    "Route appendix.tex:1354-1357 through SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation, AutoSamplingTheory.lawMapProdEqOfAEEq, AutoSamplingTheory.lawMapProdFst/Snd, SALD.generalMovingTargetDiscreteEmJointEndpointMeasureMapOfNamedInterpolation, and SALD.generalMovingTargetDiscreteEmJointEndpointMarginalLawsOfNamedInterpolation as endpoint-law bookkeeping only.",
    "Route appendix.tex:1358-1387 through SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, and sald.general_moving_target_discrete.em_interpolation_fp for common-space, density/AC, regular conditional drift, weak conditional-FP, and KL differentiation obligations.",
    "Route appendix.tex:1389-1511 through SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, SALD.generalMovingTargetDiscreteFrozenResidualAlgebraVector, the cycle-28 Young/Fisher scalar bookkeeping helpers, and sald.general_moving_target_discrete.derivative_side_conditions.",
    "Route appendix.tex:1513-1570 through SALD.saldLsiKlFiDensityTestContract, probability.lsi_to_kl_fi, dvVariationalFormulaInterface saldDvVariationSource, SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract, and sald.general_moving_target_discrete.dv_m_energy.",
    "Route appendix.tex:1573-1600 through SALD.generalMovingTargetDiscreteGronwallInstantiationContract, SALD.generalMovingTargetDiscreteGronwallSideConditionContract, cycle-58/cycle-59 Gronwall display handoffs, sald.general_moving_target_discrete.gronwall_application, and sald.general_moving_target_discrete.gronwall_side_conditions.",
    "Select lower work exactly at sald.general_moving_target_discrete.em_interpolation_fp / sald.general_moving_target_discrete.cycle48_em_endpoint_conditional_fp_audit for the conditional-law Fokker-Planck backend after the endpoint Measure.map layer."
  ]
  citedResultInterfaces := [
    "lem:gronwall remains an endpoint-safe differentiability, FTC, coefficient-regularity, endpoint-stitching, and display-matching obligation.",
    "lem:dv_variation remains source-cited through common-space, absolute-continuity, finite-KL, selected-test measurability, finite-log-mgf, and alpha-scaling witnesses.",
    "eq:LSI-KL-FI remains the density, zero-set convention, admissible sqrt-density test or approximation, entropy identity, finite KL/FI, and Fisher-chain obligation.",
    "The continuous Fokker-Planck/KL derivative is consumed upstream through sald.general_moving_target.kl_derivative and the cycle-62 scaled residual scalar handoff, not reproved for the unified theorem.",
    "The EM interpolation backend remains sald.general_moving_target_discrete.em_interpolation_fp; AutoSamplingTheory.lawMapProdEqOfAEEq, AutoSamplingTheory.lawMapProdFst/Snd, and the two SALD joint endpoint wrappers prove only paired endpoint-law congruence and marginal extraction on a common space.",
    "Local SLT material is reference-only for Measure.map and a.e.-equality style; no SLT theorem is imported or marked formalized."
  ]
  obligations := [
    "sald.unified_discrete_general.cycle63_upper_route",
    "sald.unified_discrete_general.cycle63_middle_route_audit",
    "sald.general_moving_target_discrete.cycle63_joint_endpoint_law_backfill",
    "sald.guided_general.cycle62_middle_route_audit",
    "sald.general_moving_target.cycle62_scaled_residual_lower",
    "sald.unified_forward_kl.transport_velocity_bridge",
    "sald.unified_forward_kl.specialization",
    "sald.general_moving_target_discrete.cycle48_em_endpoint_conditional_fp_audit",
    "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"
  ]
  lowerPacket := [
    "Target exactly SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation / SALD.generalMovingTargetDiscreteDerivativeSideConditionContract / sald.general_moving_target_discrete.em_interpolation_fp.",
    "First sub-slice: after the paired endpoint-law helper, expose common probability space data, hat rho_s and tilde pi_s density/absolute-continuity, and endpoint-law stitching assumptions needed before KL is differentiated.",
    "Second sub-slice: define and typecheck the regular conditional drift bar b_{k,s}(x), including measurability and integrability hypotheses for the conditional expectation in appendix.tex:1364-1371.",
    "Third sub-slice: state the weak conditional Fokker-Planck equation from appendix.tex:1372-1387 with conditional drift and Laplacian terms in the exact source signs.",
    "Do not restate either theorem, change coefficients, or promote endpoint Measure.map bookkeeping into conditional drift, density, weak Fokker-Planck, KL derivative, DV, LSI/KL/FI, or Gronwall formalization."
  ]
  reviewerChecklist := [
    "SALD.unifiedForwardKlContract and SALD.generalVaSaldDiscreteContract list SALD.cycle63UnifiedDiscreteGeneralMiddleObligation while remaining contractOnly.",
    "SALD.generalVaSaldProofDag and SALD.generalVaSaldDiscreteProofDag contain ASTIS.SALD.unified_discrete_general.cycle63_middle_route_audit and the paired endpoint-law backfill row.",
    "SALD.saldDependenciesForLabel entries for thm:unified-forward-KL and thm:general-moving-target-SALD-discrete include the cycle-63 middle contract, middle obligation, and route-audit node.",
    "Only AutoSamplingTheory.lawMapProdEqOfAEEq, AutoSamplingTheory.lawMapProdFst/Snd, SALD.generalMovingTargetDiscreteEmJointEndpointMeasureMapOfNamedInterpolation, and SALD.generalMovingTargetDiscreteEmJointEndpointMarginalLawsOfNamedInterpolation are added as formalized local endpoint-law bookkeeping in this cycle; analytic backends remain sourceCited or obligation-level.",
    "The lower packet is the conditional-law/Fokker-Planck backend over appendix.tex:1358-1387, not a new theorem statement or broad SLT/SDE port.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

/-- Cycle-63 middle obligation tying the route audit to the next lower
conditional-law/Fokker--Planck packet. -/