AutoSamplingTheory.SALD.forwardKlMovingTargetDependencyContract

Data definition / provenance and workflow record

Meaning and type

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

def forwardKlMovingTargetDependencyContract :
    ForwardKlMovingTargetDependencyContract

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

slowedTargetPath : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

main_body.tex:238 and appendix.tex:187-197 use tilde_pi_s=pi_{t(s)} with inverse slowdown s=s(t).

transportVelocityInterface : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

The theorem assumes v is the transport velocity of pi; appendix.tex:187-197 requires partial_t pi_t+div(v_t*pi_t)=0 and tilde_v_s=dot{t}(s)*v_{t(s)}.

saldLawInterface : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

rho_s is the law of SALD eq:SALD, and appendix.tex:176-185 uses the corresponding Fokker--Planck equation before any LSI, DV, or Gronwall step.

lsiBridge : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

main_body.tex:240-241 assumes C_LSI(t)>=0; appendix.tex:210-217 uses eq:LSI-KL-FI to convert the remaining -(1/2)*FI term into -C_LSI(t(s))*KL.

dvBridge : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

appendix.tex:230-241 applies lem:dv_variation with Z=alpha*||v_t||^2 and the finite alpha0-complexity assumption from main_body.tex:241.

gronwallBridge : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

appendix.tex:244-252 applies lem:gronwall after DV 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).

terminalIdentification : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

K(T)=KL(rho_S||pi_T) and K(0)=KL(rho_0||pi_0) rely on S=s(T), s(0)=0, and the slowed target identity.

lowerFormalizationTarget : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

Refine the named moving-target dependency-chain obligation before attempting the KL derivative, DV-energy, or Gronwall theorem proof.

dependencies : List String (explicit)

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

Ordered data items

1. eq:SALD
2. eq:FP-eq
3. TransportVelocityContract
4. eq:LSI-KL-FI
5. def:alpha-complexity
6. lem:dv_variation
7. lem:gronwall
8. sald.forward_kl.endpoint_schedule_identities
9. sald.forward_kl.density_boundary_regular
10. sald.forward_kl.schedule_time_change
11. sald.forward_kl.kl_derivative
12. sald.forward_kl.dv_energy_bound
13. sald.forward_kl.gronwall_application

sourceGaps : List String (explicit)

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

Ordered data items

1. the source states smooth monotone slowdown but not endpoint identities s(0)=0 and S=s(T) as a separate lemma
2. the transport-velocity and Fokker--Planck interfaces are used in the appendix proof without a local analytic backend
3. the theorem statement does not isolate continuity or integrability assumptions for C_LSI, dot{s}, and E_alpha needed by Gronwall

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 forwardKlMovingTargetDependencyContract :
    ForwardKlMovingTargetDependencyContract where
  sourceStatement := saldForwardKlSource
  sourceProof := saldForwardKlProofSource
  slowedTargetPath := "main_body.tex:238 and appendix.tex:187-197 use tilde_pi_s=pi_{t(s)} with inverse slowdown s=s(t)."
  transportVelocityInterface := "The theorem assumes v is the transport velocity of pi; appendix.tex:187-197 requires partial_t pi_t+div(v_t*pi_t)=0 and tilde_v_s=dot{t}(s)*v_{t(s)}."
  saldLawInterface := "rho_s is the law of SALD eq:SALD, and appendix.tex:176-185 uses the corresponding Fokker--Planck equation before any LSI, DV, or Gronwall step."
  lsiBridge := "main_body.tex:240-241 assumes C_LSI(t)>=0; appendix.tex:210-217 uses eq:LSI-KL-FI to convert the remaining -(1/2)*FI term into -C_LSI(t(s))*KL."
  dvBridge := "appendix.tex:230-241 applies lem:dv_variation with Z=alpha*||v_t||^2 and the finite alpha0-complexity assumption from main_body.tex:241."
  gronwallBridge := "appendix.tex:244-252 applies lem:gronwall after DV 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)."
  terminalIdentification := "K(T)=KL(rho_S||pi_T) and K(0)=KL(rho_0||pi_0) rely on S=s(T), s(0)=0, and the slowed target identity."
  lowerFormalizationTarget := "Refine the named moving-target dependency-chain obligation before attempting the KL derivative, DV-energy, or Gronwall theorem proof."
  dependencies := [
    "eq:SALD",
    "eq:FP-eq",
    "TransportVelocityContract",
    "eq:LSI-KL-FI",
    "def:alpha-complexity",
    "lem:dv_variation",
    "lem:gronwall",
    "sald.forward_kl.endpoint_schedule_identities",
    "sald.forward_kl.density_boundary_regular",
    "sald.forward_kl.schedule_time_change",
    "sald.forward_kl.kl_derivative",
    "sald.forward_kl.dv_energy_bound",
    "sald.forward_kl.gronwall_application"
  ]
  sourceGaps := [
    "the source states smooth monotone slowdown but not endpoint identities s(0)=0 and S=s(T) as a separate lemma",
    "the transport-velocity and Fokker--Planck interfaces are used in the appendix proof without a local analytic backend",
    "the theorem statement does not isolate continuity or integrability assumptions for C_LSI, dot{s}, and E_alpha needed by Gronwall"
  ]
  status := ProofStatus.obligation