AutoSamplingTheory.SALD.discreteForwardKlCoefficientChainAuditContract

Data definition / provenance and workflow record

Meaning and type

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

def discreteForwardKlCoefficientChainAuditContract :
    DiscreteForwardKlCoefficientChainAuditContract

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.saldForwardKlDiscreteCoefficientChainSource — 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

frozenCrossCoefficient : String (explicit)

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

appendix.tex:454-467 uses lem:frozen_delta_cross_lip_sald to contribute (1/4)*FI + 2*eta^2*alpha'^(-1)*Gamma(t(s))*K_s + 2*eta*Delta(t(s)).

movingCrossCoefficient : String (explicit)

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

appendix.tex:469-479 applies Young to the moving-target velocity cross term, contributing another (1/4)*FI plus ||tilde v_s||_{L2(hat rho_s)}^2.

lsiStep : String (explicit)

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

After the two quarter-FI cross-term bounds, appendix.tex:481-493 leaves -(1/2)*FI and uses eq:LSI-KL-FI to obtain -C_LSI(t(s))*K_s.

dvVelocityCoefficient : String (explicit)

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

appendix.tex:496-515 applies lem:dv_variation with Z=alpha*||v_{t(s)}||^2 under the EM-interpolation witness, yielding dot t(s)^2*(alpha^(-1)*K_s + E_alpha(pi_{t(s)},v_{t(s)})).

timeChangeStep : String (explicit)

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

appendix.tex:534-553 multiplies by dot{s}(t), rewrites dot{s}(t)*dot t(s(t))^2 as dot{s}(t)^(-1), and produces the source t-inequality with +2*dot{s}(t)*eta*Delta(t).

gronwallA : String (explicit)

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

a(t)=dot{s}(t)*C_LSI(t)-dot{s}(t)^(-1)*alpha^(-1)-2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t).

gronwallB : String (explicit)

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

b(t)=dot{s}(t)^(-1)*E_alpha(pi_t,v_t)+2*dot{s}(t)*eta*Delta(t).

linearSlowdownExponent : String (explicit)

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

For t(s)=s/r, main_body.tex:309-321 requires exp(-r*int_0^T C_LSI(t)dt)*exp(T/(r*alpha)+2*r*eta^2*barGamma/alpha') for the initial term and the positive exponent factor for the residual term.

accumulatedErrorCollection : String (explicit)

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

The residual integral must collect to (1/r)*A_alpha(pi,v)+2*r*eta*barDelta_{alpha'} using barGamma=int_0^T Gamma(t)dt and barDelta_{alpha'}=int_0^T Delta(t)dt.

endpointBridge : String (explicit)

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

The Gronwall output identifies K(T)=KL(rho_K^eta||pi_T) and K(0)=KL(rho_0||pi_0) through the EM endpoint laws and linear slowdown endpoints.

sourceLineLedger : List String (explicit)

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

Ordered data items

1. appendix.tex:454-467: the frozen defect contributes the first 1/4*FI term plus 2*eta^2*alpha'^(-1)*Gamma*K and 2*eta*Delta.
2. appendix.tex:469-479: the moving velocity Young bound contributes the second 1/4*FI term plus ||tilde v_s||^2.
3. appendix.tex:481-493: the remaining -(1/2)*FI is converted by eq:LSI-KL-FI into -C_LSI(t(s))*K_s.
4. appendix.tex:496-515: DV with Z=alpha*||v_{t(s)}||^2 under the EM-interpolation witness contributes dot t(s)^2*alpha^(-1)*K_s and dot t(s)^2*E_alpha(pi_t,v_t).
5. appendix.tex:534-553: the time change multiplies by dot{s}(t), rewrites dot{s}*dot t^2 to dot{s}^(-1) using SALD.discreteForwardKlTimeChangeSquareCoefficientRewriteScalar once inverse-schedule side conditions are supplied, and preserves the Gamma and Delta coefficients.
6. appendix.tex:557-590 and main_body.tex:309-323: Gronwall plus t(s)=s/r gives T/(r*alpha), 2*r*eta^2*barGamma/alpha', (1/r)*A_alpha(pi,v), and 2*r*eta*barDelta_{alpha'}.

scalarSideConditions : List String (explicit)

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

Ordered data items

1. alpha>0 and alpha'>0 are required for the inverse coefficients alpha^(-1) and alpha'^(-1) in the source a(t) and b(t).
2. hat rho_s and tilde pi_s must satisfy the common-space, absolute-continuity, and finite-log-mgf interfaces required by the DV witness at appendix.tex:493-523.
3. dot{s}(t)>0 and dot t(s(t))=dot{s}(t)^(-1) are required inputs for SALD.discreteForwardKlTimeChangeSquareCoefficientRewriteScalar; under linear slowdown the nonzero/positive derivative follows from r>=1.
4. C_LSI(t)>=0 is used only to discard the nonpositive LSI contribution in residual exponents, not as a new theorem assumption.
5. Gamma, Delta, E_alpha(pi_t,v_t), and C_LSI must be interval-integrable on [0,T] for the Gronwall and accumulation expressions.
6. The residual exponent bound uses interval-integral monotonicity to replace int_t^T Gamma and int_t^T dot{s}^(-1)*alpha^(-1) by the full positive exponent T/(r*alpha)+2*r*eta^2*barGamma/alpha'.
7. Endpoint continuity of the stitched EM KL path is needed before K(T) and K(0) can be rewritten as the theorem endpoints.

