AutoSamplingTheory.SALD.cycle55ForwardKlSkeletonMiddleContract

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 cycle55ForwardKlSkeletonMiddleContract :
    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 55 middle: synchronize the cycle-55 upper forward-KL route with the source-to-Lean ledger, verify main_body.tex:238-247 and appendix.tex:164-252 in paper order after the cycle-54 five-backend re-check, and keep sald.forward_kl.kl_derivative over appendix.tex:168-228 as the lower-ready backend without changing constants or theorem status.

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 statement: C_LSI(t)>=0, finite E_alpha0(pi_t,v_t), alpha in (0,alpha0], rho_s is the SALD law, and the final bound has the two source exponent factors plus the residual alpha-complexity integral.
2. appendix.tex:168-185 differentiates KL(rho_s||tilde pi_s), uses mass conservation, substitutes the SALD Fokker--Planck equation, integrates by parts, and identifies the first term as -FI.
3. appendix.tex:187-208 builds the slowed target velocity tilde v_s=dot t(s)*v_{t(s)}, evaluates the target-time term by integration by parts, and applies Cauchy--Schwarz/Young with the exact 1/2 and 1/2 split.
4. appendix.tex:210-228 applies eq:LSI-KL-FI and the inverse-schedule chain rule, preserving the t-time velocity coefficient (1/2)*dot{s}(t)^(-1).
5. appendix.tex:230-241 applies lem:dv_variation with Z=alpha*||v_t||^2, uses the alpha0-to-alpha finite-log-mgf witness, and rewrites the log-mgf quotient as mathfrak E_alpha(pi_t,v_t).
6. appendix.tex:244-252 applies lem:gronwall with a(t)=dot{s}(t)*C_LSI(t)-(1/2)*dot{s}(t)^(-1)*alpha^(-1) and b(t)=(1/2)*dot{s}(t)^(-1)*E_alpha(pi_t,v_t), then performs only the paper exponent split and residual-exponent drop.

leanStepMap : List String (explicit)

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

Ordered data items

1. Use SALD.cycle54MainSkeletonAnalyticInterfaceObligation, SALD.cycle54MainSkeletonAnalyticMiddleObligation, SALD.cycle50ForwardKlSkeletonMiddleObligation, and SALD.cycle55ForwardKlSkeletonObligation as parent route checks.
2. Keep SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract contractOnly; this middle audit adds no theorem hypotheses.
3. Route appendix.tex:168-228 through SALD.forwardKlDerivativeCandidateContract, SALD.forwardKlDerivativeSideConditionContract, SALD.forwardKlDerivativeObligation, sald.forward_kl.density_boundary_regular, sald.forward_kl.schedule_time_change, and sald.forward_kl.kl_derivative.
4. Route appendix.tex:210-217 through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi; density, zero-set, admissible sqrt-density test, entropy identity, finite KL/FI, and Fisher-chain assumptions remain obligations.
5. 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.
6. Route appendix.tex:244-252 through SALD.saldGronwallEndpointCalculusContract, SALD.forwardKlGronwallInstantiationContract, SALD.forwardKlGronwallSideConditionContract, sald.forward_kl.gronwall_side_conditions, and sald.forward_kl.gronwall_application.
7. Keep SALD.discreteForwardKlEmInterpolationSideConditionContract and sald.discrete_forward_kl.em_interpolation_fp visible only as the downstream EM/Fokker--Planck slow backend for discrete reuse.
8. Select the next lower target as SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative over appendix.tex:168-228.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. lem:gronwall remains the endpoint-safe differentiability/FTC and coefficient-regularity obligation; cycle 55 middle only records the theorem-specific instantiation.
2. lem:dv_variation remains source-cited; the forward-KL use must still supply common-space, absolute-continuity, finite KL/log-likelihood, measurability, finite log-mgf, and positive-alpha witnesses.
3. eq:LSI-KL-FI remains the density-test, zero-set, admissibility, entropy-identity, finite KL/FI, and Fisher-chain obligation.
4. The continuous Fokker--Planck/KL derivative is the selected local SDE/measure-analysis backend and is not promoted by this middle audit.
5. The Euler--Maruyama interpolation Fokker--Planck interface remains a downstream discrete obligation, not a hidden continuous forward-KL assumption.

obligations : List String (explicit)

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

Ordered data items

