AutoSamplingTheory.SALD.cycle56DiscreteForwardKlSkeletonMiddleContract

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 cycle56DiscreteForwardKlSkeletonMiddleContract :
    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 56 middle: audit the upper thm:forward-KL-discrete route against main_body.tex:299-323 and appendix.tex:260-592, verify that EM/Fokker-Planck is consumed only through named source-cited interfaces, and select sald.discrete_forward_kl.gronwall_accumulation over appendix.tex:526-592 as the next lower backend.

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 theorem display: linear slowdown t(s)=s/r, inherited forward-KL assumptions, score Lipschitz assumptions, alpha0' finite score and 1+M complexities, the 4*eta^2*L_space^2<1/2 step-size condition, and the exact T/(r*alpha), 2*r*eta^2*barGamma/alpha', r^(-1)*A_alpha, and 2*r*eta*barDelta constants.
2. appendix.tex:260-385 supplies the EM interpolation, endpoint law identities, conditional frozen drift, conditional-drift Fokker-Planck equation, Laplacian split, and stitched interval inputs; all remain named obligations or source-cited interfaces.
3. appendix.tex:388-491 is already routed through the cycle-51 derivative/LSI scalar handoff: EM-FP derivative input, frozen-cross quarter-FI bound, moving Young quarter-FI bound, and eq:LSI-KL-FI.
4. appendix.tex:493-523 is already routed through the discrete DV velocity witness with nu=hat rho_s, mu=tilde pi_s, and Z=alpha*||v_{t(s)}||^2.
5. appendix.tex:526-553 changes from s to t and produces the exact source coefficient dot{s}(t)*C_LSI(t)-dot{s}(t)^(-1)*alpha^(-1)-2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t).
6. appendix.tex:557-592 applies lem:gronwall to the general-schedule inequality and is the selected lower backend before the downstream linear-slowdown accumulated-error bridge to the main-body display.

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.cycle54MainSkeletonAnalyticMiddleObligation, SALD.cycle55ForwardKlSkeletonMiddleObligation, SALD.cycle51DiscreteForwardKlSkeletonMiddleObligation, and SALD.cycle56DiscreteForwardKlSkeletonObligation 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.cycle51DiscreteForwardKlDerivativeLowerObligation, SALD.discreteForwardKlPostLsiDerivativeBoundScalar, SALD.discreteForwardKlPostLsiDerivativeBoundOfKlFiScalar, SALD.frozenDeltaCrossLipSaldContract, and SALD.saldLsiKlFiDensityTestContract.
5. Route appendix.tex:493-523 through dvVariationalFormulaInterface saldDvVariationSource, SALD.discreteForwardKlDvFiniteLogMgfWitnessContract, sald.discrete_forward_kl.dv_finite_log_mgf_witness, and sald.discrete_forward_kl.dv_velocity_bound.
6. Route appendix.tex:526-592 through SALD.discreteForwardKlGronwallInstantiationContract, SALD.discreteForwardKlGronwallAccumulationObligation, sald.discrete_forward_kl.gronwall_accumulation, SALD.discreteForwardKlAccumulatedErrorBridgeContract, and sald.discrete_forward_kl.accumulated_error_bridge.
7. Select the next lower target as SALD.discreteForwardKlGronwallInstantiationContract / SALD.discreteForwardKlGronwallAccumulationObligation / sald.discrete_forward_kl.gronwall_accumulation, using the derivative and DV outputs as explicit hypotheses.

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; this middle audit does not prove Brownian construction, disintegration, density/AC, weak FP, or endpoint stitching.
2. eq:LSI-KL-FI remains the density-test, zero-set, admissibility, entropy-identity, finite KL/FI, and Fisher-chain obligation consumed by the cycle-51 scalar handoff.
3. lem:dv_variation remains source-cited and theorem-specific common-space, absolute-continuity, finite-KL/log-mgf, measurability, and positive-alpha witnesses remain obligations.
4. lem:gronwall remains the endpoint-safe differentiability/FTC, stitched-interval, coefficient-regularity, and exponent-rewrite obligation selected for lower work.
5. The continuous forward-KL cycle-55 mass handoff is route context only; it is not used to promote the discrete KL derivative or theorem statement.

obligations : List String (explicit)

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

Ordered data items

