AutoSamplingTheory.SALD.cycle66DiscreteForwardKlSkeletonMiddleContract

Data definition / provenance and workflow record

Meaning and type

The result has data type AutoSamplingTheory.SALD.DiscreteForwardKlEmDefectAccumulationMiddleContract. A value of this type stores descriptions; it is not a proof of the statements in those descriptions.

def cycle66DiscreteForwardKlSkeletonMiddleContract :
    DiscreteForwardKlEmDefectAccumulationMiddleContract

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.

sourceStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlDiscreteSource — audited data reference, not expanded and not a compiled dependency edge

interpolationSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlDiscreteInterpolationSource — audited data reference, not expanded and not a compiled dependency edge

derivativeSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlDiscreteDerivativeSource — audited data reference, not expanded and not a compiled dependency edge

gronwallSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlDiscreteGronwallSource — audited data reference, not expanded and not a compiled dependency edge

accumulatedSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlDiscreteAccumulatedErrorSource — 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 66 middle: audit the post-cycle-65 thm:forward-KL-discrete route against main_body.tex:299-323 and appendix.tex:260-592, verify that the theorem consumes explicit source-cited EM/Fokker-Planck, LSI/KL/FI, DV, Gronwall, and accumulated-error interfaces in paper order, and keep lower work on sald.discrete_forward_kl.accumulated_error_bridge over appendix.tex:557-592 plus main_body.tex:309-323.

sourceStepMap : List String (explicit)

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

Ordered data items