dependencies : List String (explicit)

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

Ordered data items

1. eq:LSI-KL-FI
2. def:alpha-complexity
3. lem:dv_variation
4. lem:gronwall
5. sald.discrete_forward_kl.em_endpoint_laws
6. sald.discrete_forward_kl.stitched_interval_regularity
7. sald.discrete_forward_kl.frozen_delta_cross_lip
8. sald.discrete_forward_kl.kl_derivative
9. sald.discrete_forward_kl.dv_finite_log_mgf_witness
10. sald.discrete_forward_kl.dv_velocity_bound
11. SALD.discreteForwardKlTimeChangeSquareCoefficientRewriteScalar
12. sald.discrete_forward_kl.gronwall_accumulation
13. sald.discrete_forward_kl.linear_slowdown_specialization
14. sald.discrete_forward_kl.residual_exponent_bound
15. sald.discrete_forward_kl.accumulated_error_bridge

sourceGaps : List String (explicit)

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

Ordered data items

1. the SALD-specific frozen-defect proof is omitted and must be supplied by a faithful specialization of the later general lemma
2. the inverse-schedule identity dot t(s(t))=dot{s}(t)^(-1) and nonzero dot{s}(t) are still analytic side conditions; only the scalar coefficient algebra after those inputs is formalized
3. the source applies Gronwall after interval-wise EM inequalities without a standalone stitched-interval lemma
4. the appendix gives the general-schedule Gronwall display, while the main-body theorem supplies the final linear-slowdown collected constants

lowerPacket : List String (explicit)

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

Ordered data items