1. sald.discrete_forward_kl.cycle56_theorem_interface_route
2. sald.discrete_forward_kl.cycle56_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.discreteForwardKlGronwallInstantiationContract / SALD.discreteForwardKlGronwallAccumulationObligation / sald.discrete_forward_kl.gronwall_accumulation.
2. First lower sub-slice: consume sald.discrete_forward_kl.kl_derivative and sald.discrete_forward_kl.dv_velocity_bound through SALD.discreteForwardKlPostDvTimeChangedDerivativeScalar and SALD.discreteForwardKlPointwiseGronwallInputOfPostDvTimeChanged to instantiate the source K'(t) <= -a(t)*K(t)+b(t) inequality from appendix.tex:526-553.
3. Second lower sub-slice: expose stitched endpoint side conditions K(0)=KL(rho_0||pi_0), K(T)=KL(rho_K^eta||pi_T), and interval compatibility across EM steps as named assumptions, not theorem hypotheses.
4. Third lower sub-slice: apply the existing Gronwall endpoint/FTC interface to obtain the appendix general-schedule display before the linear-slowdown collection.
5. Leave linear slowdown, residual exponent, barGamma/barDelta collection, EM conditional-FP, frozen-defect specialization, LSI/KL/FI, and DV finite-log-mgf as separate named interfaces unless their exact backends compile locally.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.discreteSaldContract lists SALD.cycle56DiscreteForwardKlSkeletonMiddleObligation while remaining contractOnly.
2. SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle56_middle_route_audit immediately after the cycle-56 theorem route.
3. SALD.saldDependenciesForLabel "thm:forward-KL-discrete" includes SALD.cycle56DiscreteForwardKlSkeletonMiddleContract, SALD.cycle56DiscreteForwardKlSkeletonMiddleObligation, and sald.discrete_forward_kl.cycle56_middle_route_audit.
4. No EM/Fokker-Planck, KL derivative, frozen-defect, LSI, DV, Gronwall, accumulated-error, or theorem statement 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 cycle56DiscreteForwardKlSkeletonMiddleContract :
    DiscreteForwardKlEmDefectAccumulationMiddleContract where
  sourceStatement := saldForwardKlDiscreteSource
  interpolationSource := saldForwardKlDiscreteInterpolationSource
  derivativeSource := saldForwardKlDiscreteDerivativeSource
  gronwallSource := saldForwardKlDiscreteGronwallSource
  accumulatedSource := saldForwardKlDiscreteAccumulatedErrorSource
  objective := "Cycle 56 middle: audit the upper thm:forward-KL-discrete route against main_body.tex:299-323 and appendix.tex:260-592, verify that EM/Fokker-Planck is consumed only through named source-cited interfaces, and select sald.discrete_forward_kl.gronwall_accumulation over appendix.tex:526-592 as the next lower backend."
  sourceStepMap := [
    "main_body.tex:299-323 fixes the theorem display: linear slowdown t(s)=s/r, inherited forward-KL assumptions, score Lipschitz assumptions, alpha0' finite score and 1+M complexities, the 4*eta^2*L_space^2<1/2 step-size condition, and the exact T/(r*alpha), 2*r*eta^2*barGamma/alpha', r^(-1)*A_alpha, and 2*r*eta*barDelta constants.",
    "appendix.tex:260-385 supplies the EM interpolation, endpoint law identities, conditional frozen drift, conditional-drift Fokker-Planck equation, Laplacian split, and stitched interval inputs; all remain named obligations or source-cited interfaces.",
    "appendix.tex:388-491 is already routed through the cycle-51 derivative/LSI scalar handoff: EM-FP derivative input, frozen-cross quarter-FI bound, moving Young quarter-FI bound, and eq:LSI-KL-FI.",
    "appendix.tex:493-523 is already routed through the discrete DV velocity witness with nu=hat rho_s, mu=tilde pi_s, and Z=alpha*||v_{t(s)}||^2.",
    "appendix.tex:526-553 changes from s to t and produces the exact source coefficient dot{s}(t)*C_LSI(t)-dot{s}(t)^(-1)*alpha^(-1)-2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t).",
    "appendix.tex:557-592 applies lem:gronwall to the general-schedule inequality and is the selected lower backend before the downstream linear-slowdown accumulated-error bridge to the main-body display."
  ]
  leanStepMap := [
    "Keep SALD.discreteForwardKlStatementContract and SALD.discreteSaldContract unchanged and contractOnly.",
    "Use SALD.cycle54MainSkeletonAnalyticMiddleObligation, SALD.cycle55ForwardKlSkeletonMiddleObligation, SALD.cycle51DiscreteForwardKlSkeletonMiddleObligation, and SALD.cycle56DiscreteForwardKlSkeletonObligation 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.cycle51DiscreteForwardKlDerivativeLowerObligation, SALD.discreteForwardKlPostLsiDerivativeBoundScalar, SALD.discreteForwardKlPostLsiDerivativeBoundOfKlFiScalar, SALD.frozenDeltaCrossLipSaldContract, and SALD.saldLsiKlFiDensityTestContract.",
    "Route appendix.tex:493-523 through dvVariationalFormulaInterface saldDvVariationSource, SALD.discreteForwardKlDvFiniteLogMgfWitnessContract, sald.discrete_forward_kl.dv_finite_log_mgf_witness, and sald.discrete_forward_kl.dv_velocity_bound.",
    "Route appendix.tex:526-592 through SALD.discreteForwardKlGronwallInstantiationContract, SALD.discreteForwardKlGronwallAccumulationObligation, sald.discrete_forward_kl.gronwall_accumulation, SALD.discreteForwardKlAccumulatedErrorBridgeContract, and sald.discrete_forward_kl.accumulated_error_bridge.",
    "Select the next lower target as SALD.discreteForwardKlGronwallInstantiationContract / SALD.discreteForwardKlGronwallAccumulationObligation / sald.discrete_forward_kl.gronwall_accumulation, using the derivative and DV outputs as explicit hypotheses."
  ]
  citedResultInterfaces := [
    "EM endpoint/conditional-law Fokker-Planck remains a source-cited obligation interface; this middle audit does not prove Brownian construction, disintegration, density/AC, weak FP, or endpoint stitching.",
    "eq:LSI-KL-FI remains the density-test, zero-set, admissibility, entropy-identity, finite KL/FI, and Fisher-chain obligation consumed by the cycle-51 scalar handoff.",
    "lem:dv_variation remains source-cited and theorem-specific common-space, absolute-continuity, finite-KL/log-mgf, measurability, and positive-alpha witnesses remain obligations.",
    "lem:gronwall remains the endpoint-safe differentiability/FTC, stitched-interval, coefficient-regularity, and exponent-rewrite obligation selected for lower work.",
    "The continuous forward-KL cycle-55 mass handoff is route context only; it is not used to promote the discrete KL derivative or theorem statement."
  ]
  obligations := [
    "sald.discrete_forward_kl.cycle56_theorem_interface_route",
    "sald.discrete_forward_kl.cycle56_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.discreteForwardKlGronwallInstantiationContract / SALD.discreteForwardKlGronwallAccumulationObligation / sald.discrete_forward_kl.gronwall_accumulation.",
    "First lower sub-slice: consume sald.discrete_forward_kl.kl_derivative and sald.discrete_forward_kl.dv_velocity_bound through SALD.discreteForwardKlPostDvTimeChangedDerivativeScalar and SALD.discreteForwardKlPointwiseGronwallInputOfPostDvTimeChanged to instantiate the source K'(t) <= -a(t)*K(t)+b(t) inequality from appendix.tex:526-553.",
    "Second lower sub-slice: expose stitched endpoint side conditions K(0)=KL(rho_0||pi_0), K(T)=KL(rho_K^eta||pi_T), and interval compatibility across EM steps as named assumptions, not theorem hypotheses.",
    "Third lower sub-slice: apply the existing Gronwall endpoint/FTC interface to obtain the appendix general-schedule display before the linear-slowdown collection.",
    "Leave linear slowdown, residual exponent, barGamma/barDelta collection, EM conditional-FP, frozen-defect specialization, LSI/KL/FI, and DV finite-log-mgf as separate named interfaces unless their exact backends compile locally."
  ]
  reviewerChecklist := [
    "SALD.discreteSaldContract lists SALD.cycle56DiscreteForwardKlSkeletonMiddleObligation while remaining contractOnly.",
    "SALD.discreteForwardKlProofDag contains ASTIS.SALD.forward_KL_discrete.cycle56_middle_route_audit immediately after the cycle-56 theorem route.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL-discrete\" includes SALD.cycle56DiscreteForwardKlSkeletonMiddleContract, SALD.cycle56DiscreteForwardKlSkeletonMiddleObligation, and sald.discrete_forward_kl.cycle56_middle_route_audit.",
    "No EM/Fokker-Planck, KL derivative, frozen-defect, LSI, DV, Gronwall, accumulated-error, or theorem statement status is promoted.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

/-- Cycle-56 middle obligation tying the discrete route audit to the selected
Gronwall lower packet. -/