1. main_body.tex:299-323 fixes the linear-slowdown statement: inherited thm:forward-KL assumptions, score Lipschitz hypotheses, alpha0' finite score and 1+M complexities, 4*eta^2*L_space^2<1/2, alpha in (0,alpha0), alpha' in (0,alpha0'], and the exact terminal constants.
2. appendix.tex:260-385 supplies the frozen EM interpolation, endpoint laws, conditional drift, conditional Fokker-Planck equation, Laplacian split, and stitched interval setup; cycle 66 middle keeps these as named obligations and does not attempt the EM backend.
3. appendix.tex:388-491 is consumed through the existing discrete KL derivative, frozen-cross, moving Young, and LSI/KL/FI scalar handoff route.
4. appendix.tex:493-523 is consumed through the discrete DV witness with nu=hat rho_s, mu=tilde pi_s, and Z=alpha*||v_{t(s)}||^2, preserving the dot t(s)^2 coefficient.
5. appendix.tex:526-553 is consumed through the cycle-56 post-DV s-to-t derivative wrapper and pointwise Gronwall input.
6. appendix.tex:557-592 gives the Gronwall output; main_body.tex:309-323 is reached only after endpoint stitching, linear-slowdown exponent splitting, barGamma/barDelta identification, and A_alpha collection.

leanStepMap : List String (explicit)

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

Ordered data items

1. Keep SALD.discreteForwardKlStatementContract and SALD.discreteSaldContract unchanged and contractOnly.
2. Use SALD.cycle66DiscreteForwardKlSkeletonUpperPacket, SALD.cycle66DiscreteForwardKlSkeletonObligation, SALD.cycle65ForwardKlSkeletonMiddleObligation, SALD.cycle61DiscreteForwardKlSkeletonMiddleObligation, SALD.cycle61DiscreteForwardKlAccumulatedErrorLowerObligation, and SALD.cycle56DiscreteForwardKlGronwallLowerObligation as parent route checks.
3. Route appendix.tex:260-385 through SALD.discreteForwardKlEmInterpolationSideConditionContract, sald.discrete_forward_kl.em_endpoint_laws, sald.discrete_forward_kl.conditional_drift_density, sald.discrete_forward_kl.em_conditional_fokker_planck, sald.discrete_forward_kl.stitched_interval_regularity, and sald.discrete_forward_kl.em_interpolation_fp.
4. Route appendix.tex:388-491 through SALD.discreteForwardKlDerivativeCandidateContract, SALD.discreteForwardKlDerivativeObligation, SALD.cycle51DiscreteForwardKlDerivativeLowerObligation, SALD.frozenDeltaCrossLipSaldContract, sald.discrete_forward_kl.frozen_delta_cross_lip, SALD.saldLsiKlFiDensityTestContract, and probability.lsi_to_kl_fi.
5. Route appendix.tex:493-523 through dvVariationalFormulaInterface saldDvVariationSource, SALD.saldDvFiniteLogMgfContract, SALD.discreteForwardKlDvFiniteLogMgfWitnessContract, sald.discrete_forward_kl.dv_finite_log_mgf_witness, and sald.discrete_forward_kl.dv_velocity_bound.
6. Route appendix.tex:526-553 through SALD.discreteForwardKlPostDvTimeChangedDerivativeScalar, SALD.discreteForwardKlPointwiseGronwallInputOfPostDvTimeChanged, SALD.discreteForwardKlGronwallInstantiationContract, and sald.discrete_forward_kl.gronwall_accumulation.
7. Route appendix.tex:557-592 and main_body.tex:309-323 through SALD.discreteForwardKlAccumulatedErrorBridgeContract, SALD.discreteForwardKlAccumulatedErrorBridgeObligation, SALD.discreteForwardKlGronwallInitialExponentSplitOfPieces, SALD.discreteForwardKlResidualExponentBoundScalar, SALD.discreteForwardKlResidualExpBoundScalar, SALD.discreteForwardKlAlphaComplexityCollectionScalar, SALD.discreteForwardKlDeltaAccumulationScalar, SALD.discreteForwardKlAccumulatedErrorCollectionScalar, SALD.discreteForwardKlResidualIntegralDisplayBoundScalar, SALD.discreteForwardKlMainDisplayBoundScalar, sald.discrete_forward_kl.linear_slowdown_specialization, sald.discrete_forward_kl.residual_exponent_bound, and sald.discrete_forward_kl.accumulated_error_bridge.
8. Select lower work on the accumulated-error bridge, not on EM conditional-FP, KL differentiation, LSI/KL/FI, DV, or a new scalar side lemma.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. EM endpoint/conditional-law Fokker-Planck remains a source-cited obligation interface; cycle 66 middle does not prove Brownian construction, regular conditional laws, density/AC, weak FP, boundary integration by parts, or endpoint stitching.
2. eq:LSI-KL-FI remains the density-test, zero-set convention, admissible sqrt-density test or approximation, entropy-identity, finite KL/FI, and Fisher-chain obligation.
3. lem:dv_variation remains source-cited with common-space, absolute-continuity, finite-KL, selected-test measurability, finite-log-mgf, and positive-alpha witnesses.
4. lem:gronwall remains the endpoint-safe differentiability/FTC, coefficient-regularity, interval-integrability, endpoint-evaluation, and exponent-rewrite obligation; cycle 56 only supplies the pointwise source-shaped input.
5. The continuous forward-KL derivative route from cycle 65 remains sibling context for inherited assumptions and does not close any discrete EM or accumulated-error backend.

obligations : List String (explicit)

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

Ordered data items

1. sald.discrete_forward_kl.cycle66_discrete_route
2. sald.discrete_forward_kl.cycle66_middle_route_audit
3. sald.discrete_forward_kl.em_endpoint_laws
4. sald.discrete_forward_kl.conditional_drift_density
5. sald.discrete_forward_kl.em_conditional_fokker_planck
6. sald.discrete_forward_kl.stitched_interval_regularity
7. sald.discrete_forward_kl.em_interpolation_fp
8. sald.discrete_forward_kl.kl_derivative
9. sald.discrete_forward_kl.frozen_delta_cross_lip
10. probability.lsi_to_kl_fi
11. sald.discrete_forward_kl.dv_finite_log_mgf_witness
12. sald.discrete_forward_kl.dv_velocity_bound
13. sald.discrete_forward_kl.gronwall_accumulation
14. sald.discrete_forward_kl.linear_slowdown_specialization
15. sald.discrete_forward_kl.residual_exponent_bound
16. sald.discrete_forward_kl.accumulated_error_bridge

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.discreteForwardKlAccumulatedErrorBridgeContract / SALD.discreteForwardKlAccumulatedErrorBridgeObligation / sald.discrete_forward_kl.accumulated_error_bridge.
2. First lower sub-slice: appendix.tex:557-592 endpoint and Gronwall-output stitching from the supplied cycle-56 pointwise derivative input and SALD.discreteForwardKlGronwallInstantiationContract.
3. Second lower sub-slice: linear slowdown t(s)=s/r, dot{s}=r, and exponent collection, preserving exp(-r*int C_LSI), T/(r*alpha), and 2*r*eta^2*barGamma/alpha'.
4. Third lower sub-slice: collect the residual integral into (1/r)*A_alpha(pi,v) plus 2*r*eta*barDelta_{alpha'} using SALD.discreteForwardKlAlphaComplexityCollectionScalar, SALD.discreteForwardKlDeltaAccumulationScalar, SALD.discreteForwardKlAccumulatedErrorCollectionScalar, and SALD.discreteForwardKlResidualIntegralDisplayBoundScalar.
5. Cycle 66 lower sub-slice: combine the supplied initial Gronwall split and supplied residual display into the exact main-body two-term bound using SALD.discreteForwardKlMainDisplayBoundScalar.
6. If blocked, sharpen endpoint-law stitching, coefficient regularity, interval-integrability, barGamma/barDelta definitions, finite-log-mgf witnesses, or residual-exponent obligations rather than changing thm:forward-KL-discrete.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.discreteSaldContract lists SALD.cycle66DiscreteForwardKlSkeletonMiddleObligation while remaining contractOnly.
2. SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle66_middle_route_audit between the cycle-66 route and lower accumulated-error packet.
3. SALD.saldDependenciesForLabel "thm:forward-KL-discrete" includes SALD.cycle66DiscreteForwardKlSkeletonMiddleContract, SALD.cycle66DiscreteForwardKlSkeletonMiddleObligation, and sald.discrete_forward_kl.cycle66_middle_route_audit.
4. No theorem statement, source constant, source label, source-file selection, theorem status, SLT reuse status, or analytic backend status is changed.
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 cycle66DiscreteForwardKlSkeletonMiddleContract :
    DiscreteForwardKlEmDefectAccumulationMiddleContract where
  sourceStatement := saldForwardKlDiscreteSource
  interpolationSource := saldForwardKlDiscreteInterpolationSource
  derivativeSource := saldForwardKlDiscreteDerivativeSource
  gronwallSource := saldForwardKlDiscreteGronwallSource
  accumulatedSource := saldForwardKlDiscreteAccumulatedErrorSource
  objective := "Cycle 66 middle: audit the post-cycle-65 thm:forward-KL-discrete route against main_body.tex:299-323 and appendix.tex:260-592, verify that the theorem consumes explicit source-cited EM/Fokker-Planck, LSI/KL/FI, DV, Gronwall, and accumulated-error interfaces in paper order, and keep lower work on sald.discrete_forward_kl.accumulated_error_bridge over appendix.tex:557-592 plus main_body.tex:309-323."
  sourceStepMap := [
    "main_body.tex:299-323 fixes the linear-slowdown statement: inherited thm:forward-KL assumptions, score Lipschitz hypotheses, alpha0' finite score and 1+M complexities, 4*eta^2*L_space^2<1/2, alpha in (0,alpha0), alpha' in (0,alpha0'], and the exact terminal constants.",
    "appendix.tex:260-385 supplies the frozen EM interpolation, endpoint laws, conditional drift, conditional Fokker-Planck equation, Laplacian split, and stitched interval setup; cycle 66 middle keeps these as named obligations and does not attempt the EM backend.",
    "appendix.tex:388-491 is consumed through the existing discrete KL derivative, frozen-cross, moving Young, and LSI/KL/FI scalar handoff route.",
    "appendix.tex:493-523 is consumed through the discrete DV witness with nu=hat rho_s, mu=tilde pi_s, and Z=alpha*||v_{t(s)}||^2, preserving the dot t(s)^2 coefficient.",
    "appendix.tex:526-553 is consumed through the cycle-56 post-DV s-to-t derivative wrapper and pointwise Gronwall input.",
    "appendix.tex:557-592 gives the Gronwall output; main_body.tex:309-323 is reached only after endpoint stitching, linear-slowdown exponent splitting, barGamma/barDelta identification, and A_alpha collection."
  ]
  leanStepMap := [
    "Keep SALD.discreteForwardKlStatementContract and SALD.discreteSaldContract unchanged and contractOnly.",
    "Use SALD.cycle66DiscreteForwardKlSkeletonUpperPacket, SALD.cycle66DiscreteForwardKlSkeletonObligation, SALD.cycle65ForwardKlSkeletonMiddleObligation, SALD.cycle61DiscreteForwardKlSkeletonMiddleObligation, SALD.cycle61DiscreteForwardKlAccumulatedErrorLowerObligation, and SALD.cycle56DiscreteForwardKlGronwallLowerObligation as parent route checks.",
    "Route appendix.tex:260-385 through SALD.discreteForwardKlEmInterpolationSideConditionContract, sald.discrete_forward_kl.em_endpoint_laws, sald.discrete_forward_kl.conditional_drift_density, sald.discrete_forward_kl.em_conditional_fokker_planck, sald.discrete_forward_kl.stitched_interval_regularity, and sald.discrete_forward_kl.em_interpolation_fp.",
    "Route appendix.tex:388-491 through SALD.discreteForwardKlDerivativeCandidateContract, SALD.discreteForwardKlDerivativeObligation, SALD.cycle51DiscreteForwardKlDerivativeLowerObligation, SALD.frozenDeltaCrossLipSaldContract, sald.discrete_forward_kl.frozen_delta_cross_lip, SALD.saldLsiKlFiDensityTestContract, and probability.lsi_to_kl_fi.",
    "Route appendix.tex:493-523 through dvVariationalFormulaInterface saldDvVariationSource, SALD.saldDvFiniteLogMgfContract, SALD.discreteForwardKlDvFiniteLogMgfWitnessContract, sald.discrete_forward_kl.dv_finite_log_mgf_witness, and sald.discrete_forward_kl.dv_velocity_bound.",
    "Route appendix.tex:526-553 through SALD.discreteForwardKlPostDvTimeChangedDerivativeScalar, SALD.discreteForwardKlPointwiseGronwallInputOfPostDvTimeChanged, SALD.discreteForwardKlGronwallInstantiationContract, and sald.discrete_forward_kl.gronwall_accumulation.",
    "Route appendix.tex:557-592 and main_body.tex:309-323 through SALD.discreteForwardKlAccumulatedErrorBridgeContract, SALD.discreteForwardKlAccumulatedErrorBridgeObligation, SALD.discreteForwardKlGronwallInitialExponentSplitOfPieces, SALD.discreteForwardKlResidualExponentBoundScalar, SALD.discreteForwardKlResidualExpBoundScalar, SALD.discreteForwardKlAlphaComplexityCollectionScalar, SALD.discreteForwardKlDeltaAccumulationScalar, SALD.discreteForwardKlAccumulatedErrorCollectionScalar, SALD.discreteForwardKlResidualIntegralDisplayBoundScalar, SALD.discreteForwardKlMainDisplayBoundScalar, sald.discrete_forward_kl.linear_slowdown_specialization, sald.discrete_forward_kl.residual_exponent_bound, and sald.discrete_forward_kl.accumulated_error_bridge.",
    "Select lower work on the accumulated-error bridge, not on EM conditional-FP, KL differentiation, LSI/KL/FI, DV, or a new scalar side lemma."
  ]
  citedResultInterfaces := [
    "EM endpoint/conditional-law Fokker-Planck remains a source-cited obligation interface; cycle 66 middle does not prove Brownian construction, regular conditional laws, density/AC, weak FP, boundary integration by parts, or endpoint stitching.",
    "eq:LSI-KL-FI remains the density-test, zero-set convention, admissible sqrt-density test or approximation, entropy-identity, finite KL/FI, and Fisher-chain obligation.",
    "lem:dv_variation remains source-cited with common-space, absolute-continuity, finite-KL, selected-test measurability, finite-log-mgf, and positive-alpha witnesses.",
    "lem:gronwall remains the endpoint-safe differentiability/FTC, coefficient-regularity, interval-integrability, endpoint-evaluation, and exponent-rewrite obligation; cycle 56 only supplies the pointwise source-shaped input.",
    "The continuous forward-KL derivative route from cycle 65 remains sibling context for inherited assumptions and does not close any discrete EM or accumulated-error backend."
  ]
  obligations := [
    "sald.discrete_forward_kl.cycle66_discrete_route",
    "sald.discrete_forward_kl.cycle66_middle_route_audit",
    "sald.discrete_forward_kl.em_endpoint_laws",
    "sald.discrete_forward_kl.conditional_drift_density",
    "sald.discrete_forward_kl.em_conditional_fokker_planck",
    "sald.discrete_forward_kl.stitched_interval_regularity",
    "sald.discrete_forward_kl.em_interpolation_fp",
    "sald.discrete_forward_kl.kl_derivative",
    "sald.discrete_forward_kl.frozen_delta_cross_lip",
    "probability.lsi_to_kl_fi",
    "sald.discrete_forward_kl.dv_finite_log_mgf_witness",
    "sald.discrete_forward_kl.dv_velocity_bound",
    "sald.discrete_forward_kl.gronwall_accumulation",
    "sald.discrete_forward_kl.linear_slowdown_specialization",
    "sald.discrete_forward_kl.residual_exponent_bound",
    "sald.discrete_forward_kl.accumulated_error_bridge"
  ]
  lowerPacket := [
    "Target exactly SALD.discreteForwardKlAccumulatedErrorBridgeContract / SALD.discreteForwardKlAccumulatedErrorBridgeObligation / sald.discrete_forward_kl.accumulated_error_bridge.",
    "First lower sub-slice: appendix.tex:557-592 endpoint and Gronwall-output stitching from the supplied cycle-56 pointwise derivative input and SALD.discreteForwardKlGronwallInstantiationContract.",
    "Second lower sub-slice: linear slowdown t(s)=s/r, dot{s}=r, and exponent collection, preserving exp(-r*int C_LSI), T/(r*alpha), and 2*r*eta^2*barGamma/alpha'.",
    "Third lower sub-slice: collect the residual integral into (1/r)*A_alpha(pi,v) plus 2*r*eta*barDelta_{alpha'} using SALD.discreteForwardKlAlphaComplexityCollectionScalar, SALD.discreteForwardKlDeltaAccumulationScalar, SALD.discreteForwardKlAccumulatedErrorCollectionScalar, and SALD.discreteForwardKlResidualIntegralDisplayBoundScalar.",
    "Cycle 66 lower sub-slice: combine the supplied initial Gronwall split and supplied residual display into the exact main-body two-term bound using SALD.discreteForwardKlMainDisplayBoundScalar.",
    "If blocked, sharpen endpoint-law stitching, coefficient regularity, interval-integrability, barGamma/barDelta definitions, finite-log-mgf witnesses, or residual-exponent obligations rather than changing thm:forward-KL-discrete."
  ]
  reviewerChecklist := [
    "SALD.discreteSaldContract lists SALD.cycle66DiscreteForwardKlSkeletonMiddleObligation while remaining contractOnly.",
    "SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle66_middle_route_audit between the cycle-66 route and lower accumulated-error packet.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL-discrete\" includes SALD.cycle66DiscreteForwardKlSkeletonMiddleContract, SALD.cycle66DiscreteForwardKlSkeletonMiddleObligation, and sald.discrete_forward_kl.cycle66_middle_route_audit.",
    "No theorem statement, source constant, source label, source-file selection, theorem status, SLT reuse status, or analytic backend status is changed.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

/-- Cycle-66 middle obligation tying the post-cycle-65 discrete route to the
accumulated-error bridge lower packet. -/