AutoSamplingTheory.SALD.generalMovingTargetDerivativeCandidateContract

Data definition / provenance and workflow record

Meaning and type

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

def generalMovingTargetDerivativeCandidateContract :
    GeneralMovingTargetDerivativeCandidateContract

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

densityAndLawInterface : String (explicit)

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

rho_s is the law of eq:general_moving_target_SALD, pi_{t(s)} is the slowed target, rho_s << pi_{t(s)}, and KL/FI are finite along the interval.

dynamicsFokkerPlanck : String (explicit)

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

partial_s rho_s = -div(dot{t}(s)*c_{t(s)}*rho_s)+(sigma_{t(s)}^2/2)*div(rho_s*nabla log(rho_s/pi_{t(s)})).

targetVelocity : String (explicit)

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

v_t generates pi_t, hence tilde v_s=dot{t}(s)*v_{t(s)} generates pi_{t(s)}.

residualVelocity : String (explicit)

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

m_t=v_t-c_t; the c_t drift and target-velocity term combine as -dot{t}(s)*int rho_s <m_{t(s)},A_s>.

klDerivativeIdentity : String (explicit)

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

d/ds KL(rho_s||pi_{t(s)}) = int partial_s rho_s log(rho_s/pi_{t(s)}) dx - int (rho_s/pi_{t(s)}) partial_s pi_{t(s)} dx.

firstTermEvaluation : String (explicit)

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

The general VA-SALD Fokker--Planck equation and integration by parts give dot{t}(s)*int rho_s <c_{t(s)},A_s> -(sigma_{t(s)}^2/2)*FI(rho_s||pi_{t(s)}). SALD.generalMovingTargetKlDerivativeResidualSplitScalar consumes this as a supplied scalar identity.

secondTermEvaluation : String (explicit)

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

The target transport equation gives -int rho_s <dot{t}(s)*v_{t(s)},A_s>; together with the supplied mass-conservation drop and m_t=v_t-c_t identification, SALD.generalMovingTargetKlDerivativeResidualSplitScalar derives the residual derivative display. SALD.generalMovingTargetKlDerivativeScaledResidualDisplayScalar additionally records the dot{t}(s) scaling and the source sign -dot{t}(s)*int rho_s <m_{t(s)},A_s>.

youngStep : String (explicit)

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

With epsilon=2*dot{t}(s)/sigma_{t(s)}^2 as stated in the source route, the residual cross term is bounded by (sigma_{t(s)}^2/4)*FI plus sigma_{t(s)}^(-2)*dot{t}(s)^2*||m_{t(s)}||_{L2(rho_s)}^2; SALD.generalMovingTargetPostYoungDerivativeBoundScalar compiles only the subsequent real-order subtraction.

lsiStep : String (explicit)

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

LSI gives FI(rho_s||pi_{t(s)}) >= 2*C_LSI(t(s))*KL(rho_s||pi_{t(s)}); SALD.generalMovingTargetLsiDerivativeBoundScalar consumes the supplied half-Fisher comparison without proving the density-test backend.

timeChangedInequality : String (explicit)

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

dK/dt <= -(sigma_t^2/2)*dot{s}(t)*C_LSI(t)*K(t)+sigma_t^(-2)*dot{s}(t)^(-1)*||m_t||_{L2(rho_{s(t)})}^2; SALD.generalMovingTargetTimeChangedDerivativeBoundScalar and SALD.generalMovingTargetPreDvDerivativeBoundScalar compile the scalar schedule handoff after inverse-schedule inputs are supplied.

requiredRegularity : List String (explicit)

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

Ordered data items

1. smooth positive densities for rho_s and pi_{t(s)}
2. valid Fokker--Planck equation for eq:general_moving_target_SALD
3. integration-by-parts hypotheses for both c_t and v_t terms
4. positive sigma_t and dot{s}(t), with inverse-schedule identity dot{t}(s(t))=dot{s}(t)^(-1)
5. finite KL/FI and L2 residual-energy terms

sourceGaps : List String (explicit)

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

Ordered data items

1. the source theorem does not isolate the regularity assumptions needed for the general Fokker--Planck and integration-by-parts steps
2. the inverse-schedule calculus is reused from the SALD proof but not restated for the sigma-weighted general theorem
3. positivity and regularity of sigma_t are used by sigma_t^(-2) and Young's inequality but are not packaged as a standalone assumption

dependencies : List String (explicit)

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

Ordered data items

