AutoSamplingTheory.SALD.cycle19DiscreteForwardKlMiddleContract

Data definition / provenance and workflow record

Meaning and type

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

def cycle19DiscreteForwardKlMiddleContract :
    DiscreteForwardKlEmDefectAccumulationMiddleContract

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

interpolationSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

derivativeSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

gronwallSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

accumulatedSource : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlDiscreteAccumulatedErrorSource — 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 the cycle-19 accumulated-error bridge into a lower-ready map for sald.discrete_forward_kl.accumulated_error_bridge, with sald.discrete_forward_kl.residual_exponent_bound isolated as the first scalar sub-slice and all source constants preserved.

sourceStepMap : List String (explicit)

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

Ordered data items

1. appendix.tex:557-571: Gronwall gives the initial-error term with a(t)=dot{s}(t)*C_LSI(t)-dot{s}(t)^(-1)*alpha^(-1)-2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t).
2. appendix.tex:573-589: the residual integral uses the same exponential kernel and b(t)=dot{s}(t)^(-1)*E_alpha(pi_t,v_t)+2*dot{s}(t)*eta*Delta(t).
3. main_body.tex:299-323: the theorem specializes to linear slowdown t(s)=s/r, so dot{s}(t)=r and the positive exponent is T/(r*alpha)+2*r*eta^2*barGamma/alpha'.
4. main_body.tex:310-323: the endpoint term keeps the LSI contraction factor exp(-r*int_0^T C_LSI(t)dt), while the residual integral is bounded by the common positive exponential factor.
5. main_body.tex:316-323: the residual b(t) collection becomes (1/r)*A_alpha(pi,v)+2*r*eta*barDelta_{alpha'} using the source definitions of A_alpha, barGamma, and barDelta.

leanStepMap : List String (explicit)

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

Ordered data items

1. The theorem statement remains SALD.discreteForwardKlStatementContract and SALD.discreteSaldContract; this middle packet changes neither.
2. The source Gronwall output is tracked by SALD.discreteForwardKlGronwallInstantiationContract and sald.discrete_forward_kl.gronwall_accumulation.
3. The final bridge is tracked by SALD.discreteForwardKlAccumulatedErrorBridgeContract and sald.discrete_forward_kl.accumulated_error_bridge.
4. The first lower scalar target is SALD.discreteForwardKlResidualExponentBoundObligation / sald.discrete_forward_kl.residual_exponent_bound.
5. Endpoint rewrites are inherited from sald.discrete_forward_kl.em_endpoint_laws and sald.discrete_forward_kl.stitched_interval_regularity; they are dependencies of the bridge, not new theorem assumptions.
6. The coefficient audit remains SALD.discreteForwardKlCoefficientChainAuditContract, which checks the Gamma, Delta, barGamma, barDelta, alpha, alpha', eta, and r constants against the source displays.

citedResultInterfaces : List String (explicit)

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

Ordered data items

1. lem:gronwall remains a local real-analysis obligation; this packet only maps the scalar output after Gronwall is invoked.
2. lem:dv_variation remains source-cited through the existing discrete DV velocity witness and is not reopened by this accumulated-error packet.
3. eq:LSI-KL-FI remains an inherited obligation; the only LSI use here is the sign C_LSI(t)>=0 needed to drop the nonpositive residual exponent contribution.
4. No SLT theorem is used for endpoint rewrites, exponent splitting, residual exponent monotonicity, or barGamma/barDelta collection.

obligations : List String (explicit)

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

Ordered data items

1. sald.discrete_forward_kl.cycle19_accumulated_error_middle
2. sald.discrete_forward_kl.accumulated_error_bridge
3. sald.discrete_forward_kl.residual_exponent_bound
4. sald.discrete_forward_kl.linear_slowdown_specialization
5. sald.discrete_forward_kl.gronwall_accumulation
6. sald.discrete_forward_kl.em_endpoint_laws
7. sald.discrete_forward_kl.stitched_interval_regularity
8. sald.discrete_forward_kl.coefficient_chain_audit
9. sald.gronwall.integrating_factor

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.discreteForwardKlAccumulatedErrorBridgeContract / SALD.discreteForwardKlAccumulatedErrorBridgeObligation / sald.discrete_forward_kl.accumulated_error_bridge.
2. First sub-slice: sald.discrete_forward_kl.residual_exponent_bound, proving only the residual exponent drop and the replacement of interval Gamma integrals by the full barGamma contribution.
3. Do not alter the source a(t), b(t), theorem endpoint, alpha ranges, step-size condition, Gamma, Delta, barGamma, or barDelta definitions.
4. Keep endpoint matching and stitched-interval regularity as explicit dependencies; if those are blocked, refine those obligations rather than adding assumptions to thm:forward-KL-discrete.
5. Leave the frozen one-step defect, DV velocity witness, LSI bridge, and full Gronwall lemma outside this lower slice.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.discreteForwardKlProofDag contains the cycle-19 middle accumulated-error block between the upper packet and the linear-slowdown/residual-exponent/accumulated-error blocks.
2. SALD.saldDependenciesForLabel "thm:forward-KL-discrete" includes SALD.cycle19DiscreteForwardKlMiddleContract and sald.discrete_forward_kl.cycle19_accumulated_error_middle.
3. The conversion window, proof-obligation ledger, and SLT audit classify this packet as local real/integral algebra plus source-contract gaps, not as a proof of thm:forward-KL-discrete.
4. No analytic dependency is promoted beyond its current obligation/source-cited status.

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 cycle19DiscreteForwardKlMiddleContract :
    DiscreteForwardKlEmDefectAccumulationMiddleContract where
  sourceStatement := saldForwardKlDiscreteSource
  interpolationSource := saldForwardKlDiscreteInterpolationSource
  derivativeSource := saldForwardKlDiscreteDerivativeSource
  gronwallSource := saldForwardKlDiscreteGronwallSource
  accumulatedSource := saldForwardKlDiscreteAccumulatedErrorSource
  objective := "Translate the cycle-19 accumulated-error bridge into a lower-ready map for sald.discrete_forward_kl.accumulated_error_bridge, with sald.discrete_forward_kl.residual_exponent_bound isolated as the first scalar sub-slice and all source constants preserved."
  sourceStepMap := [
    "appendix.tex:557-571: Gronwall gives the initial-error term with a(t)=dot{s}(t)*C_LSI(t)-dot{s}(t)^(-1)*alpha^(-1)-2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t).",
    "appendix.tex:573-589: the residual integral uses the same exponential kernel and b(t)=dot{s}(t)^(-1)*E_alpha(pi_t,v_t)+2*dot{s}(t)*eta*Delta(t).",
    "main_body.tex:299-323: the theorem specializes to linear slowdown t(s)=s/r, so dot{s}(t)=r and the positive exponent is T/(r*alpha)+2*r*eta^2*barGamma/alpha'.",
    "main_body.tex:310-323: the endpoint term keeps the LSI contraction factor exp(-r*int_0^T C_LSI(t)dt), while the residual integral is bounded by the common positive exponential factor.",
    "main_body.tex:316-323: the residual b(t) collection becomes (1/r)*A_alpha(pi,v)+2*r*eta*barDelta_{alpha'} using the source definitions of A_alpha, barGamma, and barDelta."
  ]
  leanStepMap := [
    "The theorem statement remains SALD.discreteForwardKlStatementContract and SALD.discreteSaldContract; this middle packet changes neither.",
    "The source Gronwall output is tracked by SALD.discreteForwardKlGronwallInstantiationContract and sald.discrete_forward_kl.gronwall_accumulation.",
    "The final bridge is tracked by SALD.discreteForwardKlAccumulatedErrorBridgeContract and sald.discrete_forward_kl.accumulated_error_bridge.",
    "The first lower scalar target is SALD.discreteForwardKlResidualExponentBoundObligation / sald.discrete_forward_kl.residual_exponent_bound.",
    "Endpoint rewrites are inherited from sald.discrete_forward_kl.em_endpoint_laws and sald.discrete_forward_kl.stitched_interval_regularity; they are dependencies of the bridge, not new theorem assumptions.",
    "The coefficient audit remains SALD.discreteForwardKlCoefficientChainAuditContract, which checks the Gamma, Delta, barGamma, barDelta, alpha, alpha', eta, and r constants against the source displays."
  ]
  citedResultInterfaces := [
    "lem:gronwall remains a local real-analysis obligation; this packet only maps the scalar output after Gronwall is invoked.",
    "lem:dv_variation remains source-cited through the existing discrete DV velocity witness and is not reopened by this accumulated-error packet.",
    "eq:LSI-KL-FI remains an inherited obligation; the only LSI use here is the sign C_LSI(t)>=0 needed to drop the nonpositive residual exponent contribution.",
    "No SLT theorem is used for endpoint rewrites, exponent splitting, residual exponent monotonicity, or barGamma/barDelta collection."
  ]
  obligations := [
    "sald.discrete_forward_kl.cycle19_accumulated_error_middle",
    "sald.discrete_forward_kl.accumulated_error_bridge",
    "sald.discrete_forward_kl.residual_exponent_bound",
    "sald.discrete_forward_kl.linear_slowdown_specialization",
    "sald.discrete_forward_kl.gronwall_accumulation",
    "sald.discrete_forward_kl.em_endpoint_laws",
    "sald.discrete_forward_kl.stitched_interval_regularity",
    "sald.discrete_forward_kl.coefficient_chain_audit",
    "sald.gronwall.integrating_factor"
  ]
  lowerPacket := [
    "Target exactly SALD.discreteForwardKlAccumulatedErrorBridgeContract / SALD.discreteForwardKlAccumulatedErrorBridgeObligation / sald.discrete_forward_kl.accumulated_error_bridge.",
    "First sub-slice: sald.discrete_forward_kl.residual_exponent_bound, proving only the residual exponent drop and the replacement of interval Gamma integrals by the full barGamma contribution.",
    "Do not alter the source a(t), b(t), theorem endpoint, alpha ranges, step-size condition, Gamma, Delta, barGamma, or barDelta definitions.",
    "Keep endpoint matching and stitched-interval regularity as explicit dependencies; if those are blocked, refine those obligations rather than adding assumptions to thm:forward-KL-discrete.",
    "Leave the frozen one-step defect, DV velocity witness, LSI bridge, and full Gronwall lemma outside this lower slice."
  ]
  reviewerChecklist := [
    "SALD.discreteForwardKlProofDag contains the cycle-19 middle accumulated-error block between the upper packet and the linear-slowdown/residual-exponent/accumulated-error blocks.",
    "SALD.saldDependenciesForLabel \"thm:forward-KL-discrete\" includes SALD.cycle19DiscreteForwardKlMiddleContract and sald.discrete_forward_kl.cycle19_accumulated_error_middle.",
    "The conversion window, proof-obligation ledger, and SLT audit classify this packet as local real/integral algebra plus source-contract gaps, not as a proof of thm:forward-KL-discrete.",
    "No analytic dependency is promoted beyond its current obligation/source-cited status."
  ]
  status := ProofStatus.obligation

/-- Cycle-23 upper packet for the discrete forward-KL proof spine.

This returns to `thm:forward-KL-discrete` after the continuous forward-KL
coefficient work.  It keeps the full source route visible for middle, but
chooses one lower-facing target so the next proof attempt audits constants and
side conditions rather than proving the theorem.
-/