AutoSamplingTheory.SALD.discreteForwardKlAccumulatedErrorBridgeContract

Data definition / provenance and workflow record

Meaning and type

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

def discreteForwardKlAccumulatedErrorBridgeContract :
    DiscreteForwardKlAccumulatedErrorBridgeContract

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.

sourceProof : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

theoremStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

endpointBridge : String (explicit)

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

The Gronwall K(T) and K(0) rewrite to KL(rho_K^eta||pi_T) and KL(rho_0||pi_0) using EM endpoint laws, s(0)=0, S=s(T), and the linear slowdown t(s)=s/r.

gronwallOutput : String (explicit)

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

Start from appendix.tex:557-590: K(T)<=exp(-int_0^T a)*K(0)+int_0^T exp(-int_t^T a)*((dot{s})^(-1)*E_alpha+2*dot{s}*eta*Delta)dt, with a(t)=dot{s}*C_LSI-dot{s}^(-1)*alpha^(-1)-2*dot{s}*eta^2*alpha'^(-1)*Gamma.

linearSlowdownSubstitution : String (explicit)

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

For t(s)=s/r, dot{s}(t)=r and dot{s}(t)^(-1)=1/r, so a(t)=r*C_LSI(t)-(r*alpha)^(-1)-2*r*eta^2*alpha'^(-1)*Gamma(t).

initialExponentSplit : String (explicit)

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

