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

AutoSamplingTheory.SALD.forwardKlMiddleSourceToLeanMapObligation

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 forwardKlMiddleSourceToLeanMapObligation : 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.forward_kl.middle_source_to_lean_map
statement : String (explicit)

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

Maintain the cycle-14/18/22 source-to-Lean maps, the cycle-26 upper/middle DV-witness packets, the cycle-30 derivative-side upper/middle packets, the cycle-34 derivative scalar/time-change packet, and the cycle-39 source-shaped derivative middle packet for continuous thm:forward-KL: appendix lines 168-252 and main_body lines 218-248 must map to the existing statement contract, derivative side conditions, LSI bridge, DV witness, coefficient-chain audit, Gronwall side conditions, and lower packet without changing the theorem statement or promoting analytic backends.
source : AutoSamplingTheory.SourceAnchor (explicit)

SourceAnchor supporting the intended requirement.

AutoSamplingTheory.SALD.saldForwardKlProofSource — 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.cycle14ForwardKlUpperPacket
  2. SALD.cycle14ForwardKlMiddleContract
  3. SALD.cycle18ForwardKlUpperPacket
  4. SALD.cycle18ForwardKlMiddleContract
  5. SALD.cycle22ForwardKlUpperPacket
  6. SALD.cycle22ForwardKlMiddleContract
  7. SALD.cycle26ForwardKlUpperPacket
  8. SALD.cycle26ForwardKlMiddleContract
  9. SALD.cycle30ForwardKlUpperPacket
  10. SALD.cycle30ForwardKlMiddleContract
  11. SALD.cycle34ForwardKlDerivativeUpperPacket
  12. SALD.cycle34ForwardKlDerivativeMiddleContract
  13. SALD.cycle39ForwardKlDerivativeUpperPacket
  14. SALD.cycle39ForwardKlDerivativeMiddleContract
  15. sald.forward_kl.cycle30_derivative_side_upper
  16. sald.forward_kl.cycle30_derivative_side_middle
  17. sald.forward_kl.cycle30_density_boundary_lower
  18. sald.forward_kl.cycle34_derivative_scalar
  19. sald.forward_kl.cycle34_derivative_middle
  20. sald.forward_kl.cycle39_derivative_upper
  21. sald.forward_kl.cycle39_derivative_middle
  22. SALD.continuousForwardKlStatementContract
  23. SALD.forwardKlFirstTermFisherSubstitutionScalar
  24. SALD.forwardKlTargetTransportYoungBoundScalar
  25. SALD.forwardKlPostYoungDerivativeBoundScalar
  26. SALD.forwardKlPostYoungDerivativeBoundOfCauchyScalar
  27. SALD.forwardKlLsiDerivativeBoundScalar
  28. SALD.forwardKlTimeChangedDerivativeBoundScalar
  29. SALD.forwardKlInverseScheduleDerivativeScalar
  30. SALD.forwardKlTimeChangeSquareCoefficientRewriteOfProductScalar
  31. SALD.forwardKlVelocitySquareScalingScalar
  32. SALD.forwardKlTimeChangedDerivativeBoundOfProductScalar
  33. SALD.forwardKlPreDvDerivativeBoundScalar
  34. SALD.forwardKlPreDvDerivativeBoundOfProductScalar
  35. SALD.forwardKlPreDvDerivativeBoundOfVelocityScalingScalar
  36. sald.forward_kl.endpoint_schedule_identities
  37. sald.forward_kl.moving_target_dependency_chain
  38. sald.forward_kl.density_boundary_regular
  39. sald.forward_kl.schedule_time_change
  40. sald.forward_kl.kl_derivative
  41. probability.lsi_to_kl_fi
  42. sald.forward_kl.cycle26_dv_witness_middle
  43. sald.forward_kl.dv_finite_log_mgf_witness
  44. sald.forward_kl.dv_energy_bound
  45. sald.forward_kl.coefficient_chain_audit
  46. sald.forward_kl.gronwall_application
  47. sald.forward_kl.gronwall_side_conditions
note : String (explicit)

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