1. sald.forward_kl.cycle55_continuous_skeleton_route
2. sald.forward_kl.cycle55_middle_route_audit
3. sald.forward_kl.kl_derivative
4. sald.forward_kl.density_boundary_regular
5. sald.forward_kl.schedule_time_change
6. probability.lsi_to_kl_fi
7. sald.forward_kl.dv_finite_log_mgf_witness
8. sald.forward_kl.dv_energy_bound
9. sald.forward_kl.gronwall_side_conditions
10. sald.forward_kl.gronwall_application
11. 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, KL differentiation 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 target transport 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).
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.cycle55ForwardKlSkeletonMiddleObligation while remaining contractOnly.
2. SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle55_middle_route_audit after ASTIS.SALD.forward_KL.cycle55_continuous_skeleton_route.
3. SALD.saldDependenciesForLabel "thm:forward-KL" includes SALD.cycle55ForwardKlSkeletonMiddleContract, SALD.cycle55ForwardKlSkeletonMiddleObligation, and sald.forward_kl.cycle55_middle_route_audit.
4. No theorem statement, source coefficient, source label, source-file selection, 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 cycle55ForwardKlSkeletonMiddleContract :
    ForwardKlMiddleSourceToLeanContract where
  sourceStatement := saldForwardKlSource
  sourceProof := saldForwardKlProofSource
  derivativeSource := saldForwardKlDerivativeSource
  dvSource := saldForwardKlDvEnergySource
  gronwallSource := saldForwardKlGronwallSource
  objective := "Cycle 55 middle: synchronize the cycle-55 upper forward-KL route with the source-to-Lean ledger, verify main_body.tex:238-247 and appendix.tex:164-252 in paper order after the cycle-54 five-backend re-check, and keep sald.forward_kl.kl_derivative over appendix.tex:168-228 as the lower-ready backend without changing constants or theorem status."
  sourceStepMap := [
    "main_body.tex:238-247 fixes the theorem statement: C_LSI(t)>=0, finite E_alpha0(pi_t,v_t), alpha in (0,alpha0], rho_s is the SALD law, and the final bound has the two source exponent factors plus the residual alpha-complexity integral.",
    "appendix.tex:168-185 differentiates KL(rho_s||tilde pi_s), uses mass conservation, substitutes the SALD Fokker--Planck equation, integrates by parts, and identifies the first term as -FI.",
    "appendix.tex:187-208 builds the slowed target velocity tilde v_s=dot t(s)*v_{t(s)}, evaluates the target-time term by integration by parts, and applies Cauchy--Schwarz/Young with the exact 1/2 and 1/2 split.",
    "appendix.tex:210-228 applies eq:LSI-KL-FI and the inverse-schedule chain rule, preserving the t-time velocity coefficient (1/2)*dot{s}(t)^(-1).",
    "appendix.tex:230-241 applies lem:dv_variation with Z=alpha*||v_t||^2, uses the alpha0-to-alpha finite-log-mgf witness, and rewrites the log-mgf quotient as mathfrak E_alpha(pi_t,v_t).",
    "appendix.tex:244-252 applies lem:gronwall with a(t)=dot{s}(t)*C_LSI(t)-(1/2)*dot{s}(t)^(-1)*alpha^(-1) and b(t)=(1/2)*dot{s}(t)^(-1)*E_alpha(pi_t,v_t), then performs only the paper exponent split and residual-exponent drop."
  ]
  leanStepMap := [
    "Use SALD.cycle54MainSkeletonAnalyticInterfaceObligation, SALD.cycle54MainSkeletonAnalyticMiddleObligation, SALD.cycle50ForwardKlSkeletonMiddleObligation, and SALD.cycle55ForwardKlSkeletonObligation as parent route checks.",
    "Keep SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract contractOnly; this middle audit adds no theorem hypotheses.",
    "Route appendix.tex:168-228 through SALD.forwardKlDerivativeCandidateContract, SALD.forwardKlDerivativeSideConditionContract, SALD.forwardKlDerivativeObligation, sald.forward_kl.density_boundary_regular, sald.forward_kl.schedule_time_change, and sald.forward_kl.kl_derivative.",
    "Route appendix.tex:210-217 through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi; density, zero-set, admissible sqrt-density test, entropy identity, finite KL/FI, and Fisher-chain assumptions remain 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.gronwall_side_conditions, and sald.forward_kl.gronwall_application.",
    "Keep SALD.discreteForwardKlEmInterpolationSideConditionContract and sald.discrete_forward_kl.em_interpolation_fp visible only as the downstream EM/Fokker--Planck slow backend for discrete reuse.",
    "Select the next lower target as SALD.forwardKlDerivativeCandidateContract / SALD.forwardKlDerivativeObligation / sald.forward_kl.kl_derivative over appendix.tex:168-228."
  ]
  citedResultInterfaces := [
    "lem:gronwall remains the endpoint-safe differentiability/FTC and coefficient-regularity obligation; cycle 55 middle only records the theorem-specific instantiation.",
    "lem:dv_variation remains source-cited; the forward-KL use must still supply common-space, absolute-continuity, finite KL/log-likelihood, measurability, finite log-mgf, and positive-alpha witnesses.",
    "eq:LSI-KL-FI remains the density-test, zero-set, admissibility, entropy-identity, finite KL/FI, and Fisher-chain obligation.",
    "The continuous Fokker--Planck/KL derivative is the selected local SDE/measure-analysis backend and is not promoted by this middle audit.",
    "The Euler--Maruyama interpolation Fokker--Planck interface remains a downstream discrete obligation, not a hidden continuous forward-KL assumption."
  ]
  obligations := [
    "sald.forward_kl.cycle55_continuous_skeleton_route",
    "sald.forward_kl.cycle55_middle_route_audit",
    "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.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, KL differentiation under the integral, SALD Fokker--Planck substitution, boundary/no-flux integration by parts, and -FI identification.",
    "Second lower sub-slice: appendix.tex:187-208 target transport 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).",
    "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.cycle55ForwardKlSkeletonMiddleObligation while remaining contractOnly.",
    "SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle55_middle_route_audit after ASTIS.SALD.forward_KL.cycle55_continuous_skeleton_route.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes SALD.cycle55ForwardKlSkeletonMiddleContract, SALD.cycle55ForwardKlSkeletonMiddleObligation, and sald.forward_kl.cycle55_middle_route_audit.",
    "No theorem statement, source coefficient, source label, source-file selection, 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-55 middle obligation tying the continuous forward-KL route audit to
the lower derivative/Fokker--Planck packet. -/