AutoSamplingTheory.SALD.cycle28GeneralVaSaldMiddleContract

Data definition / provenance and workflow record

Meaning and type

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

def cycle28GeneralVaSaldMiddleContract :
    GeneralVaSaldGuidedPathMiddleContract

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.

guidedResidualSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

generalContinuousSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

unifiedSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

discreteSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

objective : String (explicit)

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

Translate appendix.tex:1469-1511 into a lower-ready middle ledger for sald.general_moving_target_discrete.derivative_side_conditions, preserving the frozen/residual algebra, the two sigma_eta^2/8 Young splits, and the resulting residual/Gamma/Delta coefficients while leaving EM/Fokker--Planck, LSI, DV, time-change, and Gronwall backends as named obligations.

sourceStepMap : List String (explicit)

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

Ordered data items

1. appendix.tex:1469-1478 rewrites (sigma_eta^2/2)*nabla log tilde pi_s - bar b_{k,s} + tilde v_s as delta_pi^VA + dot{t}(s)*m_{t(s)} using eq:general_discrete_delta_def and m_t=v_t-c_t.
2. appendix.tex:1481-1488 substitutes that decomposition into the KL derivative, splitting the cross term into frozen delta_pi^VA and residual dot{t}(s)*m_{t(s)} pieces.
3. appendix.tex:1493-1501 applies Young to the residual cross term with one sigma_eta^2/8 FI share and produces 2*sigma_eta^(-2)*dot{t}(s)^2*||m_{t(s)}||_{L2(hat rho_s)}^2.
4. appendix.tex:1503-1511 applies the frozen-delta lemma to the delta_pi^VA cross term, consuming the second sigma_eta^2/8 FI share and yielding 2*Gamma(t(s))*eta^2*alpha'^(-1)*KL plus 2*Delta(t(s))*eta.
5. appendix.tex:1513-1524 combines both Young outputs with the original -(sigma_eta^2/2)*FI dissipation, leaving -(sigma_eta^2/4)*FI before the LSI handoff.

leanStepMap : List String (explicit)

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

Ordered data items

1. SALD.generalMovingTargetDiscreteDerivativeSideConditionContract.frozenResidualAlgebra records the vector-field rewrite; SALD.generalMovingTargetDiscreteFrozenResidualAlgebraVector formalizes the module-level algebra once delta_pi^VA, tilde v_s, and m_t are identified.
2. SALD.generalMovingTargetDiscreteDerivativeSideConditionContract.youngCoefficientBookkeeping records the two sigma_eta^2/8 Young splits and the exact coefficients.
3. SALD.generalMovingTargetDiscreteYoungFisherShareScalar formalizes only the real identity that one quarter of (sigma_eta^2/2)*FI is (sigma_eta^2/8)*FI.
4. SALD.generalMovingTargetDiscreteTwoYoungFisherBudgetScalar formalizes only the real budget that two sigma_eta^2/8 shares leave -(sigma_eta^2/4)*FI.
5. SALD.generalMovingTargetDiscreteResidualYoungCoefficientScalar formalizes only the residual Young coefficient rewrite with epsilon=sigma_eta^2/4 after sigma_eta^(-2) is identified.
6. SALD.cycle28GeneralVaSaldDerivativeSideMiddleObligation keeps this middle map synchronized with sald.general_moving_target_discrete.derivative_side_conditions.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. lem:frozen_delta_cross_lip is still an obligation through SALD.generalMovingTargetDiscreteFrozenDeltaObligation; this packet only records its use at appendix.tex:1503-1511.
2. eq:LSI-KL-FI starts after the two Young splits, at appendix.tex:1526-1542, and remains the inherited density-test obligation.
3. lem:dv_variation starts at appendix.tex:1544 and remains source-cited through the residual DV finite-log-mgf witness.
4. No SLT theorem applies to the frozen/residual algebra or the local Young coefficient bookkeeping.

obligations : List String (explicit)

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

Ordered data items

