AutoSamplingTheory.SALD.generalMovingTargetDiscreteDerivativeCandidateContract

Data definition / provenance and workflow record

Meaning and type

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

def generalMovingTargetDiscreteDerivativeCandidateContract :
    GeneralMovingTargetDiscreteDerivativeCandidateContract

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

interpolationLaw : String (explicit)

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

For s in [s_k,s_{k+1}], hat rho_s=Law(hat X_s), with endpoint laws rho_k^eta and rho_{k+1}^eta.

frozenConditionalDrift : String (explicit)

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

bar b_{k,s}(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].

fokkerPlanck : String (explicit)

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

partial_s hat rho_s = -div(hat rho_s*bar b_{k,s})+(sigma_eta^2/2)*Delta hat rho_s, then Delta hat rho_s is split relative to A_s=nabla log(hat rho_s/tilde pi_s); SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract records the weak-test source statement and SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff plus SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff compile only its test-indexed sign/coefficient packaging, while SALD.generalMovingTargetDiscreteConditionalFpSourceSignsHandoff and SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff consume the supplied analytic FP/Laplacian identities for algebraic regrouping.

klDerivativeIdentity : String (explicit)

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

d/ds KL(hat rho_s||tilde pi_s)=int partial_s hat rho_s*log(hat rho_s/tilde pi_s) - int (hat rho_s/tilde pi_s)*partial_s tilde pi_s; SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract records the cycle-73 handoff that applies the weak FP identity to the log-ratio test before integration by parts, SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSigns isolates the normalized source-sign-to-KL substitution, SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns composes that handoff through the cycle-72 admissible source-sign wrapper, and SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces composes it through the cycle-77 generator-piece source-sign wrapper.

frozenResidualDecomposition : String (explicit)

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

(sigma_eta^2/2)*nabla log tilde pi_s - bar b_{k,s} + tilde v_s = delta_pi^VA + dot{t}(s)*m_{t(s)}.

mYoungStep : String (explicit)

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

-dot{t}(s)*int hat rho_s <m_{t(s)},A_s> <= (sigma_eta^2/8)*FI + 2*sigma_eta^(-2)*dot{t}(s)^2*||m_{t(s)}||_{L2(hat rho_s)}^2.

frozenDeltaStep : String (explicit)

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

lem:frozen_delta_cross_lip bounds -int hat rho_s <delta_pi^VA,A_s> by (sigma_eta^2/8)*FI + 2*Gamma*eta^2*alpha'^(-1)*KL + 2*Delta*eta.

lsiStep : String (explicit)

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

After the two Young splits, LSI converts -(sigma_eta^2/4)*FI into -(sigma_eta^2/2)*C_LSI*K.

dvStep : String (explicit)

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

Apply DV with Z=alpha*||m_t||^2, using the discrete residual finite-log-mgf witness, to replace ||m_t||_{L2(hat rho_s)}^2 by alpha^(-1)*K+E_alpha(pi_t,m_t).

outputSInequality : String (explicit)

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

d/ds K_s <= -((sigma_eta^2/2)*C_LSI(t(s))-2*sigma_eta^(-2)*dot{t}(s)^2*alpha^(-1)-2*Gamma(t(s))*eta^2*alpha'^(-1))*K_s + 2*sigma_eta^(-2)*dot{t}(s)^2*E_alpha(pi_{t(s)},m_{t(s)}) + 2*Delta(t(s))*eta.

timeChangedInequality : String (explicit)

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

d/dt K(t) <= -((sigma_eta(t)^2/2)*dot{s}(t)*C_LSI(t)-2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*alpha^(-1)-2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t))*K(t) + 2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t)+2*dot{s}(t)*Delta(t)*eta.

requiredRegularity : List String (explicit)

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

Ordered data items

