AutoSamplingTheory.SALD.forwardKlEndpointScheduleContract

Data definition / provenance and workflow record

Meaning and type

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

def forwardKlEndpointScheduleContract :
    ForwardKlEndpointScheduleContract

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

slowdownInterface : String (explicit)

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

main_body.tex:9-13 introduces t=t(s) on s in [0,S] as a smooth monotone increasing slowdown and main_body.tex:238 names the inverse s=s(t).

inverseEndpointIdentities : String (explicit)

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

For the theorem endpoint display, the Lean route must isolate s(0)=0, S=s(T), t(s(T))=T, and t(s(0))=0 as inverse-schedule endpoint identities rather than adding them to thm:forward-KL.

slowedTargetIdentity : String (explicit)

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

appendix.tex:218-228 rewrites KL(rho_{s(t)}||tilde_pi_{s(t)}) as KL(rho_{s(t)}||pi_t), using tilde_pi_s=pi_{t(s)} and the inverse identity t(s(t))=t.

klPathDefinition : String (explicit)

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

The scalar Gronwall quantity is K(t)=KL(rho_{s(t)}||pi_t) after the slowed-target rewrite, with K defined on the original t-interval [0,T].

terminalRewrite : String (explicit)

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

The terminal Gronwall endpoint K(T) becomes KL(rho_{s(T)}||pi_T), then KL(rho_S||pi_T) using S=s(T), exactly matching main_body.tex:243.

initialRewrite : String (explicit)

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

The initial Gronwall endpoint K(0) becomes KL(rho_{s(0)}||pi_0), then KL(rho_0||pi_0) using s(0)=0, exactly matching main_body.tex:245.

gronwallUse : String (explicit)

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

appendix.tex:244-252 uses these endpoint rewrites only after the differential inequality and DV step; they do not change the source a(t), b(t), or terminal theorem display.

dependencies : List String (explicit)

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

Ordered data items

1. SALD.forwardKlMovingTargetDependencyContract
2. SALD.forwardKlGronwallSideConditionContract
3. sald.forward_kl.moving_target_dependency_chain
4. sald.forward_kl.schedule_time_change
5. sald.forward_kl.gronwall_side_conditions

sourceGaps : List String (explicit)

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

Ordered data items

1. the source states the slowdown and inverse schedule but does not prove a closed-interval inverse endpoint lemma
2. the paper identifies S with s(T) in the theorem endpoint display without a named assumption or lemma
3. the slowed-target equality tilde_pi_{s(t)}=pi_t depends on the inverse identity t(s(t))=t on [0,T]

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 forwardKlEndpointScheduleContract :
    ForwardKlEndpointScheduleContract where
  sourceStatement := saldForwardKlSource
  sourceProof := saldForwardKlEndpointScheduleSource
  slowdownInterface := "main_body.tex:9-13 introduces t=t(s) on s in [0,S] as a smooth monotone increasing slowdown and main_body.tex:238 names the inverse s=s(t)."
  inverseEndpointIdentities := "For the theorem endpoint display, the Lean route must isolate s(0)=0, S=s(T), t(s(T))=T, and t(s(0))=0 as inverse-schedule endpoint identities rather than adding them to thm:forward-KL."
  slowedTargetIdentity := "appendix.tex:218-228 rewrites KL(rho_{s(t)}||tilde_pi_{s(t)}) as KL(rho_{s(t)}||pi_t), using tilde_pi_s=pi_{t(s)} and the inverse identity t(s(t))=t."
  klPathDefinition := "The scalar Gronwall quantity is K(t)=KL(rho_{s(t)}||pi_t) after the slowed-target rewrite, with K defined on the original t-interval [0,T]."
  terminalRewrite := "The terminal Gronwall endpoint K(T) becomes KL(rho_{s(T)}||pi_T), then KL(rho_S||pi_T) using S=s(T), exactly matching main_body.tex:243."
  initialRewrite := "The initial Gronwall endpoint K(0) becomes KL(rho_{s(0)}||pi_0), then KL(rho_0||pi_0) using s(0)=0, exactly matching main_body.tex:245."
  gronwallUse := "appendix.tex:244-252 uses these endpoint rewrites only after the differential inequality and DV step; they do not change the source a(t), b(t), or terminal theorem display."
  dependencies := [
    "SALD.forwardKlMovingTargetDependencyContract",
    "SALD.forwardKlGronwallSideConditionContract",
    "sald.forward_kl.moving_target_dependency_chain",
    "sald.forward_kl.schedule_time_change",
    "sald.forward_kl.gronwall_side_conditions"
  ]
  sourceGaps := [
    "the source states the slowdown and inverse schedule but does not prove a closed-interval inverse endpoint lemma",
    "the paper identifies S with s(T) in the theorem endpoint display without a named assumption or lemma",
    "the slowed-target equality tilde_pi_{s(t)}=pi_t depends on the inverse identity t(s(t))=t on [0,T]"
  ]
  status := ProofStatus.obligation