AutoSamplingTheory.SALD.cycle50ForwardKlSkeletonMiddleContract

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 cycle50ForwardKlSkeletonMiddleContract :
    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 50 middle: synchronize the post-readiness thm:forward-KL route after SALD.cycle50ForwardKlSkeletonObligation, verify the exact main_body.tex:238-247 statement and appendix.tex:168-252 derivative -> LSI -> DV -> Gronwall proof order, and select sald.forward_kl.kl_derivative as the next lower 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], SALD law rho_s, and the two-exponential initial term plus 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, and identifies the first term as -FI by integration by parts.
3. appendix.tex:187-208 builds the slowed target transport velocity tilde v_s=dot t(s)*v_{t(s)}, evaluates the second term, and applies Cauchy--Schwarz/Young with the exact 1/2 share.
4. appendix.tex:210-228 applies eq:LSI-KL-FI and inverse-schedule calculus to obtain the t-time pre-DV inequality with coefficient (1/2)*dot{s}(t)^(-1).
5. appendix.tex:230-241 invokes lem:dv_variation with Z=alpha*||v_t||^2 and rewrites the log-mgf as E_alpha(pi_t,v_t), preserving alpha^(-1).
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 source exponent split/drop.

leanStepMap : List String (explicit)

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

Ordered data items

1. Use SALD.cycle49MainSkeletonAnalyticReadinessObligation, SALD.cycle49MainSkeletonAnalyticMiddleObligation, SALD.cycle45ForwardKlSkeletonMiddleObligation, and SALD.cycle50ForwardKlSkeletonObligation as parent route checks.
2. Keep SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract contractOnly; this middle contract adds no theorem hypotheses.
3. Route appendix.tex:168-228 through SALD.forwardKlDerivativeCandidateContract, SALD.forwardKlDerivativeSideConditionContract, 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, admissibility, entropy, and Fisher-chain assumptions remain obligations.
5. Route appendix.tex:230-241 through SALD.forwardKlDvFiniteLogMgfWitnessContract and sald.forward_kl.dv_finite_log_mgf_witness before using sald.forward_kl.dv_energy_bound.
6. Route appendix.tex:244-252 through 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 downstream discrete slow interfaces.
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 real-analysis obligation with coefficient regularity, FTC/order integration, endpoint rewrites, and exponent-display side conditions.
2. lem:dv_variation remains source-cited; no SLT entropy-duality theorem is imported or marked formalized.
3. eq:LSI-KL-FI remains the density-test, entropy-identity, zero-set, admissibility, and Fisher-chain obligation.
4. The continuous Fokker-Planck/KL derivative is the selected local SDE/measure-analysis backend; this middle audit does not promote it.
5. The EM interpolation Fokker-Planck interface remains a downstream discrete obligation and is not a continuous theorem assumption.

obligations : List String (explicit)

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

Ordered data items