1. eq:general_moving_target_SALD
2. TransportVelocityContract
3. KLContract
4. FIContract
5. eq:LSI-KL-FI
6. SALD.generalMovingTargetKlDerivativeResidualSplitScalar
7. SALD.generalMovingTargetKlDerivativeScaledResidualDisplayScalar
8. SALD.generalMovingTargetPostYoungDerivativeBoundScalar
9. SALD.generalMovingTargetLsiDerivativeBoundScalar
10. SALD.generalMovingTargetTimeChangedDerivativeBoundScalar
11. SALD.generalMovingTargetPreDvDerivativeBoundScalar
12. SALD.generalMovingTargetKlDerivativePreDvBoundOfSplitScalar
13. sald.forward_kl.density_boundary_regular
14. 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 generalMovingTargetDerivativeCandidateContract :
    GeneralMovingTargetDerivativeCandidateContract where
  sourceBlock := saldGeneralMovingTargetDerivativeSource
  densityAndLawInterface := "rho_s is the law of eq:general_moving_target_SALD, pi_{t(s)} is the slowed target, rho_s << pi_{t(s)}, and KL/FI are finite along the interval."
  dynamicsFokkerPlanck := "partial_s rho_s = -div(dot{t}(s)*c_{t(s)}*rho_s)+(sigma_{t(s)}^2/2)*div(rho_s*nabla log(rho_s/pi_{t(s)}))."
  targetVelocity := "v_t generates pi_t, hence tilde v_s=dot{t}(s)*v_{t(s)} generates pi_{t(s)}."
  residualVelocity := "m_t=v_t-c_t; the c_t drift and target-velocity term combine as -dot{t}(s)*int rho_s <m_{t(s)},A_s>."
  klDerivativeIdentity := "d/ds KL(rho_s||pi_{t(s)}) = int partial_s rho_s log(rho_s/pi_{t(s)}) dx - int (rho_s/pi_{t(s)}) partial_s pi_{t(s)} dx."
  firstTermEvaluation := "The general VA-SALD Fokker--Planck equation and integration by parts give dot{t}(s)*int rho_s <c_{t(s)},A_s> -(sigma_{t(s)}^2/2)*FI(rho_s||pi_{t(s)}). SALD.generalMovingTargetKlDerivativeResidualSplitScalar consumes this as a supplied scalar identity."
  secondTermEvaluation := "The target transport equation gives -int rho_s <dot{t}(s)*v_{t(s)},A_s>; together with the supplied mass-conservation drop and m_t=v_t-c_t identification, SALD.generalMovingTargetKlDerivativeResidualSplitScalar derives the residual derivative display. SALD.generalMovingTargetKlDerivativeScaledResidualDisplayScalar additionally records the dot{t}(s) scaling and the source sign -dot{t}(s)*int rho_s <m_{t(s)},A_s>."
  youngStep := "With epsilon=2*dot{t}(s)/sigma_{t(s)}^2 as stated in the source route, the residual cross term is bounded by (sigma_{t(s)}^2/4)*FI plus sigma_{t(s)}^(-2)*dot{t}(s)^2*||m_{t(s)}||_{L2(rho_s)}^2; SALD.generalMovingTargetPostYoungDerivativeBoundScalar compiles only the subsequent real-order subtraction."
  lsiStep := "LSI gives FI(rho_s||pi_{t(s)}) >= 2*C_LSI(t(s))*KL(rho_s||pi_{t(s)}); SALD.generalMovingTargetLsiDerivativeBoundScalar consumes the supplied half-Fisher comparison without proving the density-test backend."
  timeChangedInequality := "dK/dt <= -(sigma_t^2/2)*dot{s}(t)*C_LSI(t)*K(t)+sigma_t^(-2)*dot{s}(t)^(-1)*||m_t||_{L2(rho_{s(t)})}^2; SALD.generalMovingTargetTimeChangedDerivativeBoundScalar and SALD.generalMovingTargetPreDvDerivativeBoundScalar compile the scalar schedule handoff after inverse-schedule inputs are supplied."
  requiredRegularity := [
    "smooth positive densities for rho_s and pi_{t(s)}",
    "valid Fokker--Planck equation for eq:general_moving_target_SALD",
    "integration-by-parts hypotheses for both c_t and v_t terms",
    "positive sigma_t and dot{s}(t), with inverse-schedule identity dot{t}(s(t))=dot{s}(t)^(-1)",
    "finite KL/FI and L2 residual-energy terms"
  ]
  sourceGaps := [
    "the source theorem does not isolate the regularity assumptions needed for the general Fokker--Planck and integration-by-parts steps",
    "the inverse-schedule calculus is reused from the SALD proof but not restated for the sigma-weighted general theorem",
    "positivity and regularity of sigma_t are used by sigma_t^(-2) and Young's inequality but are not packaged as a standalone assumption"
  ]
  dependencies := [
    "eq:general_moving_target_SALD",
    "TransportVelocityContract",
    "KLContract",
    "FIContract",
    "eq:LSI-KL-FI",
    "SALD.generalMovingTargetKlDerivativeResidualSplitScalar",
    "SALD.generalMovingTargetKlDerivativeScaledResidualDisplayScalar",
    "SALD.generalMovingTargetPostYoungDerivativeBoundScalar",
    "SALD.generalMovingTargetLsiDerivativeBoundScalar",
    "SALD.generalMovingTargetTimeChangedDerivativeBoundScalar",
    "SALD.generalMovingTargetPreDvDerivativeBoundScalar",
    "SALD.generalMovingTargetKlDerivativePreDvBoundOfSplitScalar",
    "sald.forward_kl.density_boundary_regular",
    "sald.forward_kl.schedule_time_change"
  ]
  status := ProofStatus.obligation