AutoSamplingTheory.SALD.saldGronwallExponentRewriteContract

Data definition / provenance and workflow record

Meaning and type

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

def saldGronwallExponentRewriteContract :
    GronwallExponentRewriteContract

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

startingFactor : String (explicit)

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

After appendix.tex:63, the remaining integral term is exp(-(int u in 0..t1, a u)) * int t in 0..t1, exp(int u in 0..t, a u) * b t dt.

intervalAdditivity : String (explicit)

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

For each t in [0,t1], use interval-integral additivity int_0^t1 a = int_0^t a + int_t^t1 a, with orientation handled exactly by the source interval 0 <= t <= t1.

negIntegralRewrite : String (explicit)

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

Rewrite -(int_0^t1 a) + int_0^t a as -(int_t^t1 a), without imposing sign assumptions on a; the scalar real identity is compiled as SALD.gronwallNegIntegralRewriteScalar once interval additivity supplies the three integral values.

expProductRewrite : String (explicit)

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

Use exp(x)*exp(y)=exp(x+y) to identify exp(-(int_0^t1 a))*exp(int_0^t a) with exp(-(int_t^t1 a)); the scalar Real.exp product step is compiled as SALD.gronwallExpProductRewriteScalar.

integralTermRewrite : String (explicit)

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

Push the pointwise exponential rewrite through the integral over t in [0,t1], preserving the multiplier b_t and the inequality direction from the previous line.

noSignAssumptions : String (explicit)

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

The rewrite uses only interval additivity and exponential algebra; it must not add positivity or monotonicity assumptions on a or b.

dependencies : List String (explicit)

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

Ordered data items

1. SALD.saldGronwallEndpointCalculusContract
2. SALD.gronwallNegIntegralRewriteScalar
3. SALD.gronwallExpProductRewriteScalar
4. SALD.gronwallIntervalIntegralAdditivityScalar
5. SALD.gronwallExpProductRewriteIntervalIntegral
6. SALD.gronwallExpProductRewriteIntegralCongr
7. SALD.gronwallEndpointIntegralRewrite
8. interval-integrability on adjacent Real intervals

sourceGaps : List String (explicit)

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

Ordered data items

1. appendix.tex:65-69 performs the exponent rewrite in one display; SALD.gronwallIntervalIntegralAdditivityScalar now supplies the adjacent-interval scalar equality once interval-integrability is proved
2. SALD.gronwallExpProductRewriteIntegralCongr now pushes the pointwise exponential rewrite through the t-integral once adjacent interval-integrability is supplied for each t in the source interval
3. SALD.gronwallEndpointIntegralRewrite now moves the endpoint inverse factor through the b_t integral and applies the compiled congruence

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 saldGronwallExponentRewriteContract :
    GronwallExponentRewriteContract where
  sourceBlock := saldGronwallExponentRewriteSource
  startingFactor := "After appendix.tex:63, the remaining integral term is exp(-(int u in 0..t1, a u)) * int t in 0..t1, exp(int u in 0..t, a u) * b t dt."
  intervalAdditivity := "For each t in [0,t1], use interval-integral additivity int_0^t1 a = int_0^t a + int_t^t1 a, with orientation handled exactly by the source interval 0 <= t <= t1."
  negIntegralRewrite := "Rewrite -(int_0^t1 a) + int_0^t a as -(int_t^t1 a), without imposing sign assumptions on a; the scalar real identity is compiled as SALD.gronwallNegIntegralRewriteScalar once interval additivity supplies the three integral values."
  expProductRewrite := "Use exp(x)*exp(y)=exp(x+y) to identify exp(-(int_0^t1 a))*exp(int_0^t a) with exp(-(int_t^t1 a)); the scalar Real.exp product step is compiled as SALD.gronwallExpProductRewriteScalar."
  integralTermRewrite := "Push the pointwise exponential rewrite through the integral over t in [0,t1], preserving the multiplier b_t and the inequality direction from the previous line."
  noSignAssumptions := "The rewrite uses only interval additivity and exponential algebra; it must not add positivity or monotonicity assumptions on a or b."
  dependencies := [
      "SALD.saldGronwallEndpointCalculusContract",
      "SALD.gronwallNegIntegralRewriteScalar",
      "SALD.gronwallExpProductRewriteScalar",
    "SALD.gronwallIntervalIntegralAdditivityScalar",
    "SALD.gronwallExpProductRewriteIntervalIntegral",
    "SALD.gronwallExpProductRewriteIntegralCongr",
    "SALD.gronwallEndpointIntegralRewrite",
    "interval-integrability on adjacent Real intervals"
  ]
  sourceGaps := [
    "appendix.tex:65-69 performs the exponent rewrite in one display; SALD.gronwallIntervalIntegralAdditivityScalar now supplies the adjacent-interval scalar equality once interval-integrability is proved",
    "SALD.gronwallExpProductRewriteIntegralCongr now pushes the pointwise exponential rewrite through the t-integral once adjacent interval-integrability is supplied for each t in the source interval",
    "SALD.gronwallEndpointIntegralRewrite now moves the endpoint inverse factor through the b_t integral and applies the compiled congruence"
  ]
  status := ProofStatus.obligation