1. sald.general_moving_target_discrete.cycle28_derivative_side_middle
2. sald.general_moving_target_discrete.derivative_side_conditions
3. sald.general_moving_target_discrete.em_interpolation_fp
4. sald.general_moving_target_discrete.frozen_delta_cross_lip
5. probability.lsi_to_kl_fi
6. sald.general_moving_target_discrete.dv_finite_log_mgf_witness
7. sald.forward_kl.schedule_time_change
8. sald.general_moving_target_discrete.kl_derivative

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.generalMovingTargetDiscreteDerivativeSideConditionContract / SALD.generalMovingTargetDiscreteDerivativeSideConditionObligation / sald.general_moving_target_discrete.derivative_side_conditions.
2. Preferred lower sub-slice: prove or refine the frozen/residual algebra in appendix.tex:1469-1478, then use the compiled scalar Young bookkeeping helpers only after the analytic Young and FI identities are supplied.
3. Keep the frozen-delta lemma, LSI-to-KL/FI, residual DV finite-log-mgf, s-to-t time change, and final Gronwall/display bridge as separate dependencies.
4. Do not add regularity, endpoint, positivity, finite-energy, or coefficient assumptions to thm:general-moving-target-SALD-discrete; refine named obligations instead.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. Every source step from appendix.tex:1469-1511 is classified as Lean contract, compiled scalar helper, cited result, or named obligation.
2. SALD.generalVaSaldDiscreteContract lists SALD.cycle28GeneralVaSaldDerivativeSideMiddleObligation and still keeps the theorem contractOnly.
3. SALD.generalVaSaldDiscreteProofDag contains ASTIS.SALD.general_moving_target_discrete.cycle28_middle_derivative_side_conditions between the upper packet and derivative_side_conditions block.
4. SALD.saldDependenciesForLabel "thm:general-moving-target-SALD-discrete" includes SALD.cycle28GeneralVaSaldMiddleContract, sald.general_moving_target_discrete.cycle28_derivative_side_middle, and the three compiled scalar Young bookkeeping helpers.
5. The theorem display, source coefficients, source file selection, and analytic dependency statuses are unchanged.

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 cycle28GeneralVaSaldMiddleContract :
    GeneralVaSaldGuidedPathMiddleContract where
  guidedResidualSource := saldGuidedResidualSource
  generalContinuousSource := saldGeneralMovingTargetSource
  unifiedSource := saldUnifiedForwardKlSource
  discreteSource := saldGeneralMovingTargetDiscreteSource
  objective := "Translate appendix.tex:1469-1511 into a lower-ready middle ledger for sald.general_moving_target_discrete.derivative_side_conditions, preserving the frozen/residual algebra, the two sigma_eta^2/8 Young splits, and the resulting residual/Gamma/Delta coefficients while leaving EM/Fokker--Planck, LSI, DV, time-change, and Gronwall backends as named obligations."
  sourceStepMap := [
    "appendix.tex:1469-1478 rewrites (sigma_eta^2/2)*nabla log tilde pi_s - bar b_{k,s} + tilde v_s as delta_pi^VA + dot{t}(s)*m_{t(s)} using eq:general_discrete_delta_def and m_t=v_t-c_t.",
    "appendix.tex:1481-1488 substitutes that decomposition into the KL derivative, splitting the cross term into frozen delta_pi^VA and residual dot{t}(s)*m_{t(s)} pieces.",
    "appendix.tex:1493-1501 applies Young to the residual cross term with one sigma_eta^2/8 FI share and produces 2*sigma_eta^(-2)*dot{t}(s)^2*||m_{t(s)}||_{L2(hat rho_s)}^2.",
    "appendix.tex:1503-1511 applies the frozen-delta lemma to the delta_pi^VA cross term, consuming the second sigma_eta^2/8 FI share and yielding 2*Gamma(t(s))*eta^2*alpha'^(-1)*KL plus 2*Delta(t(s))*eta.",
    "appendix.tex:1513-1524 combines both Young outputs with the original -(sigma_eta^2/2)*FI dissipation, leaving -(sigma_eta^2/4)*FI before the LSI handoff."
  ]
  leanStepMap := [
    "SALD.generalMovingTargetDiscreteDerivativeSideConditionContract.frozenResidualAlgebra records the vector-field rewrite; SALD.generalMovingTargetDiscreteFrozenResidualAlgebraVector formalizes the module-level algebra once delta_pi^VA, tilde v_s, and m_t are identified.",
    "SALD.generalMovingTargetDiscreteDerivativeSideConditionContract.youngCoefficientBookkeeping records the two sigma_eta^2/8 Young splits and the exact coefficients.",
    "SALD.generalMovingTargetDiscreteYoungFisherShareScalar formalizes only the real identity that one quarter of (sigma_eta^2/2)*FI is (sigma_eta^2/8)*FI.",
    "SALD.generalMovingTargetDiscreteTwoYoungFisherBudgetScalar formalizes only the real budget that two sigma_eta^2/8 shares leave -(sigma_eta^2/4)*FI.",
    "SALD.generalMovingTargetDiscreteResidualYoungCoefficientScalar formalizes only the residual Young coefficient rewrite with epsilon=sigma_eta^2/4 after sigma_eta^(-2) is identified.",
    "SALD.cycle28GeneralVaSaldDerivativeSideMiddleObligation keeps this middle map synchronized with sald.general_moving_target_discrete.derivative_side_conditions."
  ]
  citedResultInterfaces := [
    "lem:frozen_delta_cross_lip is still an obligation through SALD.generalMovingTargetDiscreteFrozenDeltaObligation; this packet only records its use at appendix.tex:1503-1511.",
    "eq:LSI-KL-FI starts after the two Young splits, at appendix.tex:1526-1542, and remains the inherited density-test obligation.",
    "lem:dv_variation starts at appendix.tex:1544 and remains source-cited through the residual DV finite-log-mgf witness.",
    "No SLT theorem applies to the frozen/residual algebra or the local Young coefficient bookkeeping."
  ]
  obligations := [
    "sald.general_moving_target_discrete.cycle28_derivative_side_middle",
    "sald.general_moving_target_discrete.derivative_side_conditions",
    "sald.general_moving_target_discrete.em_interpolation_fp",
    "sald.general_moving_target_discrete.frozen_delta_cross_lip",
    "probability.lsi_to_kl_fi",
    "sald.general_moving_target_discrete.dv_finite_log_mgf_witness",
    "sald.forward_kl.schedule_time_change",
    "sald.general_moving_target_discrete.kl_derivative"
  ]
  lowerPacket := [
    "Target exactly SALD.generalMovingTargetDiscreteDerivativeSideConditionContract / SALD.generalMovingTargetDiscreteDerivativeSideConditionObligation / sald.general_moving_target_discrete.derivative_side_conditions.",
    "Preferred lower sub-slice: prove or refine the frozen/residual algebra in appendix.tex:1469-1478, then use the compiled scalar Young bookkeeping helpers only after the analytic Young and FI identities are supplied.",
    "Keep the frozen-delta lemma, LSI-to-KL/FI, residual DV finite-log-mgf, s-to-t time change, and final Gronwall/display bridge as separate dependencies.",
    "Do not add regularity, endpoint, positivity, finite-energy, or coefficient assumptions to thm:general-moving-target-SALD-discrete; refine named obligations instead."
  ]
  reviewerChecklist := [
    "Every source step from appendix.tex:1469-1511 is classified as Lean contract, compiled scalar helper, cited result, or named obligation.",
    "SALD.generalVaSaldDiscreteContract lists SALD.cycle28GeneralVaSaldDerivativeSideMiddleObligation and still keeps the theorem contractOnly.",
    "SALD.generalVaSaldDiscreteProofDag contains ASTIS.SALD.general_moving_target_discrete.cycle28_middle_derivative_side_conditions between the upper packet and derivative_side_conditions block.",
    "SALD.saldDependenciesForLabel \"thm:general-moving-target-SALD-discrete\" includes SALD.cycle28GeneralVaSaldMiddleContract, sald.general_moving_target_discrete.cycle28_derivative_side_middle, and the three compiled scalar Young bookkeeping helpers.",
    "The theorem display, source coefficients, source file selection, and analytic dependency statuses are unchanged."
  ]
  status := ProofStatus.obligation