1. Target the scalar coefficient algebra from appendix.tex:454-553 before attempting the full discrete theorem.
2. Keep the two 1/4 FI Young contributions, the full DV coefficient dot{s}^(-1)*alpha^(-1), and the one-step 2*dot{s}*eta^2*alpha'^(-1)*Gamma term unchanged; SALD.discreteForwardKlTimeChangeSquareCoefficientRewriteScalar covers only the scalar dot{s}*dot t^2 rewrite.
3. Use sald.discrete_forward_kl.accumulated_error_bridge for the endpoint, exponent, barGamma, and barDelta collection tied to main_body.tex:309-323.

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 discreteForwardKlCoefficientChainAuditContract :
    DiscreteForwardKlCoefficientChainAuditContract where
  sourceProof := saldForwardKlDiscreteCoefficientChainSource
  theoremStatement := saldForwardKlDiscreteSource
  frozenCrossCoefficient := "appendix.tex:454-467 uses lem:frozen_delta_cross_lip_sald to contribute (1/4)*FI + 2*eta^2*alpha'^(-1)*Gamma(t(s))*K_s + 2*eta*Delta(t(s))."
  movingCrossCoefficient := "appendix.tex:469-479 applies Young to the moving-target velocity cross term, contributing another (1/4)*FI plus ||tilde v_s||_{L2(hat rho_s)}^2."
  lsiStep := "After the two quarter-FI cross-term bounds, appendix.tex:481-493 leaves -(1/2)*FI and uses eq:LSI-KL-FI to obtain -C_LSI(t(s))*K_s."
  dvVelocityCoefficient := "appendix.tex:496-515 applies lem:dv_variation with Z=alpha*||v_{t(s)}||^2 under the EM-interpolation witness, yielding dot t(s)^2*(alpha^(-1)*K_s + E_alpha(pi_{t(s)},v_{t(s)}))."
  timeChangeStep := "appendix.tex:534-553 multiplies by dot{s}(t), rewrites dot{s}(t)*dot t(s(t))^2 as dot{s}(t)^(-1), and produces the source t-inequality with +2*dot{s}(t)*eta*Delta(t)."
  gronwallA := "a(t)=dot{s}(t)*C_LSI(t)-dot{s}(t)^(-1)*alpha^(-1)-2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t)."
  gronwallB := "b(t)=dot{s}(t)^(-1)*E_alpha(pi_t,v_t)+2*dot{s}(t)*eta*Delta(t)."
  linearSlowdownExponent := "For t(s)=s/r, main_body.tex:309-321 requires exp(-r*int_0^T C_LSI(t)dt)*exp(T/(r*alpha)+2*r*eta^2*barGamma/alpha') for the initial term and the positive exponent factor for the residual term."
  accumulatedErrorCollection := "The residual integral must collect to (1/r)*A_alpha(pi,v)+2*r*eta*barDelta_{alpha'} using barGamma=int_0^T Gamma(t)dt and barDelta_{alpha'}=int_0^T Delta(t)dt."
  endpointBridge := "The Gronwall output identifies K(T)=KL(rho_K^eta||pi_T) and K(0)=KL(rho_0||pi_0) through the EM endpoint laws and linear slowdown endpoints."
  sourceLineLedger := [
    "appendix.tex:454-467: the frozen defect contributes the first 1/4*FI term plus 2*eta^2*alpha'^(-1)*Gamma*K and 2*eta*Delta.",
    "appendix.tex:469-479: the moving velocity Young bound contributes the second 1/4*FI term plus ||tilde v_s||^2.",
    "appendix.tex:481-493: the remaining -(1/2)*FI is converted by eq:LSI-KL-FI into -C_LSI(t(s))*K_s.",
    "appendix.tex:496-515: DV with Z=alpha*||v_{t(s)}||^2 under the EM-interpolation witness contributes dot t(s)^2*alpha^(-1)*K_s and dot t(s)^2*E_alpha(pi_t,v_t).",
    "appendix.tex:534-553: the time change multiplies by dot{s}(t), rewrites dot{s}*dot t^2 to dot{s}^(-1) using SALD.discreteForwardKlTimeChangeSquareCoefficientRewriteScalar once inverse-schedule side conditions are supplied, and preserves the Gamma and Delta coefficients.",
    "appendix.tex:557-590 and main_body.tex:309-323: Gronwall plus t(s)=s/r gives T/(r*alpha), 2*r*eta^2*barGamma/alpha', (1/r)*A_alpha(pi,v), and 2*r*eta*barDelta_{alpha'}."
  ]
  scalarSideConditions := [
    "alpha>0 and alpha'>0 are required for the inverse coefficients alpha^(-1) and alpha'^(-1) in the source a(t) and b(t).",
    "hat rho_s and tilde pi_s must satisfy the common-space, absolute-continuity, and finite-log-mgf interfaces required by the DV witness at appendix.tex:493-523.",
    "dot{s}(t)>0 and dot t(s(t))=dot{s}(t)^(-1) are required inputs for SALD.discreteForwardKlTimeChangeSquareCoefficientRewriteScalar; under linear slowdown the nonzero/positive derivative follows from r>=1.",
    "C_LSI(t)>=0 is used only to discard the nonpositive LSI contribution in residual exponents, not as a new theorem assumption.",
    "Gamma, Delta, E_alpha(pi_t,v_t), and C_LSI must be interval-integrable on [0,T] for the Gronwall and accumulation expressions.",
    "The residual exponent bound uses interval-integral monotonicity to replace int_t^T Gamma and int_t^T dot{s}^(-1)*alpha^(-1) by the full positive exponent T/(r*alpha)+2*r*eta^2*barGamma/alpha'.",
    "Endpoint continuity of the stitched EM KL path is needed before K(T) and K(0) can be rewritten as the theorem endpoints."
  ]
  dependencies := [
    "eq:LSI-KL-FI",
    "def:alpha-complexity",
    "lem:dv_variation",
    "lem:gronwall",
    "sald.discrete_forward_kl.em_endpoint_laws",
    "sald.discrete_forward_kl.stitched_interval_regularity",
    "sald.discrete_forward_kl.frozen_delta_cross_lip",
    "sald.discrete_forward_kl.kl_derivative",
    "sald.discrete_forward_kl.dv_finite_log_mgf_witness",
    "sald.discrete_forward_kl.dv_velocity_bound",
    "SALD.discreteForwardKlTimeChangeSquareCoefficientRewriteScalar",
    "sald.discrete_forward_kl.gronwall_accumulation",
    "sald.discrete_forward_kl.linear_slowdown_specialization",
    "sald.discrete_forward_kl.residual_exponent_bound",
    "sald.discrete_forward_kl.accumulated_error_bridge"
  ]
  sourceGaps := [
    "the SALD-specific frozen-defect proof is omitted and must be supplied by a faithful specialization of the later general lemma",
    "the inverse-schedule identity dot t(s(t))=dot{s}(t)^(-1) and nonzero dot{s}(t) are still analytic side conditions; only the scalar coefficient algebra after those inputs is formalized",
    "the source applies Gronwall after interval-wise EM inequalities without a standalone stitched-interval lemma",
    "the appendix gives the general-schedule Gronwall display, while the main-body theorem supplies the final linear-slowdown collected constants"
  ]
  lowerPacket := [
    "Target the scalar coefficient algebra from appendix.tex:454-553 before attempting the full discrete theorem.",
    "Keep the two 1/4 FI Young contributions, the full DV coefficient dot{s}^(-1)*alpha^(-1), and the one-step 2*dot{s}*eta^2*alpha'^(-1)*Gamma term unchanged; SALD.discreteForwardKlTimeChangeSquareCoefficientRewriteScalar covers only the scalar dot{s}*dot t^2 rewrite.",
    "Use sald.discrete_forward_kl.accumulated_error_bridge for the endpoint, exponent, barGamma, and barDelta collection tied to main_body.tex:309-323."
  ]
  status := ProofStatus.obligation