AutoSamplingTheory.SALD.cycle65ForwardKlSkeletonMiddleContract

Data definition / provenance and workflow record

Meaning and type

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

def cycle65ForwardKlSkeletonMiddleContract :
    ForwardKlMiddleSourceToLeanContract

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.saldForwardKlSource — audited data reference, not expanded and not a compiled dependency edge

sourceProof : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

derivativeSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

dvSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

gronwallSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlGronwallSource — 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 65 middle: synchronize the post-cycle-64 continuous thm:forward-KL route against main_body.tex:238-247 and appendix.tex:164-252, verify that the upper packet consumes the five source-cited analytic interfaces in paper order, and keep the lower packet exactly on SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative over appendix.tex:168-228 without changing constants, statements, source labels, or backend statuses.

sourceStepMap : List String (explicit)

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

Ordered data items

1. main_body.tex:238-247 fixes the theorem display: LSI constants C_LSI(t)>=0, finite alpha0-complexity for the transport velocity v_t, alpha in (0,alpha0], SALD law rho_s, the initial KL factor exp(-int dot{s} C_LSI)*exp(int (1/2)*dot{s}^(-1)*alpha^(-1)), and the residual alpha-complexity integral.
2. appendix.tex:168-185 differentiates KL(rho_s||tilde pi_s), uses int partial_s rho_s dx=0, substitutes the SALD Fokker--Planck equation, integrates by parts, and identifies the first term with -FI.
3. appendix.tex:187-208 defines tilde v_s=dot t(s)*v_{t(s)}, proves it transports tilde pi_s, evaluates the target-time term by integration by parts, and applies Cauchy--Schwarz/Young with the exact one-half coefficient.
4. appendix.tex:210-228 combines the derivative identity with eq:LSI-KL-FI and the inverse-schedule chain rule to obtain the t-time inequality with residual coefficient (1/2)*dot{s}(t)^(-1)*||v_t||^2.
5. appendix.tex:230-241 applies lem:dv_variation to Z=alpha*||v_t||^2, using the theorem's finite-log-mgf assumption through the alpha-complexity interface, and produces the pre-Gronwall coefficient dot{s}(t)*C_LSI(t)-(1/2)*dot{s}(t)^(-1)*alpha^(-1).
6. appendix.tex:244-252 applies lem:gronwall and then performs the source exponent split and nonnegative-LSI residual exponent drop that match the theorem display.

leanStepMap : List String (explicit)

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

Ordered data items