1. sald.forward_kl.cycle50_theorem_skeleton_route
2. sald.forward_kl.cycle50_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, integration by parts for the target term, Cauchy--Schwarz/Young, and the L2 velocity term.
4. Third lower sub-slice: appendix.tex:218-228 inverse-schedule chain rule and dot{s}(t)*dot t(s(t))^2=dot{s}(t)^(-1).
5. Do not add density, AC, endpoint, finite-KL/FI, finite-log-mgf, coefficient-regularity, or schedule assumptions to thm:forward-KL; keep blocked facts as named obligations.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.continuousSaldContract lists SALD.cycle50ForwardKlSkeletonMiddleObligation while remaining contractOnly.
2. SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle50_middle_route_audit after the cycle-50 route node.
3. SALD.saldDependenciesForLabel "thm:forward-KL" includes the cycle-50 middle contract, obligation, and named audit obligation.
4. No theorem statement, source constant, 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 cycle50ForwardKlSkeletonMiddleContract :
    ForwardKlMiddleSourceToLeanContract where
  sourceStatement := saldForwardKlSource
  sourceProof := saldForwardKlProofSource
  derivativeSource := saldForwardKlDerivativeSource
  dvSource := saldForwardKlDvEnergySource
  gronwallSource := saldForwardKlGronwallSource
  objective := "Cycle 50 middle: synchronize the post-readiness thm:forward-KL route after SALD.cycle50ForwardKlSkeletonObligation, verify the exact main_body.tex:238-247 statement and appendix.tex:168-252 derivative -> LSI -> DV -> Gronwall proof order, and select sald.forward_kl.kl_derivative as the next lower 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], SALD law rho_s, and the two-exponential initial term plus 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, and identifies the first term as -FI by integration by parts.",
    "appendix.tex:187-208 builds the slowed target transport velocity tilde v_s=dot t(s)*v_{t(s)}, evaluates the second term, and applies Cauchy--Schwarz/Young with the exact 1/2 share.",
    "appendix.tex:210-228 applies eq:LSI-KL-FI and inverse-schedule calculus to obtain the t-time pre-DV inequality with coefficient (1/2)*dot{s}(t)^(-1).",
    "appendix.tex:230-241 invokes lem:dv_variation with Z=alpha*||v_t||^2 and rewrites the log-mgf as E_alpha(pi_t,v_t), preserving alpha^(-1).",
    "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 source exponent split/drop."
  ]
  leanStepMap := [
    "Use SALD.cycle49MainSkeletonAnalyticReadinessObligation, SALD.cycle49MainSkeletonAnalyticMiddleObligation, SALD.cycle45ForwardKlSkeletonMiddleObligation, and SALD.cycle50ForwardKlSkeletonObligation as parent route checks.",
    "Keep SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract contractOnly; this middle contract adds no theorem hypotheses.",
    "Route appendix.tex:168-228 through SALD.forwardKlDerivativeCandidateContract, SALD.forwardKlDerivativeSideConditionContract, 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, admissibility, entropy, and Fisher-chain assumptions remain obligations.",
    "Route appendix.tex:230-241 through SALD.forwardKlDvFiniteLogMgfWitnessContract and sald.forward_kl.dv_finite_log_mgf_witness before using sald.forward_kl.dv_energy_bound.",
    "Route appendix.tex:244-252 through 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 downstream discrete slow interfaces.",
    "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 real-analysis obligation with coefficient regularity, FTC/order integration, endpoint rewrites, and exponent-display side conditions.",
    "lem:dv_variation remains source-cited; no SLT entropy-duality theorem is imported or marked formalized.",
    "eq:LSI-KL-FI remains the density-test, entropy-identity, zero-set, admissibility, and Fisher-chain obligation.",
    "The continuous Fokker-Planck/KL derivative is the selected local SDE/measure-analysis backend; this middle audit does not promote it.",
    "The EM interpolation Fokker-Planck interface remains a downstream discrete obligation and is not a continuous theorem assumption."
  ]
  obligations := [
    "sald.forward_kl.cycle50_theorem_skeleton_route",
    "sald.forward_kl.cycle50_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, integration by parts for the target term, Cauchy--Schwarz/Young, and the L2 velocity term.",
    "Third lower sub-slice: appendix.tex:218-228 inverse-schedule chain rule and dot{s}(t)*dot t(s(t))^2=dot{s}(t)^(-1).",
    "Do not add density, AC, endpoint, finite-KL/FI, finite-log-mgf, coefficient-regularity, or schedule assumptions to thm:forward-KL; keep blocked facts as named obligations."
  ]
  reviewerChecklist := [
    "SALD.continuousSaldContract lists SALD.cycle50ForwardKlSkeletonMiddleObligation while remaining contractOnly.",
    "SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle50_middle_route_audit after the cycle-50 route node.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes the cycle-50 middle contract, obligation, and named audit obligation.",
    "No theorem statement, source constant, 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-50 middle obligation selecting the continuous KL derivative backend. -/