AutoSamplingTheory.SALD.frozenDeltaCrossLipSaldContract

Data definition / provenance and workflow record

Meaning and type

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

def frozenDeltaCrossLipSaldContract : FrozenDeltaCrossLipSaldContract

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.

sourceBlock : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldFrozenDeltaCrossLipSaldSource — audited data reference, not expanded and not a compiled dependency edge

specializationRoute : String (explicit)

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

The source omits the SALD-specific proof and says it follows from lem:frozen_delta_cross_lip by setting c identically zero and sigma_eta(t)=sqrt(2).

frozenError : String (explicit)

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

delta_{pi_t}(x) = nabla log pi_t(x) - E[nabla log pi_{t_k}(X_k^eta) | hat X_s=x].

assumptions : List String (explicit)

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

Ordered data items

1. score space Lipschitz with L_{pi,space}
2. score time Lipschitz with L_{pi,time} and measurable growth function M
3. finite alpha0' exponential complexities for nabla log pi_t and 1+M
4. eta^2*L_{pi,space}^2 < 1/8

bound : String (explicit)

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

-int hat rho_s <delta_{pi_{t(s)}},A_s> <= (1/4)*FI(hat rho_s||tilde pi_s) + 2*eta^2*alpha'^(-1)*Gamma(t(s))*KL(hat rho_s||tilde pi_s) + 2*eta*Delta(t(s)).

gammaDefinition : String (explicit)

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

Gamma(t)=2*L_{pi,time}^2+64*L_{pi,space}^2*(dot{s}(t)^(-2)+1+eta^2*L_{pi,time}^2).

deltaDefinition : String (explicit)

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

Delta(t)=64*eta*L_{pi,space}^2*E_{alpha'}(pi_t,nabla log pi_t)+2*eta*L_{pi,time}^2*(1+32*eta^2*L_{pi,space}^2)*E_{alpha'}(pi_t,1+M)+16*d*L_{pi,space}^2.

dependencies : List String (explicit)

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

Ordered data items

1. lem:frozen_delta_cross_lip
2. lem:dv_variation
3. eq:lip_SALD_1
4. eq:lip_SALD_2
5. eq:frozen_interp_terminal_disc_prop_additive_final

sourceGaps : List String (explicit)

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

Ordered data items

1. the SALD-specific frozen-defect proof is omitted in the source and must be obtained by a faithful specialization of the later general lemma
2. the Lean route must reconcile the main-body step-size condition 4*eta^2*L_space^2 < 1/2 with the appendix lemma condition eta^2*L_space^2 < 1/8

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 frozenDeltaCrossLipSaldContract : FrozenDeltaCrossLipSaldContract where
  sourceBlock := saldFrozenDeltaCrossLipSaldSource
  specializationRoute := "The source omits the SALD-specific proof and says it follows from lem:frozen_delta_cross_lip by setting c identically zero and sigma_eta(t)=sqrt(2)."
  frozenError := "delta_{pi_t}(x) = nabla log pi_t(x) - E[nabla log pi_{t_k}(X_k^eta) | hat X_s=x]."
  assumptions := [
    "score space Lipschitz with L_{pi,space}",
    "score time Lipschitz with L_{pi,time} and measurable growth function M",
    "finite alpha0' exponential complexities for nabla log pi_t and 1+M",
    "eta^2*L_{pi,space}^2 < 1/8"
  ]
  bound := "-int hat rho_s <delta_{pi_{t(s)}},A_s> <= (1/4)*FI(hat rho_s||tilde pi_s) + 2*eta^2*alpha'^(-1)*Gamma(t(s))*KL(hat rho_s||tilde pi_s) + 2*eta*Delta(t(s))."
  gammaDefinition := "Gamma(t)=2*L_{pi,time}^2+64*L_{pi,space}^2*(dot{s}(t)^(-2)+1+eta^2*L_{pi,time}^2)."
  deltaDefinition := "Delta(t)=64*eta*L_{pi,space}^2*E_{alpha'}(pi_t,nabla log pi_t)+2*eta*L_{pi,time}^2*(1+32*eta^2*L_{pi,space}^2)*E_{alpha'}(pi_t,1+M)+16*d*L_{pi,space}^2."
  dependencies := [
    "lem:frozen_delta_cross_lip",
    "lem:dv_variation",
    "eq:lip_SALD_1",
    "eq:lip_SALD_2",
    "eq:frozen_interp_terminal_disc_prop_additive_final"
  ]
  sourceGaps := [
    "the SALD-specific frozen-defect proof is omitted in the source and must be obtained by a faithful specialization of the later general lemma",
    "the Lean route must reconcile the main-body step-size condition 4*eta^2*L_space^2 < 1/2 with the appendix lemma condition eta^2*L_space^2 < 1/8"
  ]
  status := ProofStatus.obligation