AutoSamplingTheory.SALD.gronwallEndpointCalculusObligation

Data definition / provenance and workflow record

Meaning and type

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

def gronwallEndpointCalculusObligation : ProofObligation

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.

id : String (explicit)

Stable obligation identifier.

sald.gronwall.endpoint_calculus

statement : String (explicit)

Desired mathematical or workflow content as String; it is not a proposition in Prop and the def does not prove it.

Formalize the endpoint-safe calculus side conditions in appendix lines 55-69: choose a closed-interval derivative or absolute-continuity backend, differentiate the integrating factor exp(int_0^t a), integrate the derivative inequality from 0 to t1, evaluate endpoints, and rewrite exp(-int_0^t1 a)*exp(int_0^t a) as exp(-int_t^t1 a).

source : AutoSamplingTheory.SourceAnchor (explicit)

SourceAnchor supporting the intended requirement.

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

status : AutoSamplingTheory.ProofStatus (explicit)

Stored ProofStatus, default obligation; even an explicitly stored formalized does not independently certify a Lean theorem.

AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

dependsOn : List String (explicit)

List of declared dependency names as strings; may mix theorem names, obligations, source labels, or descriptions. Not the compiled dependency DAG.

Ordered data items

1. SALD.saldGronwallCandidateContract
2. SALD.saldGronwallEndpointCalculusContract
3. SALD.gronwallIntegratingFactorProductDerivative
4. SALD.gronwallIntegratingFactorDerivativeInequalityScalar
5. SALD.gronwallIntegratingFactorDerivativeLe
6. SALD.gronwallIntegratingFactorDerivativeLeOfIntegral
7. SALD.gronwallOrderIntegrationOfHasDerivAt
8. SALD.gronwallOrderIntegrationOfHasDerivRight
9. SALD.gronwallEndpointEvaluationScalar
10. SALD.gronwallEndpointMultiplyByExpNegScalar
11. SALD.gronwallEndpointIntegralRewrite
12. SALD.gronwallIntegratingFactorBoundOfDerivatives
13. SALD.gronwallIntegratingFactorBoundOfIntegral
14. SALD.gronwallIntegratingFactorBoundOfInteriorDerivatives
15. SALD.gronwallCoefficientSideConditionsOfContinuous
16. SALD.gronwallIntegratingFactorBoundOfContinuousData
17. SALD.gronwallIntegratingFactorBoundOfDifferentiable
18. SALD.gronwallIntegratingFactorBoundOfC1
19. SALD.gronwallIntegratingFactorBoundOfInteriorContinuousData
20. SALD.gronwallIntegratingFactorBoundOfInteriorC1
21. SALD.cycle41GronwallMiddleObligation
22. SALD.cycle41GronwallLowerObligation
23. Real intervalIntegral backend
24. Real.exp algebra

note : String (explicit)

Recorded evidence/caveats; may distinguish a compiled scalar helper from still-open source analysis.

This obligation refines the local Gronwall proof backend only. Cycle 31 proves the pointwise derivative inequality after local FTC and HasDerivAt inputs, and adds a compiled interval-order integration lemma plus endpoint scalar algebra. Cycle 36 middle proves the displayed bound under explicit global derivative/integrability hypotheses; cycle 36 lower proves the same display from continuous a, b, K, and K' plus the derivative inequality. Cycle 41 middle proves the same display with the paper derivative written as deriv K; cycle 41 lower adds the right-derivative FTC/order-integration assembly with no endpoint derivative hypotheses, while keeping the C1 or absolute-continuity interpretation explicit. It does not add sign assumptions on a or b, and it does not mark lem:gronwall formalized because the source-to-Mathlib closed-interval differentiability bridge remains open.

def gronwallEndpointCalculusObligation : ProofObligation where
  id := "sald.gronwall.endpoint_calculus"
  statement := "Formalize the endpoint-safe calculus side conditions in appendix lines 55-69: choose a closed-interval derivative or absolute-continuity backend, differentiate the integrating factor exp(int_0^t a), integrate the derivative inequality from 0 to t1, evaluate endpoints, and rewrite exp(-int_0^t1 a)*exp(int_0^t a) as exp(-int_t^t1 a)."
  source := saldGronwallSource
  status := ProofStatus.obligation
  dependsOn := [
    "SALD.saldGronwallCandidateContract",
    "SALD.saldGronwallEndpointCalculusContract",
    "SALD.gronwallIntegratingFactorProductDerivative",
    "SALD.gronwallIntegratingFactorDerivativeInequalityScalar",
    "SALD.gronwallIntegratingFactorDerivativeLe",
    "SALD.gronwallIntegratingFactorDerivativeLeOfIntegral",
    "SALD.gronwallOrderIntegrationOfHasDerivAt",
    "SALD.gronwallOrderIntegrationOfHasDerivRight",
    "SALD.gronwallEndpointEvaluationScalar",
    "SALD.gronwallEndpointMultiplyByExpNegScalar",
    "SALD.gronwallEndpointIntegralRewrite",
    "SALD.gronwallIntegratingFactorBoundOfDerivatives",
    "SALD.gronwallIntegratingFactorBoundOfIntegral",
    "SALD.gronwallIntegratingFactorBoundOfInteriorDerivatives",
    "SALD.gronwallCoefficientSideConditionsOfContinuous",
    "SALD.gronwallIntegratingFactorBoundOfContinuousData",
    "SALD.gronwallIntegratingFactorBoundOfDifferentiable",
    "SALD.gronwallIntegratingFactorBoundOfC1",
    "SALD.gronwallIntegratingFactorBoundOfInteriorContinuousData",
    "SALD.gronwallIntegratingFactorBoundOfInteriorC1",
    "SALD.cycle41GronwallMiddleObligation",
    "SALD.cycle41GronwallLowerObligation",
    "Real intervalIntegral backend",
    "Real.exp algebra"
  ]
  note := "This obligation refines the local Gronwall proof backend only. Cycle 31 proves the pointwise derivative inequality after local FTC and HasDerivAt inputs, and adds a compiled interval-order integration lemma plus endpoint scalar algebra. Cycle 36 middle proves the displayed bound under explicit global derivative/integrability hypotheses; cycle 36 lower proves the same display from continuous a, b, K, and K' plus the derivative inequality. Cycle 41 middle proves the same display with the paper derivative written as deriv K; cycle 41 lower adds the right-derivative FTC/order-integration assembly with no endpoint derivative hypotheses, while keeping the C1 or absolute-continuity interpretation explicit. It does not add sign assumptions on a or b, and it does not mark lem:gronwall formalized because the source-to-Mathlib closed-interval differentiability bridge remains open."