Split exp(-int_0^T a) as exp(-r*int_0^T C_LSI(t)dt)*exp(T/(r*alpha)+2*r*eta^2*alpha'^(-1)*int_0^T Gamma(t)dt), matching main_body.tex lines 310-315 after barGamma identification.

residualExponentBound : String (explicit)

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

For each t, exp(-int_t^T a) is bounded by exp(T/(r*alpha)+2*r*eta^2*barGamma/alpha') after discarding the nonpositive LSI contribution and bounding interval integrals by the full [0,T] integrals.

alphaComplexityCollection : String (explicit)

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

The E_alpha term collects to (1/r)*A_alpha(pi,v), using A_alpha(pi,v)=int_0^T E_alpha(pi_t,v_t)dt.

gammaAccumulation : String (explicit)

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

barGamma denotes int_0^T Gamma(t)dt, so the Gamma contribution in the positive exponent is 2*r*eta^2*barGamma/alpha'.

deltaAccumulation : String (explicit)

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

barDelta_{alpha'} denotes int_0^T Delta(t)dt, so the residual Delta contribution collects to 2*r*eta*barDelta_{alpha'}.

dependencies : List String (explicit)

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

Ordered data items

1. lem:gronwall
2. def:alpha-complexity
3. sald.discrete_forward_kl.em_endpoint_laws
4. sald.discrete_forward_kl.stitched_interval_regularity
5. sald.discrete_forward_kl.gronwall_accumulation
6. sald.discrete_forward_kl.linear_slowdown_specialization
7. sald.discrete_forward_kl.residual_exponent_bound
8. SALD.discreteForwardKlGronwallCoeffIntervalIntegrable
9. SALD.discreteForwardKlGronwallCoeffIntegralSubSub
10. SALD.discreteForwardKlGronwallInitialExponentSplitScalar
11. SALD.discreteForwardKlGronwallInitialExponentSplitOfPieces
12. SALD.discreteForwardKlResidualExponentBoundScalar
13. SALD.discreteForwardKlResidualExpBoundScalar
14. SALD.discreteForwardKlAlphaComplexityCollectionScalar
15. SALD.discreteForwardKlDeltaAccumulationScalar
16. SALD.discreteForwardKlAccumulatedErrorCollectionScalar
17. SALD.discreteForwardKlResidualIntegralDisplayBoundScalar
18. SALD.discreteForwardKlMainDisplayBoundScalar

sourceGaps : List String (explicit)

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

Ordered data items

1. the appendix proof stops at the general-schedule Gronwall display and does not spell out the main-body linear-slowdown collection
2. the source states that barGamma and barDelta are controlled by smoothness and complexities but does not define the Lean integral objects or regularity assumptions
3. the residual exponent bound uses sign and interval-integral monotonicity facts implicitly
4. SALD.discreteForwardKlGronwallInitialExponentSplitOfPieces now formalizes the local three-piece exponent split once the source LSI, alpha, and Gamma coefficient integrability hypotheses are supplied
5. the compiled cycle-27 collection scalars only factor constants through interval integrals after A_alpha and barDelta have already been identified with the source full-interval integrals
6. SALD.discreteForwardKlResidualIntegralDisplayBoundScalar now composes the supplied residual-kernel bound with that collection algebra; endpoint stitching and residual exponent monotonicity remain obligations
7. SALD.discreteForwardKlMainDisplayBoundScalar now combines the supplied Gronwall initial term and supplied residual display into the exact two-term main-body bound, but does not prove the analytic source identifications

lowerPacket : List String (explicit)

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

Ordered data items

1. Prove the endpoint rewrites and exponent split before attempting the theorem-level discrete bound.
2. Cycle 46 lower compiled scalar core: SALD.discreteForwardKlGronwallCoeffIntervalIntegrable, SALD.discreteForwardKlGronwallCoeffIntegralSubSub, SALD.discreteForwardKlGronwallInitialExponentSplitScalar, and SALD.discreteForwardKlGronwallInitialExponentSplitOfPieces cover only the initial Gronwall exponent split under explicit interval-integrability inputs.
3. Refine sald.discrete_forward_kl.residual_exponent_bound as the lower scalar bridge for the residual Gronwall exponent before collecting the residual integral.
4. Use the source a(t) from appendix.tex:557-590 exactly; do not normalize away the Gamma term.
5. Separate the alpha-complexity, Gamma, and Delta integral collections so each can be checked against main_body.tex:309-323.
6. Cycle 27 lower target: after the coefficient-chain audit, focus on endpointBridge plus alphaComplexityCollection and deltaAccumulation, keeping residual-exponent monotonicity and barGamma identification as named obligations if they remain blocked.
7. Cycle 27 lower compiled scalar core: SALD.discreteForwardKlAlphaComplexityCollectionScalar, SALD.discreteForwardKlDeltaAccumulationScalar, and SALD.discreteForwardKlAccumulatedErrorCollectionScalar cover only constant-factor extraction for the additive residual integrals.
8. Cycle 61 lower compiled scalar wrapper: SALD.discreteForwardKlResidualIntegralDisplayBoundScalar connects a supplied common-exponential residual bound to the exact main-body additive display.
9. Cycle 66 lower compiled scalar wrapper: SALD.discreteForwardKlMainDisplayBoundScalar combines the supplied initial exponent split and supplied residual display into the exact main-body two-term bound.

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 discreteForwardKlAccumulatedErrorBridgeContract :
    DiscreteForwardKlAccumulatedErrorBridgeContract where
  sourceProof := saldForwardKlDiscreteAccumulatedErrorSource
  theoremStatement := saldForwardKlDiscreteSource
  endpointBridge := "The Gronwall K(T) and K(0) rewrite to KL(rho_K^eta||pi_T) and KL(rho_0||pi_0) using EM endpoint laws, s(0)=0, S=s(T), and the linear slowdown t(s)=s/r."
  gronwallOutput := "Start from appendix.tex:557-590: K(T)<=exp(-int_0^T a)*K(0)+int_0^T exp(-int_t^T a)*((dot{s})^(-1)*E_alpha+2*dot{s}*eta*Delta)dt, with a(t)=dot{s}*C_LSI-dot{s}^(-1)*alpha^(-1)-2*dot{s}*eta^2*alpha'^(-1)*Gamma."
  linearSlowdownSubstitution := "For t(s)=s/r, dot{s}(t)=r and dot{s}(t)^(-1)=1/r, so a(t)=r*C_LSI(t)-(r*alpha)^(-1)-2*r*eta^2*alpha'^(-1)*Gamma(t)."
  initialExponentSplit := "Split exp(-int_0^T a) as exp(-r*int_0^T C_LSI(t)dt)*exp(T/(r*alpha)+2*r*eta^2*alpha'^(-1)*int_0^T Gamma(t)dt), matching main_body.tex lines 310-315 after barGamma identification."
  residualExponentBound := "For each t, exp(-int_t^T a) is bounded by exp(T/(r*alpha)+2*r*eta^2*barGamma/alpha') after discarding the nonpositive LSI contribution and bounding interval integrals by the full [0,T] integrals."
  alphaComplexityCollection := "The E_alpha term collects to (1/r)*A_alpha(pi,v), using A_alpha(pi,v)=int_0^T E_alpha(pi_t,v_t)dt."
  gammaAccumulation := "barGamma denotes int_0^T Gamma(t)dt, so the Gamma contribution in the positive exponent is 2*r*eta^2*barGamma/alpha'."
  deltaAccumulation := "barDelta_{alpha'} denotes int_0^T Delta(t)dt, so the residual Delta contribution collects to 2*r*eta*barDelta_{alpha'}."
  dependencies := [
    "lem:gronwall",
    "def:alpha-complexity",
    "sald.discrete_forward_kl.em_endpoint_laws",
    "sald.discrete_forward_kl.stitched_interval_regularity",
    "sald.discrete_forward_kl.gronwall_accumulation",
    "sald.discrete_forward_kl.linear_slowdown_specialization",
    "sald.discrete_forward_kl.residual_exponent_bound",
    "SALD.discreteForwardKlGronwallCoeffIntervalIntegrable",
    "SALD.discreteForwardKlGronwallCoeffIntegralSubSub",
    "SALD.discreteForwardKlGronwallInitialExponentSplitScalar",
    "SALD.discreteForwardKlGronwallInitialExponentSplitOfPieces",
    "SALD.discreteForwardKlResidualExponentBoundScalar",
    "SALD.discreteForwardKlResidualExpBoundScalar",
    "SALD.discreteForwardKlAlphaComplexityCollectionScalar",
    "SALD.discreteForwardKlDeltaAccumulationScalar",
    "SALD.discreteForwardKlAccumulatedErrorCollectionScalar",
    "SALD.discreteForwardKlResidualIntegralDisplayBoundScalar",
    "SALD.discreteForwardKlMainDisplayBoundScalar"
  ]
  sourceGaps := [
    "the appendix proof stops at the general-schedule Gronwall display and does not spell out the main-body linear-slowdown collection",
    "the source states that barGamma and barDelta are controlled by smoothness and complexities but does not define the Lean integral objects or regularity assumptions",
    "the residual exponent bound uses sign and interval-integral monotonicity facts implicitly",
    "SALD.discreteForwardKlGronwallInitialExponentSplitOfPieces now formalizes the local three-piece exponent split once the source LSI, alpha, and Gamma coefficient integrability hypotheses are supplied",
    "the compiled cycle-27 collection scalars only factor constants through interval integrals after A_alpha and barDelta have already been identified with the source full-interval integrals",
    "SALD.discreteForwardKlResidualIntegralDisplayBoundScalar now composes the supplied residual-kernel bound with that collection algebra; endpoint stitching and residual exponent monotonicity remain obligations",
    "SALD.discreteForwardKlMainDisplayBoundScalar now combines the supplied Gronwall initial term and supplied residual display into the exact two-term main-body bound, but does not prove the analytic source identifications"
  ]
  lowerPacket := [
    "Prove the endpoint rewrites and exponent split before attempting the theorem-level discrete bound.",
    "Cycle 46 lower compiled scalar core: SALD.discreteForwardKlGronwallCoeffIntervalIntegrable, SALD.discreteForwardKlGronwallCoeffIntegralSubSub, SALD.discreteForwardKlGronwallInitialExponentSplitScalar, and SALD.discreteForwardKlGronwallInitialExponentSplitOfPieces cover only the initial Gronwall exponent split under explicit interval-integrability inputs.",
    "Refine sald.discrete_forward_kl.residual_exponent_bound as the lower scalar bridge for the residual Gronwall exponent before collecting the residual integral.",
    "Use the source a(t) from appendix.tex:557-590 exactly; do not normalize away the Gamma term.",
    "Separate the alpha-complexity, Gamma, and Delta integral collections so each can be checked against main_body.tex:309-323.",
    "Cycle 27 lower target: after the coefficient-chain audit, focus on endpointBridge plus alphaComplexityCollection and deltaAccumulation, keeping residual-exponent monotonicity and barGamma identification as named obligations if they remain blocked.",
    "Cycle 27 lower compiled scalar core: SALD.discreteForwardKlAlphaComplexityCollectionScalar, SALD.discreteForwardKlDeltaAccumulationScalar, and SALD.discreteForwardKlAccumulatedErrorCollectionScalar cover only constant-factor extraction for the additive residual integrals.",
    "Cycle 61 lower compiled scalar wrapper: SALD.discreteForwardKlResidualIntegralDisplayBoundScalar connects a supplied common-exponential residual bound to the exact main-body additive display.",
    "Cycle 66 lower compiled scalar wrapper: SALD.discreteForwardKlMainDisplayBoundScalar combines the supplied initial exponent split and supplied residual display into the exact main-body two-term bound."
  ]
  status := ProofStatus.obligation