AutoSamplingTheory.SALD.generalFrozenDeltaCrossLipContract

Data definition / provenance and workflow record

Meaning and type

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

def generalFrozenDeltaCrossLipContract : GeneralFrozenDeltaCrossLipContract

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

frozenError : String (explicit)

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

delta_pi^VA(x)=dot{t}(s)*c_t(x)+(sigma_eta^2/2)*nabla log pi_t(x)-E[dot{t}_k*c_{t_k}(X_k^eta)+(sigma_eta^2/2)*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. space Lipschitzness of c_t with L_{c,space} and score with L_{pi,space}
2. time Lipschitzness along s for c_t and score with growth function M
3. finite alpha0' exponential complexities for c_t, nabla log pi_t, and 1+M
4. linear slowdown or constant dot{t}(s)=dot{s}(t)^(-1) on [0,S]

stepSizeCondition : String (explicit)

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

4*eta^2*(dot{t}(s)*L_{c,space}+(sigma_eta(t(s))^2/2)*L_{pi,space})^2 < 1/2.

bound : String (explicit)

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

-int hat rho_s <delta_pi^VA,A_s> <= (sigma_eta(t(s))^2/8)*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)=sigma_eta(t)^(-2)*{4*dot{s}(t)^(-2)*L_c_time^2+sigma_eta(t)^4*L_pi_time^2+8*(4*dot{s}(t)^(-2)*L_c_space^2+sigma_eta(t)^4*L_pi_space^2)*(4*dot{s}(t)^(-2)+sigma_eta(t)^4+eta^2*(4*dot{s}(t)^(-2)*L_c_time^2+sigma_eta(t)^4*L_pi_time^2))}.

deltaDefinition : String (explicit)

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

Delta(t)=eta*sigma_eta(t)^(-2)*{8*(4*dot{s}(t)^(-2)*L_c_space^2+sigma_eta(t)^4*L_pi_space^2)*(4*dot{s}(t)^(-2)*E_alpha'(pi_t,c_t)+sigma_eta(t)^4*E_alpha'(pi_t,nabla log pi_t))+(4*dot{s}(t)^(-2)*L_c_time^2+sigma_eta(t)^4*L_pi_time^2)*(1+8*eta^2*(4*dot{s}(t)^(-2)*L_c_space^2+sigma_eta(t)^4*L_pi_space^2))*E_alpha'(pi_t,1+M)}+4*d*(4*dot{s}(t)^(-2)*L_c_space^2+sigma_eta(t)^4*L_pi_space^2).

proofRoute : List String (explicit)

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

Ordered data items

1. appendix.tex:1112-1123 rewrites the cross term using the joint law of X_k^eta and hat X_s, then applies Young with coefficient sigma_eta^2/8.
2. appendix.tex:1125-1158 splits the frozen-field difference into time and space increments using the Lipschitz hypotheses.
3. appendix.tex:1161-1210 bounds the EM interpolation increment and resolves the self-referential term using the step-size condition.
4. appendix.tex:1213-1275 controls phi_{t_k} in L2(hat rho_s) and applies DV to c_t, the score, and 1+M.
5. appendix.tex:1277-1306 collects the resulting Gamma and Delta terms.

dependencies : List String (explicit)

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

Ordered data items

1. eq:SALD_general_EM
2. eq:general_moving_target_SALD_frozen_interp
3. eq:general_discrete_delta_def
4. lem:dv_variation
5. def:alpha-complexity

sourceGaps : List String (explicit)

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

Ordered data items

1. the proof uses conditional distributions of (X_k^eta,hat X_s) and L2 estimates under hat rho_s without a local probability backend
2. the statement assumes dot{t}(s) is constant but Gamma and Delta are written in dot{s}(t) notation; the Lean route must expose the constant inverse-schedule interface
3. finite log-mgf monotonicity for alpha' <= alpha0' is needed for the three DV uses

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 generalFrozenDeltaCrossLipContract : GeneralFrozenDeltaCrossLipContract where
  sourceBlock := saldFrozenDeltaCrossLipGeneralSource
  frozenError := "delta_pi^VA(x)=dot{t}(s)*c_t(x)+(sigma_eta^2/2)*nabla log pi_t(x)-E[dot{t}_k*c_{t_k}(X_k^eta)+(sigma_eta^2/2)*nabla log pi_{t_k}(X_k^eta) | hat X_s=x]."
  assumptions := [
    "space Lipschitzness of c_t with L_{c,space} and score with L_{pi,space}",
    "time Lipschitzness along s for c_t and score with growth function M",
    "finite alpha0' exponential complexities for c_t, nabla log pi_t, and 1+M",
    "linear slowdown or constant dot{t}(s)=dot{s}(t)^(-1) on [0,S]"
  ]
  stepSizeCondition := "4*eta^2*(dot{t}(s)*L_{c,space}+(sigma_eta(t(s))^2/2)*L_{pi,space})^2 < 1/2."
  bound := "-int hat rho_s <delta_pi^VA,A_s> <= (sigma_eta(t(s))^2/8)*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)=sigma_eta(t)^(-2)*{4*dot{s}(t)^(-2)*L_c_time^2+sigma_eta(t)^4*L_pi_time^2+8*(4*dot{s}(t)^(-2)*L_c_space^2+sigma_eta(t)^4*L_pi_space^2)*(4*dot{s}(t)^(-2)+sigma_eta(t)^4+eta^2*(4*dot{s}(t)^(-2)*L_c_time^2+sigma_eta(t)^4*L_pi_time^2))}."
  deltaDefinition := "Delta(t)=eta*sigma_eta(t)^(-2)*{8*(4*dot{s}(t)^(-2)*L_c_space^2+sigma_eta(t)^4*L_pi_space^2)*(4*dot{s}(t)^(-2)*E_alpha'(pi_t,c_t)+sigma_eta(t)^4*E_alpha'(pi_t,nabla log pi_t))+(4*dot{s}(t)^(-2)*L_c_time^2+sigma_eta(t)^4*L_pi_time^2)*(1+8*eta^2*(4*dot{s}(t)^(-2)*L_c_space^2+sigma_eta(t)^4*L_pi_space^2))*E_alpha'(pi_t,1+M)}+4*d*(4*dot{s}(t)^(-2)*L_c_space^2+sigma_eta(t)^4*L_pi_space^2)."
  proofRoute := [
    "appendix.tex:1112-1123 rewrites the cross term using the joint law of X_k^eta and hat X_s, then applies Young with coefficient sigma_eta^2/8.",
    "appendix.tex:1125-1158 splits the frozen-field difference into time and space increments using the Lipschitz hypotheses.",
    "appendix.tex:1161-1210 bounds the EM interpolation increment and resolves the self-referential term using the step-size condition.",
    "appendix.tex:1213-1275 controls phi_{t_k} in L2(hat rho_s) and applies DV to c_t, the score, and 1+M.",
    "appendix.tex:1277-1306 collects the resulting Gamma and Delta terms."
  ]
  dependencies := [
    "eq:SALD_general_EM",
    "eq:general_moving_target_SALD_frozen_interp",
    "eq:general_discrete_delta_def",
    "lem:dv_variation",
    "def:alpha-complexity"
  ]
  sourceGaps := [
    "the proof uses conditional distributions of (X_k^eta,hat X_s) and L2 estimates under hat rho_s without a local probability backend",
    "the statement assumes dot{t}(s) is constant but Gamma and Delta are written in dot{s}(t) notation; the Lean route must expose the constant inverse-schedule interface",
    "finite log-mgf monotonicity for alpha' <= alpha0' is needed for the three DV uses"
  ]
  status := ProofStatus.obligation