This is a workflow obligation for middle-role synchronization. Cycle 14 selected endpoint schedule identities, cycles 18 and 22 selected Gronwall side-condition refinements, cycle 26 selects and maps the DV finite-log-mgf witness, cycle 30 returns to the derivative-side density/boundary and slowed-target transport interface, cycle 34 adds scalar post-Young/LSI/time-change handoffs, and cycle 39 adds source-shaped scalar schedule/velocity lemmas for appendix.tex:191-228; DV, LSI, Gronwall, schedule calculus, and KL derivative facts remain unformalized.
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 forwardKlMiddleSourceToLeanMapObligation : ProofObligation where
  id := "sald.forward_kl.middle_source_to_lean_map"
  statement := "Maintain the cycle-14/18/22 source-to-Lean maps, the cycle-26 upper/middle DV-witness packets, the cycle-30 derivative-side upper/middle packets, the cycle-34 derivative scalar/time-change packet, and the cycle-39 source-shaped derivative middle packet for continuous thm:forward-KL: appendix lines 168-252 and main_body lines 218-248 must map to the existing statement contract, derivative side conditions, LSI bridge, DV witness, coefficient-chain audit, Gronwall side conditions, and lower packet without changing the theorem statement or promoting analytic backends."
  source := saldForwardKlProofSource
  status := ProofStatus.obligation
  dependsOn := [
    "SALD.cycle14ForwardKlUpperPacket",
    "SALD.cycle14ForwardKlMiddleContract",
    "SALD.cycle18ForwardKlUpperPacket",
    "SALD.cycle18ForwardKlMiddleContract",
    "SALD.cycle22ForwardKlUpperPacket",
      "SALD.cycle22ForwardKlMiddleContract",
      "SALD.cycle26ForwardKlUpperPacket",
      "SALD.cycle26ForwardKlMiddleContract",
      "SALD.cycle30ForwardKlUpperPacket",
      "SALD.cycle30ForwardKlMiddleContract",
      "SALD.cycle34ForwardKlDerivativeUpperPacket",
      "SALD.cycle34ForwardKlDerivativeMiddleContract",
      "SALD.cycle39ForwardKlDerivativeUpperPacket",
      "SALD.cycle39ForwardKlDerivativeMiddleContract",
      "sald.forward_kl.cycle30_derivative_side_upper",
      "sald.forward_kl.cycle30_derivative_side_middle",
      "sald.forward_kl.cycle30_density_boundary_lower",
      "sald.forward_kl.cycle34_derivative_scalar",
      "sald.forward_kl.cycle34_derivative_middle",
      "sald.forward_kl.cycle39_derivative_upper",
      "sald.forward_kl.cycle39_derivative_middle",
      "SALD.continuousForwardKlStatementContract",
      "SALD.forwardKlFirstTermFisherSubstitutionScalar",
      "SALD.forwardKlTargetTransportYoungBoundScalar",
      "SALD.forwardKlPostYoungDerivativeBoundScalar",
      "SALD.forwardKlPostYoungDerivativeBoundOfCauchyScalar",
      "SALD.forwardKlLsiDerivativeBoundScalar",
      "SALD.forwardKlTimeChangedDerivativeBoundScalar",
      "SALD.forwardKlInverseScheduleDerivativeScalar",
      "SALD.forwardKlTimeChangeSquareCoefficientRewriteOfProductScalar",
      "SALD.forwardKlVelocitySquareScalingScalar",
      "SALD.forwardKlTimeChangedDerivativeBoundOfProductScalar",
      "SALD.forwardKlPreDvDerivativeBoundScalar",
      "SALD.forwardKlPreDvDerivativeBoundOfProductScalar",
      "SALD.forwardKlPreDvDerivativeBoundOfVelocityScalingScalar",
      "sald.forward_kl.endpoint_schedule_identities",
      "sald.forward_kl.moving_target_dependency_chain",
      "sald.forward_kl.density_boundary_regular",
    "sald.forward_kl.schedule_time_change",
    "sald.forward_kl.kl_derivative",
    "probability.lsi_to_kl_fi",
    "sald.forward_kl.cycle26_dv_witness_middle",
    "sald.forward_kl.dv_finite_log_mgf_witness",
    "sald.forward_kl.dv_energy_bound",
    "sald.forward_kl.coefficient_chain_audit",
    "sald.forward_kl.gronwall_application",
    "sald.forward_kl.gronwall_side_conditions"
  ]
  note := "This is a workflow obligation for middle-role synchronization. Cycle 14 selected endpoint schedule identities, cycles 18 and 22 selected Gronwall side-condition refinements, cycle 26 selects and maps the DV finite-log-mgf witness, cycle 30 returns to the derivative-side density/boundary and slowed-target transport interface, cycle 34 adds scalar post-Young/LSI/time-change handoffs, and cycle 39 adds source-shaped scalar schedule/velocity lemmas for appendix.tex:191-228; DV, LSI, Gronwall, schedule calculus, and KL derivative facts remain unformalized."

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