1. Use SALD.cycle65ForwardKlSkeletonUpperPacket and SALD.cycle65ForwardKlSkeletonObligation as parent route data after the accepted cycle-64 analytic-interface pass.
2. Keep SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract contractOnly; this middle audit adds no theorem hypotheses and changes no theorem display.
3. Route appendix.tex:168-228 through SALD.forwardKlDerivativeCandidateContract, SALD.forwardKlDerivativeSideConditionContract, SALD.forwardKlDerivativeObligation, SALD.forwardKlDensityBoundaryObligation, SALD.forwardKlScheduleTimeChangeObligation, sald.forward_kl.density_boundary_regular, sald.forward_kl.schedule_time_change, and sald.forward_kl.kl_derivative.
4. Consume SALD.forwardKlPreDvDerivativeBoundOfRawKlFiVelocityScalingScalar and the pointwise wrapper SALD.forwardKlPointwisePreDvDerivativeBoundOfRawKlFiVelocityScaling only after the raw derivative split, mass-conservation input, LSI comparison, slowed-velocity scaling, and inverse-schedule identity are supplied explicitly.
5. Route appendix.tex:210-217 through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi, preserving density, zero-set convention, admissible sqrt-density test or approximation, entropy identity, finite KL/FI, and Fisher chain-rule obligations.
6. Route appendix.tex:230-241 through dvVariationalFormulaInterface saldDvVariationSource, SALD.saldDvFiniteLogMgfContract, SALD.forwardKlDvFiniteLogMgfWitnessContract, sald.forward_kl.dv_finite_log_mgf_witness, and sald.forward_kl.dv_energy_bound.
7. Route appendix.tex:244-252 through SALD.saldGronwallEndpointCalculusContract, SALD.forwardKlGronwallInstantiationContract, SALD.forwardKlGronwallSideConditionContract, sald.forward_kl.endpoint_schedule_identities, sald.forward_kl.gronwall_side_conditions, and sald.forward_kl.gronwall_application.
8. Keep SALD.discreteForwardKlEmInterpolationSideConditionContract and sald.discrete_forward_kl.em_interpolation_fp visible only as downstream discrete sibling interfaces, not hidden assumptions of thm:forward-KL.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. lem:gronwall remains an obligation with endpoint-safe differentiability/FTC, interval-integrability, coefficient regularity, endpoint rewrites, exponent splitting, and theorem-display matching.
2. lem:dv_variation remains source-cited with common-space, absolute-continuity, finite-KL, selected-test measurability, finite-log-mgf, and positive-alpha scaling witnesses.
3. eq:LSI-KL-FI remains an obligation for density, zero-set convention, admissible sqrt-density test or approximation, entropy identity, finite KL/FI, and Fisher chain rule.
4. The continuous Fokker--Planck/KL derivative identity remains the selected local SDE/measure-analysis backend, with mass conservation, boundary/no-flux, target transport, and schedule calculus still open.
5. The Euler--Maruyama interpolation Fokker--Planck endpoint/conditional-law backend remains a downstream discrete obligation and is not imported into the continuous theorem.

obligations : List String (explicit)

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

Ordered data items

