AutoSamplingTheory.SALD.cycle45ForwardKlSkeletonMiddleContract

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 cycle45ForwardKlSkeletonMiddleContract :
    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.

Middle source-to-Lean audit for main skeleton sprint 2: verify that cycle45ForwardKlSkeletonObligation consumes the continuous KL derivative, LSI/KL/FI, DV finite-log-mgf, and Gronwall endpoint interfaces in the exact appendix.tex:168-252 order, while main_body.tex:238-247 remains the unchanged theorem statement.

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 statement: pi_t has C_LSI(t)>=0, finite E_alpha0(pi_t,v_t), alpha in (0,alpha0], rho_s is the SALD law, and the terminal bound has the source two-exponential initial term plus residual integral.
2. appendix.tex:168-185 differentiates KL(rho_s||tilde pi_s), uses mass conservation, substitutes the SALD Fokker-Planck equation, and identifies the first term as -FI through integration by parts.
3. appendix.tex:187-208 transports tilde pi_s by tilde v_s=dot{t}(s)v_{t(s)}, evaluates the second term, then applies Cauchy--Schwarz and 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 to get the t-time pre-DV inequality with coefficient (1/2)*dot{s}(t)^(-1).
5. appendix.tex:230-241 applies lem:dv_variation to Z=alpha*||v_t||^2 and rewrites the log-mgf as E_alpha(pi_t,v_t), preserving the alpha^(-1) coefficient.
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), then splits the initial exponent and drops the LSI term from the residual exponent exactly as in the source display.

leanStepMap : List String (explicit)

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

Ordered data items

