AutoSamplingTheory.SALD.cycle16UnifiedForwardKlTransportBridgeLowerContract

Data definition / provenance and workflow record

Meaning and type

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

def cycle16UnifiedForwardKlTransportBridgeLowerContract :
    UnifiedForwardKlTransportBridgeLowerContract

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

parentPacket : String (explicit)

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

SALD.cycle16UnifiedForwardKlTransportBridgeMiddleContract

targetObligation : String (explicit)

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

sald.unified_forward_kl.transport_velocity_bridge

residualEquation : String (explicit)

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

main_body.tex:359-363 gives partial_t pi_t + div(pi_t*u_t) = -pi_t*(g_t - E_pi_t[g_t]) from prop:guided_path_residual.

correctionEquation : String (explicit)

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

main_body.tex:364-367 assumes div(pi_t*w_t) = pi_t*(g_t - E_pi_t[g_t]) for the correction field w_t.

divergenceLinearity : String (explicit)

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

A future Lean proof needs a weak/product-divergence backend rewriting div(pi_t*(u_t+w_t)) as div(pi_t*u_t)+div(pi_t*w_t), with the required integrability and boundary conditions.

cancellationStep : String (explicit)

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

Adding the residual and correction displays cancels -pi_t*(g_t-E_pi_t[g_t]) with +pi_t*(g_t-E_pi_t[g_t]), yielding partial_t pi_t + div(pi_t*u_t) + div(pi_t*w_t) = 0.

transportVelocityConclusion : String (explicit)

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

After the divergence-linearity rewrite, the source conclusion is partial_t pi_t + div(pi_t*(u_t+w_t)) = 0, so v_t=u_t+w_t transports pi_t.

specializationIdentifications : String (explicit)

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

For appendix.tex:949-951, set c_t=u_t in thm:general-moving-target-SALD; with v_t=u_t+w_t, the residual m_t=v_t-c_t is w_t.

exclusions : List String (explicit)

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

Ordered data items

1. Do not prove existence, uniqueness, regularity, or boundary conditions for w_t in this lower slice.
2. Do not prove thm:unified-forward-KL directly; the source route remains specialization of thm:general-moving-target-SALD.
3. Do not enter residual DV, Gronwall, pure-contraction, or discrete EM proof search.

dependencies : List String (explicit)

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

Ordered data items

1. SALD.cycle16UnifiedForwardKlTransportBridgeMiddleContract
2. SALD.unifiedForwardKlSpecializationContract
3. sald.guided_path_residual.identity
4. eq:poisson-eq
5. TransportVelocityContract

sourceGaps : List String (explicit)

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

Ordered data items

1. The paper states the correction equation but does not construct w_t or prove its regularity.
2. The divergence algebra is written in classical notation; Lean still needs a weak or classical divergence interface for pi_t*u_t, pi_t*w_t, and pi_t*(u_t+w_t).
3. Boundary/no-flux or decay assumptions needed to interpret the continuity equation are not separated in the source theorem.

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 cycle16UnifiedForwardKlTransportBridgeLowerContract :
    UnifiedForwardKlTransportBridgeLowerContract where
  sourceBlock := saldUnifiedTransportBridgeSource
  parentPacket := "SALD.cycle16UnifiedForwardKlTransportBridgeMiddleContract"
  targetObligation := "sald.unified_forward_kl.transport_velocity_bridge"
  residualEquation := "main_body.tex:359-363 gives partial_t pi_t + div(pi_t*u_t) = -pi_t*(g_t - E_pi_t[g_t]) from prop:guided_path_residual."
  correctionEquation := "main_body.tex:364-367 assumes div(pi_t*w_t) = pi_t*(g_t - E_pi_t[g_t]) for the correction field w_t."
  divergenceLinearity := "A future Lean proof needs a weak/product-divergence backend rewriting div(pi_t*(u_t+w_t)) as div(pi_t*u_t)+div(pi_t*w_t), with the required integrability and boundary conditions."
  cancellationStep := "Adding the residual and correction displays cancels -pi_t*(g_t-E_pi_t[g_t]) with +pi_t*(g_t-E_pi_t[g_t]), yielding partial_t pi_t + div(pi_t*u_t) + div(pi_t*w_t) = 0."
  transportVelocityConclusion := "After the divergence-linearity rewrite, the source conclusion is partial_t pi_t + div(pi_t*(u_t+w_t)) = 0, so v_t=u_t+w_t transports pi_t."
  specializationIdentifications := "For appendix.tex:949-951, set c_t=u_t in thm:general-moving-target-SALD; with v_t=u_t+w_t, the residual m_t=v_t-c_t is w_t."
  exclusions := [
    "Do not prove existence, uniqueness, regularity, or boundary conditions for w_t in this lower slice.",
    "Do not prove thm:unified-forward-KL directly; the source route remains specialization of thm:general-moving-target-SALD.",
    "Do not enter residual DV, Gronwall, pure-contraction, or discrete EM proof search."
  ]
  dependencies := [
    "SALD.cycle16UnifiedForwardKlTransportBridgeMiddleContract",
    "SALD.unifiedForwardKlSpecializationContract",
    "sald.guided_path_residual.identity",
    "eq:poisson-eq",
    "TransportVelocityContract"
  ]
  sourceGaps := [
    "The paper states the correction equation but does not construct w_t or prove its regularity.",
    "The divergence algebra is written in classical notation; Lean still needs a weak or classical divergence interface for pi_t*u_t, pi_t*w_t, and pi_t*(u_t+w_t).",
    "Boundary/no-flux or decay assumptions needed to interpret the continuity equation are not separated in the source theorem."
  ]
  status := ProofStatus.obligation