AutoSamplingTheory.SALD.unifiedForwardKlSpecializationContract

Data definition / provenance and workflow record

Meaning and type

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

def unifiedForwardKlSpecializationContract :
    UnifiedForwardKlSpecializationContract

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

sourceProof : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

vaSaldDynamics : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

residualEquation : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

correctionEquation : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

generalTheorem : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

specialization : String (explicit)

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

Set c_t <- u_t in eq:general_moving_target_SALD; then the general SDE becomes VA-SALD eq:SALD_Ito because its score term is (sigma_t^2/2)*nabla log pi_t.

correctionFieldTransportBridge : String (explicit)

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

main_body.tex:359-368 combines prop:guided_path_residual with div(pi_t*w_t)=pi_t*(g_t-E_pi_t[g_t]) to infer partial_t pi_t+div(pi_t*(u_t+w_t))=0.

residualFieldIdentification : String (explicit)

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

Use v_t=u_t+w_t as the transport velocity for pi_t and c_t=u_t as the implementable velocity; the general residual m_t=v_t-c_t is w_t.

assumptionsBridge : String (explicit)

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

The unified theorem's LSI assumption and finite E_alpha0(pi_t,w_t) assumption are exactly the general theorem assumptions after m_t=w_t.

terminalBoundMatch : String (explicit)

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

Substituting m_t=w_t into eq:general_moving_target_KL_bound gives main_body.tex lines 374-390, with the same sigma-weighted exponents and residual complexity term.

proofRoute : List String (explicit)

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

Ordered data items

1. main_body.tex:359-363 quotes prop:guided_path_residual for the guided path residual.
2. main_body.tex:364-368 introduces w_t by the Poisson/divergence equation and states u_t+w_t is a transport velocity for pi_t.
3. main_body.tex:372-390 states the unified theorem with residual complexity E_alpha(pi_t,w_t).
4. appendix.tex:949-951 proves the theorem by specializing thm:general-moving-target-SALD with c_t <- u_t.

dependencies : List String (explicit)

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

Ordered data items

1. prop:guided_path_residual
2. eq:poisson-eq
3. eq:SALD_Ito
4. thm:general-moving-target-SALD
5. sald.guided_path_residual.identity
6. sald.general_moving_target.gronwall_application
7. sald.general_moving_target.gronwall_side_conditions

sourceGaps : List String (explicit)

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

Ordered data items

1. the source introduces w_t through a divergence equation but does not formalize existence, regularity, or boundary conditions for a solution
2. the transport-velocity bridge from the residual identity plus the correction equation to u_t+w_t generating pi_t is stated in prose and remains a local obligation
3. the equality between VA-SALD eq:SALD_Ito and the general moving-target SDE under c_t=u_t requires the guided-density score identity for pi_t
4. no direct theorem proof is supplied for thm:unified-forward-KL; the only faithful route is the specialization of thm:general-moving-target-SALD

lowerPacket : List String (explicit)

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

Ordered data items

1. Target the transport-velocity bridge u_t+w_t for pi_t before theorem-level proof search.
2. Keep the specialization c_t <- u_t and residual m_t=w_t exactly; do not introduce a direct VA-SALD proof.
3. Record existence and regularity of the correction field w_t as obligations unless a compiled Poisson/divergence backend is added.

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 unifiedForwardKlSpecializationContract :
    UnifiedForwardKlSpecializationContract where
  sourceStatement := saldUnifiedForwardKlSource
  sourceProof := saldUnifiedForwardKlProofSource
  vaSaldDynamics := saldVaSaldItoSource
  residualEquation := saldGuidedResidualMainSource
  correctionEquation := saldCorrectionFieldSource
  generalTheorem := saldGeneralMovingTargetSource
  specialization := "Set c_t <- u_t in eq:general_moving_target_SALD; then the general SDE becomes VA-SALD eq:SALD_Ito because its score term is (sigma_t^2/2)*nabla log pi_t."
  correctionFieldTransportBridge := "main_body.tex:359-368 combines prop:guided_path_residual with div(pi_t*w_t)=pi_t*(g_t-E_pi_t[g_t]) to infer partial_t pi_t+div(pi_t*(u_t+w_t))=0."
  residualFieldIdentification := "Use v_t=u_t+w_t as the transport velocity for pi_t and c_t=u_t as the implementable velocity; the general residual m_t=v_t-c_t is w_t."
  assumptionsBridge := "The unified theorem's LSI assumption and finite E_alpha0(pi_t,w_t) assumption are exactly the general theorem assumptions after m_t=w_t."
  terminalBoundMatch := "Substituting m_t=w_t into eq:general_moving_target_KL_bound gives main_body.tex lines 374-390, with the same sigma-weighted exponents and residual complexity term."
  proofRoute := [
    "main_body.tex:359-363 quotes prop:guided_path_residual for the guided path residual.",
    "main_body.tex:364-368 introduces w_t by the Poisson/divergence equation and states u_t+w_t is a transport velocity for pi_t.",
    "main_body.tex:372-390 states the unified theorem with residual complexity E_alpha(pi_t,w_t).",
    "appendix.tex:949-951 proves the theorem by specializing thm:general-moving-target-SALD with c_t <- u_t."
  ]
  dependencies := [
    "prop:guided_path_residual",
    "eq:poisson-eq",
    "eq:SALD_Ito",
    "thm:general-moving-target-SALD",
    "sald.guided_path_residual.identity",
    "sald.general_moving_target.gronwall_application",
    "sald.general_moving_target.gronwall_side_conditions"
  ]
  sourceGaps := [
    "the source introduces w_t through a divergence equation but does not formalize existence, regularity, or boundary conditions for a solution",
    "the transport-velocity bridge from the residual identity plus the correction equation to u_t+w_t generating pi_t is stated in prose and remains a local obligation",
    "the equality between VA-SALD eq:SALD_Ito and the general moving-target SDE under c_t=u_t requires the guided-density score identity for pi_t",
    "no direct theorem proof is supplied for thm:unified-forward-KL; the only faithful route is the specialization of thm:general-moving-target-SALD"
  ]
  lowerPacket := [
    "Target the transport-velocity bridge u_t+w_t for pi_t before theorem-level proof search.",
    "Keep the specialization c_t <- u_t and residual m_t=w_t exactly; do not introduce a direct VA-SALD proof.",
    "Record existence and regularity of the correction field w_t as obligations unless a compiled Poisson/divergence backend is added."
  ]
  status := ProofStatus.obligation