1. sald.forward_kl.cycle65_continuous_route
2. sald.forward_kl.cycle65_middle_route_audit
3. sald.forward_kl.cycle65_derivative_pointwise_lower
4. sald.forward_kl.kl_derivative
5. sald.forward_kl.density_boundary_regular
6. sald.forward_kl.schedule_time_change
7. probability.lsi_to_kl_fi
8. sald.forward_kl.dv_finite_log_mgf_witness
9. sald.forward_kl.dv_energy_bound
10. sald.forward_kl.endpoint_schedule_identities
11. sald.forward_kl.gronwall_side_conditions
12. sald.forward_kl.gronwall_application
13. sald.discrete_forward_kl.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.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative.
2. First lower sub-slice: appendix.tex:168-185 mass conservation, differentiating KL under the integral, SALD Fokker--Planck substitution, boundary/no-flux integration by parts, and -FI identification.
3. Second lower sub-slice: appendix.tex:187-208 slowed target velocity, target integration by parts, Cauchy--Schwarz/Young with the exact 1/2 share, and the L2 velocity term.
4. Third lower sub-slice: appendix.tex:218-228 inverse-schedule chain rule, slowed-velocity square scaling, and dot{s}(t)*dot t(s(t))^2=dot{s}(t)^(-1), with the compiled pointwise wrapper producing the t-indexed pre-DV inequality.
5. Leave LSI/KL/FI, DV finite-log-mgf, Gronwall endpoint/exponent conditions, and EM interpolation as separate named interfaces unless their exact analytic backends compile locally.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.continuousSaldContract lists SALD.cycle65ForwardKlSkeletonMiddleObligation while remaining contractOnly.
2. SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle65_middle_route_audit after ASTIS.SALD.forward_KL.cycle65_continuous_route and before the selected lower-packet node.
3. SALD.saldDependenciesForLabel "thm:forward-KL" includes SALD.cycle65ForwardKlSkeletonMiddleContract, SALD.cycle65ForwardKlSkeletonMiddleObligation, and sald.forward_kl.cycle65_middle_route_audit.
4. No theorem statement, source coefficient, source label, source-file selection, SLT reuse entry, 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 cycle65ForwardKlSkeletonMiddleContract :
    ForwardKlMiddleSourceToLeanContract where
  sourceStatement := saldForwardKlSource
  sourceProof := saldForwardKlProofSource
  derivativeSource := saldForwardKlDerivativeSource
  dvSource := saldForwardKlDvEnergySource
  gronwallSource := saldForwardKlGronwallSource
  objective := "Cycle 65 middle: synchronize the post-cycle-64 continuous thm:forward-KL route against main_body.tex:238-247 and appendix.tex:164-252, verify that the upper packet consumes the five source-cited analytic interfaces in paper order, and keep the lower packet exactly on SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative over appendix.tex:168-228 without changing constants, statements, source labels, or backend statuses."
  sourceStepMap := [
    "main_body.tex:238-247 fixes the theorem display: LSI constants C_LSI(t)>=0, finite alpha0-complexity for the transport velocity v_t, alpha in (0,alpha0], SALD law rho_s, the initial KL factor exp(-int dot{s} C_LSI)*exp(int (1/2)*dot{s}^(-1)*alpha^(-1)), and the residual alpha-complexity integral.",
    "appendix.tex:168-185 differentiates KL(rho_s||tilde pi_s), uses int partial_s rho_s dx=0, substitutes the SALD Fokker--Planck equation, integrates by parts, and identifies the first term with -FI.",
    "appendix.tex:187-208 defines tilde v_s=dot t(s)*v_{t(s)}, proves it transports tilde pi_s, evaluates the target-time term by integration by parts, and applies Cauchy--Schwarz/Young with the exact one-half coefficient.",
    "appendix.tex:210-228 combines the derivative identity with eq:LSI-KL-FI and the inverse-schedule chain rule to obtain the t-time inequality with residual coefficient (1/2)*dot{s}(t)^(-1)*||v_t||^2.",
    "appendix.tex:230-241 applies lem:dv_variation to Z=alpha*||v_t||^2, using the theorem's finite-log-mgf assumption through the alpha-complexity interface, and produces the pre-Gronwall coefficient dot{s}(t)*C_LSI(t)-(1/2)*dot{s}(t)^(-1)*alpha^(-1).",
    "appendix.tex:244-252 applies lem:gronwall and then performs the source exponent split and nonnegative-LSI residual exponent drop that match the theorem display."
  ]
  leanStepMap := [
    "Use SALD.cycle65ForwardKlSkeletonUpperPacket and SALD.cycle65ForwardKlSkeletonObligation as parent route data after the accepted cycle-64 analytic-interface pass.",
    "Keep SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract contractOnly; this middle audit adds no theorem hypotheses and changes no theorem display.",
    "Route appendix.tex:168-228 through SALD.forwardKlDerivativeCandidateContract, SALD.forwardKlDerivativeSideConditionContract, SALD.forwardKlDerivativeObligation, SALD.forwardKlDensityBoundaryObligation, SALD.forwardKlScheduleTimeChangeObligation, sald.forward_kl.density_boundary_regular, sald.forward_kl.schedule_time_change, and sald.forward_kl.kl_derivative.",
    "Consume SALD.forwardKlPreDvDerivativeBoundOfRawKlFiVelocityScalingScalar and the pointwise wrapper SALD.forwardKlPointwisePreDvDerivativeBoundOfRawKlFiVelocityScaling only after the raw derivative split, mass-conservation input, LSI comparison, slowed-velocity scaling, and inverse-schedule identity are supplied explicitly.",
    "Route appendix.tex:210-217 through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi, preserving density, zero-set convention, admissible sqrt-density test or approximation, entropy identity, finite KL/FI, and Fisher chain-rule obligations.",
    "Route appendix.tex:230-241 through dvVariationalFormulaInterface saldDvVariationSource, SALD.saldDvFiniteLogMgfContract, SALD.forwardKlDvFiniteLogMgfWitnessContract, sald.forward_kl.dv_finite_log_mgf_witness, and sald.forward_kl.dv_energy_bound.",
    "Route appendix.tex:244-252 through SALD.saldGronwallEndpointCalculusContract, SALD.forwardKlGronwallInstantiationContract, SALD.forwardKlGronwallSideConditionContract, sald.forward_kl.endpoint_schedule_identities, sald.forward_kl.gronwall_side_conditions, and sald.forward_kl.gronwall_application.",
    "Keep SALD.discreteForwardKlEmInterpolationSideConditionContract and sald.discrete_forward_kl.em_interpolation_fp visible only as downstream discrete sibling interfaces, not hidden assumptions of thm:forward-KL."
  ]
  citedResultInterfaces := [
    "lem:gronwall remains an obligation with endpoint-safe differentiability/FTC, interval-integrability, coefficient regularity, endpoint rewrites, exponent splitting, and theorem-display matching.",
    "lem:dv_variation remains source-cited with common-space, absolute-continuity, finite-KL, selected-test measurability, finite-log-mgf, and positive-alpha scaling witnesses.",
    "eq:LSI-KL-FI remains an obligation for density, zero-set convention, admissible sqrt-density test or approximation, entropy identity, finite KL/FI, and Fisher chain rule.",
    "The continuous Fokker--Planck/KL derivative identity remains the selected local SDE/measure-analysis backend, with mass conservation, boundary/no-flux, target transport, and schedule calculus still open.",
    "The Euler--Maruyama interpolation Fokker--Planck endpoint/conditional-law backend remains a downstream discrete obligation and is not imported into the continuous theorem."
  ]
  obligations := [
    "sald.forward_kl.cycle65_continuous_route",
    "sald.forward_kl.cycle65_middle_route_audit",
    "sald.forward_kl.cycle65_derivative_pointwise_lower",
    "sald.forward_kl.kl_derivative",
    "sald.forward_kl.density_boundary_regular",
    "sald.forward_kl.schedule_time_change",
    "probability.lsi_to_kl_fi",
    "sald.forward_kl.dv_finite_log_mgf_witness",
    "sald.forward_kl.dv_energy_bound",
    "sald.forward_kl.endpoint_schedule_identities",
    "sald.forward_kl.gronwall_side_conditions",
    "sald.forward_kl.gronwall_application",
    "sald.discrete_forward_kl.em_interpolation_fp"
  ]
  lowerPacket := [
    "Target exactly SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative.",
    "First lower sub-slice: appendix.tex:168-185 mass conservation, differentiating KL under the integral, SALD Fokker--Planck substitution, boundary/no-flux integration by parts, and -FI identification.",
    "Second lower sub-slice: appendix.tex:187-208 slowed target velocity, target integration by parts, Cauchy--Schwarz/Young with the exact 1/2 share, and the L2 velocity term.",
    "Third lower sub-slice: appendix.tex:218-228 inverse-schedule chain rule, slowed-velocity square scaling, and dot{s}(t)*dot t(s(t))^2=dot{s}(t)^(-1), with the compiled pointwise wrapper producing the t-indexed pre-DV inequality.",
    "Leave LSI/KL/FI, DV finite-log-mgf, Gronwall endpoint/exponent conditions, and EM interpolation as separate named interfaces unless their exact analytic backends compile locally."
  ]
  reviewerChecklist := [
    "SALD.continuousSaldContract lists SALD.cycle65ForwardKlSkeletonMiddleObligation while remaining contractOnly.",
    "SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle65_middle_route_audit after ASTIS.SALD.forward_KL.cycle65_continuous_route and before the selected lower-packet node.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes SALD.cycle65ForwardKlSkeletonMiddleContract, SALD.cycle65ForwardKlSkeletonMiddleObligation, and sald.forward_kl.cycle65_middle_route_audit.",
    "No theorem statement, source coefficient, source label, source-file selection, SLT reuse entry, 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-65 middle obligation tying the post-cycle-64 forward-KL route audit
to the selected continuous derivative/Fokker--Planck lower packet. -/