1. Keep SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract unchanged; the middle contract only audits the route wrapper.
2. Use SALD.cycle44MainSkeletonAnalyticInterfaceLedger and SALD.cycle45ForwardKlSkeletonObligation as the parent theorem-skeleton interfaces.
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 the LSI step through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi; the density-test, zero-set, admissibility, entropy, and Fisher-chain backends remain obligations.
5. Route appendix.tex:230-241 through SALD.forwardKlDvFiniteLogMgfWitnessContract, sald.forward_kl.dv_finite_log_mgf_witness, and sald.forward_kl.dv_energy_bound; the DV formula remains source-cited and the alpha0-to-alpha witness remains an obligation.
6. Route appendix.tex:244-252 through SALD.forwardKlGronwallInstantiationContract, SALD.forwardKlGronwallSideConditionContract, and sald.forward_kl.gronwall_application.
7. Keep SALD.discreteForwardKlEmInterpolationSideConditionContract visible only as the downstream slow backend checked by the cycle-44 ledger; it is not used to change the continuous theorem.
8. Select the next lower target as sald.forward_kl.gronwall_side_conditions, because it is the theorem-level display-matching backend after derivative, LSI, and DV interfaces are already named.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. lem:dv_variation remains source-cited through the DV interface; no SLT entropy-duality theorem is imported or marked formalized.
2. lem:gronwall remains the endpoint-safe real-analysis obligation with FTC, coefficient regularity, endpoint, and exponent-splitting side conditions.
3. eq:LSI-KL-FI remains the density-test and Fisher-chain obligation; existing compiled scalar and RN-density helpers are dependencies only.
4. The continuous Fokker-Planck/KL derivative remains a local SDE/measure-analysis obligation; no Fokker-Planck backend is promoted by this middle audit.
5. The EM interpolation Fokker-Planck backend remains a downstream discrete obligation, not a 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.cycle45_theorem_skeleton_route
2. sald.forward_kl.cycle45_middle_route_audit
3. sald.forward_kl.kl_derivative
4. probability.lsi_to_kl_fi
5. sald.forward_kl.dv_finite_log_mgf_witness
6. sald.forward_kl.dv_energy_bound
7. sald.forward_kl.gronwall_side_conditions
8. sald.forward_kl.gronwall_application
9. 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.forwardKlGronwallSideConditionContract / SALD.forwardKlGronwallSideConditionObligation / sald.forward_kl.gronwall_side_conditions.
2. First lower sub-slice: expose coefficient regularity and adjacent interval-integrability for dot{s}(t)*C_LSI(t), (1/2)*dot{s}(t)^(-1)*alpha^(-1), and (1/2)*dot{s}(t)^(-1)*E_alpha(pi_t,v_t).
3. Second lower sub-slice: connect the theorem-specific exponent split to SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces without changing signs, endpoint limits, or constants.
4. Leave endpoint K(0)/K(T) rewrites, residual-exponent monotonicity, DV finite-log-mgf, LSI density-test, continuous KL derivative, and full Gronwall as obligations unless an exact compiled proof is added.
5. Do not work on discrete EM interpolation in this lower packet; it remains only the downstream sibling slow interface for theorem-route stability.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.continuousSaldContract lists SALD.cycle45ForwardKlSkeletonMiddleObligation while remaining contractOnly.
2. SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle45_middle_route_audit after the cycle-45 theorem skeleton route and before lower derivative/DV/Gronwall nodes.
3. SALD.saldDependenciesForLabel "thm:forward-KL" includes SALD.cycle45ForwardKlSkeletonMiddleContract, SALD.cycle45ForwardKlSkeletonMiddleObligation, and sald.forward_kl.cycle45_middle_route_audit.
4. No analytic backend status is promoted, no theorem statement or source constant changes, and no alternate proof route is introduced.
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 cycle45ForwardKlSkeletonMiddleContract :
    ForwardKlMiddleSourceToLeanContract where
  sourceStatement := saldForwardKlSource
  sourceProof := saldForwardKlProofSource
  derivativeSource := saldForwardKlDerivativeSource
  dvSource := saldForwardKlDvEnergySource
  gronwallSource := saldForwardKlGronwallSource
  objective := "Middle source-to-Lean audit for main skeleton sprint 2: verify that cycle45ForwardKlSkeletonObligation consumes the continuous KL derivative, LSI/KL/FI, DV finite-log-mgf, and Gronwall endpoint interfaces in the exact appendix.tex:168-252 order, while main_body.tex:238-247 remains the unchanged theorem statement."
  sourceStepMap := [
    "main_body.tex:238-247 fixes the statement: pi_t has C_LSI(t)>=0, finite E_alpha0(pi_t,v_t), alpha in (0,alpha0], rho_s is the SALD law, and the terminal bound has the source two-exponential initial term plus residual integral.",
    "appendix.tex:168-185 differentiates KL(rho_s||tilde pi_s), uses mass conservation, substitutes the SALD Fokker-Planck equation, and identifies the first term as -FI through integration by parts.",
    "appendix.tex:187-208 transports tilde pi_s by tilde v_s=dot{t}(s)v_{t(s)}, evaluates the second term, then applies Cauchy--Schwarz and 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 to get the t-time pre-DV inequality with coefficient (1/2)*dot{s}(t)^(-1).",
    "appendix.tex:230-241 applies lem:dv_variation to Z=alpha*||v_t||^2 and rewrites the log-mgf as E_alpha(pi_t,v_t), preserving the alpha^(-1) coefficient.",
    "appendix.tex:244-252 applies lem:gronwall with a(t)=dot{s}(t)*C_LSI(t)-(1/2)*dot{s}(t)^(-1)*alpha^(-1), then splits the initial exponent and drops the LSI term from the residual exponent exactly as in the source display."
  ]
  leanStepMap := [
    "Keep SALD.continuousForwardKlStatementContract and SALD.continuousSaldContract unchanged; the middle contract only audits the route wrapper.",
    "Use SALD.cycle44MainSkeletonAnalyticInterfaceLedger and SALD.cycle45ForwardKlSkeletonObligation as the parent theorem-skeleton interfaces.",
    "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 the LSI step through SALD.saldLsiKlFiDensityTestContract and probability.lsi_to_kl_fi; the density-test, zero-set, admissibility, entropy, and Fisher-chain backends remain obligations.",
    "Route appendix.tex:230-241 through SALD.forwardKlDvFiniteLogMgfWitnessContract, sald.forward_kl.dv_finite_log_mgf_witness, and sald.forward_kl.dv_energy_bound; the DV formula remains source-cited and the alpha0-to-alpha witness remains an obligation.",
    "Route appendix.tex:244-252 through SALD.forwardKlGronwallInstantiationContract, SALD.forwardKlGronwallSideConditionContract, and sald.forward_kl.gronwall_application.",
    "Keep SALD.discreteForwardKlEmInterpolationSideConditionContract visible only as the downstream slow backend checked by the cycle-44 ledger; it is not used to change the continuous theorem.",
    "Select the next lower target as sald.forward_kl.gronwall_side_conditions, because it is the theorem-level display-matching backend after derivative, LSI, and DV interfaces are already named."
  ]
  citedResultInterfaces := [
    "lem:dv_variation remains source-cited through the DV interface; no SLT entropy-duality theorem is imported or marked formalized.",
    "lem:gronwall remains the endpoint-safe real-analysis obligation with FTC, coefficient regularity, endpoint, and exponent-splitting side conditions.",
    "eq:LSI-KL-FI remains the density-test and Fisher-chain obligation; existing compiled scalar and RN-density helpers are dependencies only.",
    "The continuous Fokker-Planck/KL derivative remains a local SDE/measure-analysis obligation; no Fokker-Planck backend is promoted by this middle audit.",
    "The EM interpolation Fokker-Planck backend remains a downstream discrete obligation, not a continuous forward-KL assumption."
  ]
  obligations := [
    "sald.forward_kl.cycle45_theorem_skeleton_route",
    "sald.forward_kl.cycle45_middle_route_audit",
    "sald.forward_kl.kl_derivative",
    "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.forwardKlGronwallSideConditionContract / SALD.forwardKlGronwallSideConditionObligation / sald.forward_kl.gronwall_side_conditions.",
    "First lower sub-slice: expose coefficient regularity and adjacent interval-integrability for dot{s}(t)*C_LSI(t), (1/2)*dot{s}(t)^(-1)*alpha^(-1), and (1/2)*dot{s}(t)^(-1)*E_alpha(pi_t,v_t).",
    "Second lower sub-slice: connect the theorem-specific exponent split to SALD.forwardKlGronwallExpProductRewriteIntegralCongrOfPieces without changing signs, endpoint limits, or constants.",
    "Leave endpoint K(0)/K(T) rewrites, residual-exponent monotonicity, DV finite-log-mgf, LSI density-test, continuous KL derivative, and full Gronwall as obligations unless an exact compiled proof is added.",
    "Do not work on discrete EM interpolation in this lower packet; it remains only the downstream sibling slow interface for theorem-route stability."
  ]
  reviewerChecklist := [
    "SALD.continuousSaldContract lists SALD.cycle45ForwardKlSkeletonMiddleObligation while remaining contractOnly.",
    "SALD.forwardKlProofDag contains ASTIS.SALD.forward_KL.cycle45_middle_route_audit after the cycle-45 theorem skeleton route and before lower derivative/DV/Gronwall nodes.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL\" includes SALD.cycle45ForwardKlSkeletonMiddleContract, SALD.cycle45ForwardKlSkeletonMiddleObligation, and sald.forward_kl.cycle45_middle_route_audit.",
    "No analytic backend status is promoted, no theorem statement or source constant changes, and no alternate proof route is introduced.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

/-- Cycle-45 middle obligation tying the forward-KL route audit to lower work. -/