1. endpoint law matching for the general VA-SALD EM interpolation
2. conditional-drift weak Fokker--Planck equation with drift sign -div(hat rho_s*bar b_{k,s}) and diffusion sign +(sigma_eta^2/2)*Delta hat rho_s
3. density positivity, finite KL/FI, differentiation-under-integral, and integration-by-parts on every EM subinterval
4. constant inverse schedule and dot{s}(t)>0
5. positive sigma_eta(t) and finite residual L2/log-mgf terms

sourceGaps : List String (explicit)

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

Ordered data items

1. the interpolation Fokker--Planck equation and conditional drift are invoked as standard facts rather than stated as a lemma
2. the cycle-72 and cycle-69 lower theorems prove only weak-test/source-sign coefficient packaging, including the explicit admissible-test predicate variant, after the analytic weak FP identity is supplied; cycle 73 then substitutes that supplied weak FP identity into the differentiated KL display at the log-ratio test, with a lower wrapper composing through the cycle-72 admissible source-sign theorem; cycle 78 isolates the normalized source-sign-to-KL substitution and composes the same KL handoff through the cycle-77 generator-piece source-sign theorem, but none of these prove the weak FP theorem, conditional law, density, log-ratio admissibility, or integration-by-parts theorem
3. the proof applies a global Gronwall step after interval-wise estimates without isolating stitched-interval regularity
4. the source says to substitute Gamma(t) before the final inequality; the collection of all constants must be kept synchronized with lem:frozen_delta_cross_lip

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:frozen_delta_cross_lip
5. eq:LSI-KL-FI
6. lem:dv_variation
7. sald.general_moving_target_discrete.dv_finite_log_mgf_witness
8. sald.general_moving_target_discrete.derivative_side_conditions
9. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract
10. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff
11. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff
12. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract
13. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffScalar
14. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSigns
15. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns
16. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces
17. SALD.generalMovingTargetDiscreteConditionalFpSourceSignsHandoff
18. sald.general_moving_target_discrete.cycle69_em_fp_source_signs_lower
19. SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff
20. sald.general_moving_target_discrete.cycle54_em_fp_lower
21. sald.forward_kl.density_boundary_regular
22. sald.forward_kl.schedule_time_change

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 generalMovingTargetDiscreteDerivativeCandidateContract :
    GeneralMovingTargetDiscreteDerivativeCandidateContract where
  sourceBlock := saldGeneralMovingTargetDiscreteDerivativeSource
  interpolationLaw := "For s in [s_k,s_{k+1}], hat rho_s=Law(hat X_s), with endpoint laws rho_k^eta and rho_{k+1}^eta."
  frozenConditionalDrift := "bar b_{k,s}(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]."
  fokkerPlanck := "partial_s hat rho_s = -div(hat rho_s*bar b_{k,s})+(sigma_eta^2/2)*Delta hat rho_s, then Delta hat rho_s is split relative to A_s=nabla log(hat rho_s/tilde pi_s); SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract records the weak-test source statement and SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff plus SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff compile only its test-indexed sign/coefficient packaging, while SALD.generalMovingTargetDiscreteConditionalFpSourceSignsHandoff and SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff consume the supplied analytic FP/Laplacian identities for algebraic regrouping."
  klDerivativeIdentity := "d/ds KL(hat rho_s||tilde pi_s)=int partial_s hat rho_s*log(hat rho_s/tilde pi_s) - int (hat rho_s/tilde pi_s)*partial_s tilde pi_s; SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract records the cycle-73 handoff that applies the weak FP identity to the log-ratio test before integration by parts, SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSigns isolates the normalized source-sign-to-KL substitution, SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns composes that handoff through the cycle-72 admissible source-sign wrapper, and SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces composes it through the cycle-77 generator-piece source-sign wrapper."
  frozenResidualDecomposition := "(sigma_eta^2/2)*nabla log tilde pi_s - bar b_{k,s} + tilde v_s = delta_pi^VA + dot{t}(s)*m_{t(s)}."
  mYoungStep := "-dot{t}(s)*int hat rho_s <m_{t(s)},A_s> <= (sigma_eta^2/8)*FI + 2*sigma_eta^(-2)*dot{t}(s)^2*||m_{t(s)}||_{L2(hat rho_s)}^2."
  frozenDeltaStep := "lem:frozen_delta_cross_lip bounds -int hat rho_s <delta_pi^VA,A_s> by (sigma_eta^2/8)*FI + 2*Gamma*eta^2*alpha'^(-1)*KL + 2*Delta*eta."
  lsiStep := "After the two Young splits, LSI converts -(sigma_eta^2/4)*FI into -(sigma_eta^2/2)*C_LSI*K."
  dvStep := "Apply DV with Z=alpha*||m_t||^2, using the discrete residual finite-log-mgf witness, to replace ||m_t||_{L2(hat rho_s)}^2 by alpha^(-1)*K+E_alpha(pi_t,m_t)."
  outputSInequality := "d/ds K_s <= -((sigma_eta^2/2)*C_LSI(t(s))-2*sigma_eta^(-2)*dot{t}(s)^2*alpha^(-1)-2*Gamma(t(s))*eta^2*alpha'^(-1))*K_s + 2*sigma_eta^(-2)*dot{t}(s)^2*E_alpha(pi_{t(s)},m_{t(s)}) + 2*Delta(t(s))*eta."
  timeChangedInequality := "d/dt K(t) <= -((sigma_eta(t)^2/2)*dot{s}(t)*C_LSI(t)-2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*alpha^(-1)-2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t))*K(t) + 2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t)+2*dot{s}(t)*Delta(t)*eta."
  requiredRegularity := [
    "endpoint law matching for the general VA-SALD EM interpolation",
    "conditional-drift weak Fokker--Planck equation with drift sign -div(hat rho_s*bar b_{k,s}) and diffusion sign +(sigma_eta^2/2)*Delta hat rho_s",
    "density positivity, finite KL/FI, differentiation-under-integral, and integration-by-parts on every EM subinterval",
    "constant inverse schedule and dot{s}(t)>0",
    "positive sigma_eta(t) and finite residual L2/log-mgf terms"
  ]
  sourceGaps := [
    "the interpolation Fokker--Planck equation and conditional drift are invoked as standard facts rather than stated as a lemma",
    "the cycle-72 and cycle-69 lower theorems prove only weak-test/source-sign coefficient packaging, including the explicit admissible-test predicate variant, after the analytic weak FP identity is supplied; cycle 73 then substitutes that supplied weak FP identity into the differentiated KL display at the log-ratio test, with a lower wrapper composing through the cycle-72 admissible source-sign theorem; cycle 78 isolates the normalized source-sign-to-KL substitution and composes the same KL handoff through the cycle-77 generator-piece source-sign theorem, but none of these prove the weak FP theorem, conditional law, density, log-ratio admissibility, or integration-by-parts theorem",
    "the proof applies a global Gronwall step after interval-wise estimates without isolating stitched-interval regularity",
    "the source says to substitute Gamma(t) before the final inequality; the collection of all constants must be kept synchronized with lem:frozen_delta_cross_lip"
  ]
  dependencies := [
    "eq:SALD_general_EM",
    "eq:general_moving_target_SALD_frozen_interp",
    "eq:general_discrete_delta_def",
    "lem:frozen_delta_cross_lip",
    "eq:LSI-KL-FI",
    "lem:dv_variation",
    "sald.general_moving_target_discrete.dv_finite_log_mgf_witness",
    "sald.general_moving_target_discrete.derivative_side_conditions",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffScalar",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSigns",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces",
    "SALD.generalMovingTargetDiscreteConditionalFpSourceSignsHandoff",
    "sald.general_moving_target_discrete.cycle69_em_fp_source_signs_lower",
    "SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff",
    "sald.general_moving_target_discrete.cycle54_em_fp_lower",
    "sald.forward_kl.density_boundary_regular",
    "sald.forward_kl.schedule_time_change"
  ]
  status := ProofStatus.obligation