Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

AutoSamplingTheory.SALD.cycle59MainSkeletonAnalyticMiddleObligation

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.

Lean statement of this data definition

The part after the colon is the output data type. This declaration takes no mathematical proof inputs.

def cycle59MainSkeletonAnalyticMiddleObligation : 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.main_skeleton.cycle59_middle_interface_audit
statement : String (explicit)

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

Cycle 59 middle verifies that the upper analytic-interface ledger is consumed in paper order by thm:forward-KL, thm:forward-KL-discrete, prop:guided_path_residual, thm:general-moving-target-SALD, thm:unified-forward-KL, and thm:general-moving-target-SALD-discrete. It keeps the next lower target exactly on sald.general_moving_target_discrete.gronwall_side_conditions over appendix.tex:1573-1600 for endpoint stitching, coefficient regularity, endpoint-safe Gronwall use, and exact display matching, while keeping all unproved analytic backends obligation or sourceCited.
source : AutoSamplingTheory.SourceAnchor (explicit)

SourceAnchor supporting the intended requirement.

AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteGronwallSideConditionSource — 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.cycle59MainSkeletonAnalyticMiddleContract
  2. SALD.cycle59MainSkeletonAnalyticInterfaceObligation
  3. SALD.cycle58UnifiedDiscreteGeneralMiddleObligation
  4. SALD.cycle56DiscreteForwardKlGronwallLowerObligation
  5. SALD.cycle55ForwardKlSkeletonMiddleObligation
  6. SALD.cycle57GuidedGeneralSkeletonMiddleObligation
  7. SALD.saldGronwallEndpointCalculusContract
  8. dvVariationalFormulaInterface saldDvVariationSource
  9. SALD.saldDvFiniteLogMgfContract
  10. SALD.saldLsiKlFiDensityTestContract
  11. SALD.forwardKlDerivativeSideConditionContract
  12. SALD.generalMovingTargetDerivativeCandidateContract
  13. SALD.discreteForwardKlEmInterpolationSideConditionContract
  14. SALD.generalMovingTargetDiscreteDerivativeSideConditionContract
  15. SALD.generalMovingTargetDiscretePointwiseGronwallInputOfPostDvTimeChanged
  16. SALD.generalMovingTargetDiscreteGronwallNamedCoefficientInput
  17. SALD.generalMovingTargetDiscreteGronwallEndpointRewriteScalar
  18. SALD.generalMovingTargetDiscreteGronwallSideConditionContract
  19. SALD.generalMovingTargetDiscreteGronwallSideConditionObligation
  20. sald.general_moving_target_discrete.gronwall_side_conditions
  21. lem:gronwall
  22. lem:dv_variation
  23. eq:LSI-KL-FI
note : String (explicit)

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

Middle workflow audit only. It adds no theorem hypotheses, changes no source constants, and does not promote Gronwall, DV, LSI/KL/FI, continuous FP/KL derivative, EM conditional-FP, discrete Gronwall stitching, theorem contracts, or SLT reuse statuses.
Exact Lean data construction

Each field assignment stores the corresponding value shown above. Omitted fields use the explicitly identified schema defaults. Strings that name theorems remain strings; they do not call those theorems.

def cycle59MainSkeletonAnalyticMiddleObligation : ProofObligation where
  id := "sald.main_skeleton.cycle59_middle_interface_audit"
  statement := "Cycle 59 middle verifies that the upper analytic-interface ledger is consumed in paper order by thm:forward-KL, thm:forward-KL-discrete, prop:guided_path_residual, thm:general-moving-target-SALD, thm:unified-forward-KL, and thm:general-moving-target-SALD-discrete. It keeps the next lower target exactly on sald.general_moving_target_discrete.gronwall_side_conditions over appendix.tex:1573-1600 for endpoint stitching, coefficient regularity, endpoint-safe Gronwall use, and exact display matching, while keeping all unproved analytic backends obligation or sourceCited."
  source := saldGeneralMovingTargetDiscreteGronwallSideConditionSource
  status := ProofStatus.obligation
  dependsOn := [
    "SALD.cycle59MainSkeletonAnalyticMiddleContract",
    "SALD.cycle59MainSkeletonAnalyticInterfaceObligation",
    "SALD.cycle58UnifiedDiscreteGeneralMiddleObligation",
    "SALD.cycle56DiscreteForwardKlGronwallLowerObligation",
    "SALD.cycle55ForwardKlSkeletonMiddleObligation",
    "SALD.cycle57GuidedGeneralSkeletonMiddleObligation",
    "SALD.saldGronwallEndpointCalculusContract",
    "dvVariationalFormulaInterface saldDvVariationSource",
    "SALD.saldDvFiniteLogMgfContract",
    "SALD.saldLsiKlFiDensityTestContract",
    "SALD.forwardKlDerivativeSideConditionContract",
    "SALD.generalMovingTargetDerivativeCandidateContract",
    "SALD.discreteForwardKlEmInterpolationSideConditionContract",
    "SALD.generalMovingTargetDiscreteDerivativeSideConditionContract",
    "SALD.generalMovingTargetDiscretePointwiseGronwallInputOfPostDvTimeChanged",
    "SALD.generalMovingTargetDiscreteGronwallNamedCoefficientInput",
    "SALD.generalMovingTargetDiscreteGronwallEndpointRewriteScalar",
    "SALD.generalMovingTargetDiscreteGronwallSideConditionContract",
    "SALD.generalMovingTargetDiscreteGronwallSideConditionObligation",
    "sald.general_moving_target_discrete.gronwall_side_conditions",
    "lem:gronwall",
    "lem:dv_variation",
    "eq:LSI-KL-FI"
  ]
  note := "Middle workflow audit only. It adds no theorem hypotheses, changes no source constants, and does not promote Gronwall, DV, LSI/KL/FI, continuous FP/KL derivative, EM conditional-FP, discrete Gronwall stitching, theorem contracts, or SLT reuse statuses."

/-- Cycle-59 lower obligation for the discrete general Gronwall/display
side-condition packet.

The proof-producing part of this lower packet is local: it introduces named
Gronwall coefficients from the cycle-58 pointwise derivative input and rewrites
the final Gronwall endpoint inequality to the theorem's KL endpoints.  The
analytic endpoint laws, coefficient regularity, stitched absolute continuity,
and `lem:gronwall` application remain obligations.
-/

Existing module entry · Audited data-reader index · All teaching coverage