AutoSamplingTheory.SALD.cycle49MainSkeletonAnalyticReadinessLedger

Data definition / provenance and workflow record

Meaning and type

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

def cycle49MainSkeletonAnalyticReadinessLedger :
    MainSkeletonAnalyticInterfaceLedger

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.saldGeneralMovingTargetDiscreteDerivativeSource — 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.

Cycle 49 upper: re-check the five slow analytic backends after the theorem skeleton route is wired, record the exact source-cited interface expected from each backend, and assign the next lower packet to the discrete general EM endpoint/conditional-law Fokker--Planck slice.

sourceLabels : List String (explicit)

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

Ordered data items

1. lem:gronwall
2. lem:dv_variation
3. eq:LSI-KL-FI
4. proof:thm:forward-KL:derivative
5. proof:thm:general-moving-target-SALD-discrete:em-fp
6. thm:forward-KL
7. thm:forward-KL-discrete
8. prop:guided_path_residual
9. thm:general-moving-target-SALD
10. thm:unified-forward-KL
11. thm:general-moving-target-SALD-discrete

analyticInterfaces : List String (explicit)

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

Ordered data items

1. Gronwall backend: SALD.saldGronwallCandidateContract and SALD.saldGronwallEndpointCalculusContract now name the closed-interval derivative semantics, FTC/order-integration requirement, endpoint evaluation, interval-integrability, and exponent-rewrite handoffs; the full source lemma remains ProofStatus.obligation.
2. DV backend: dvVariationalFormulaInterface saldDvVariationSource and SALD.saldDvFiniteLogMgfContract name common measurable space, nu << mu, finite KL/log-likelihood, selected-test measurability, finite log-mgf, and the one-sided selected-test consequence; the Boucheron equality remains ProofStatus.sourceCited.
3. LSI/KL/FI backend: SALD.saldLsiKlFiDensityTestContract names rho << pi, Radon-Nikodym density r, zero-density convention, sqrt(r) test admissibility or approximation, entropy identity, finite KL/FI, and Fisher chain rule; probability.lsi_to_kl_fi remains ProofStatus.obligation.
4. Continuous Fokker--Planck/KL derivative backend: SALD.forwardKlDerivativeCandidateContract, SALD.forwardKlDerivativeSideConditionContract, and SALD.generalMovingTargetDerivativeCandidateContract name law/density regularity, mass conservation, KL differentiation under the integral, SALD/general Fokker--Planck equations, integration by parts, target transport, LSI handoff, and inverse-schedule calculus; the KL derivative blocks remain ProofStatus.obligation.
5. EM interpolation Fokker--Planck backend: SALD.discreteForwardKlEmInterpolationSideConditionContract, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, SALD.generalMovingTargetDiscreteEmEndpointLawPairHandoff, SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation, and SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation name endpoint laws, regular conditional drift, conditional-law density/absolute-continuity, weak conditional Fokker--Planck, Laplacian split, stitched intervals, and common-space assumptions; the analytic backend remains ProofStatus.obligation.

theoremRoute : List String (explicit)

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

Ordered data items

1. 1. thm:forward-KL is already routed through the continuous KL derivative, LSI/KL/FI, DV velocity witness, Gronwall, and endpoint schedule obligations.
2. 2. thm:forward-KL-discrete is already routed through EM endpoint/conditional-FP, discrete KL derivative, frozen-delta/LSI, DV velocity, Gronwall accumulation, and accumulated-error obligations.
3. 3. prop:guided_path_residual is already routed through the normalizer derivative and residual identity obligations; it remains contractOnly and feeds only the unified specialization.
4. 4. thm:general-moving-target-SALD is already routed through the continuous general KL derivative, residual DV, sigma-weighted Gronwall, and pure-contraction obligations.
5. 5. thm:unified-forward-KL is already routed as a specialization of thm:general-moving-target-SALD via prop:guided_path_residual, eq:poisson-eq, and the transport bridge.
6. 6. thm:general-moving-target-SALD-discrete is the next lower target: appendix.tex:1354-1387 now has a compiled named-interpolation endpoint-law handoff, while conditional-law density and weak conditional-Fokker--Planck remain obligations before frozen/residual algebra or Gronwall display work continues.

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper Phase 1 only: preserve the original source statements and constants from main_body.tex and appendix.tex, with sald_version_2.tex excluded.
2. Do not add endpoint, density, absolute-continuity, finite-log-mgf, smoothness, boundary, or stitched-interval assumptions to theorem statements; record them in obligations.
3. Do not promote Gronwall, DV, LSI/KL/FI, continuous KL derivative, or EM interpolation Fokker--Planck beyond obligation/sourceCited until a local proof or imported theorem builds.
4. Keep theorem-level skeleton closure ahead of broad SLT/measure-theory backfill.

nonGoals : List String (explicit)

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

Ordered data items

1. No source-index rebaseline beyond the required acceptance command.
2. No new scalar-only lemma unless it directly discharges the selected EM endpoint/conditional-law backend.
3. No SLT import or formalized reuse claim for entropy duality, LSI, concentration, or one-step EM analysis in this packet.
4. No alternate proof route replacing derivative -> LSI -> DV -> Gronwall or the paper EM/frozen-delta path.

lowerPacket : List String (explicit)

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

Ordered data items

1. Lower target: SALD.generalMovingTargetDiscreteDerivativeCandidateContract / SALD.generalMovingTargetDiscreteDerivativeObligation / sald.general_moving_target_discrete.kl_derivative.
2. First sub-slice: appendix.tex:1354-1387, especially endpoint laws for hat rho_s, named-law representations for rho_k^eta and rho_{k+1}^eta, regular conditional drift bar b_{k,s}, density/absolute-continuity, and weak conditional Fokker--Planck.
3. Use SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation for the named-process endpoint-law bookkeeping once pointwise interpolation identities and law representations are supplied; do not treat it as the Brownian/EM construction or conditional-FP proof.
4. Preserve the cycle-28 frozen/residual algebra and the two sigma_eta^2/8 Young shares for the next sub-slice after the EM interface is stable.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. All five analytic backends have named Lean-facing interfaces and statuses below formalized, except already compiled local algebra helpers.
2. The six theorem contracts include this cycle-49 readiness obligation while remaining contractOnly where appropriate.
3. The selected lower packet points to appendix.tex:1354-1387 and not to a source-index rebaseline or broad SLT backfill.
4. No source theorem statement, coefficient, source label, or theorem proofStatus is changed.
5. python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass.

dependencies : List String (explicit)

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

Ordered data items

1. SALD.cycle44MainSkeletonAnalyticInterfaceLedger
2. SALD.cycle45ForwardKlSkeletonObligation
3. SALD.cycle46DiscreteForwardKlSkeletonObligation
4. SALD.cycle47GuidedGeneralSkeletonObligation
5. SALD.cycle48UnifiedDiscreteSkeletonObligation
6. SALD.saldGronwallEndpointCalculusContract
7. dvVariationalFormulaInterface saldDvVariationSource
8. SALD.saldLsiKlFiDensityTestContract
9. SALD.forwardKlDerivativeCandidateContract
10. SALD.generalMovingTargetDerivativeCandidateContract
11. SALD.generalMovingTargetDiscreteDerivativeSideConditionContract
12. SALD.generalMovingTargetDiscreteEmEndpointLawPairHandoff
13. SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation
14. SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation

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 cycle49MainSkeletonAnalyticReadinessLedger :
    MainSkeletonAnalyticInterfaceLedger where
  sourceBlock := saldGeneralMovingTargetDiscreteDerivativeSource
  objective := "Cycle 49 upper: re-check the five slow analytic backends after the theorem skeleton route is wired, record the exact source-cited interface expected from each backend, and assign the next lower packet to the discrete general EM endpoint/conditional-law Fokker--Planck slice."
  sourceLabels := [
    "lem:gronwall",
    "lem:dv_variation",
    "eq:LSI-KL-FI",
    "proof:thm:forward-KL:derivative",
    "proof:thm:general-moving-target-SALD-discrete:em-fp",
    "thm:forward-KL",
    "thm:forward-KL-discrete",
    "prop:guided_path_residual",
    "thm:general-moving-target-SALD",
    "thm:unified-forward-KL",
    "thm:general-moving-target-SALD-discrete"
  ]
  analyticInterfaces := [
    "Gronwall backend: SALD.saldGronwallCandidateContract and SALD.saldGronwallEndpointCalculusContract now name the closed-interval derivative semantics, FTC/order-integration requirement, endpoint evaluation, interval-integrability, and exponent-rewrite handoffs; the full source lemma remains ProofStatus.obligation.",
    "DV backend: dvVariationalFormulaInterface saldDvVariationSource and SALD.saldDvFiniteLogMgfContract name common measurable space, nu << mu, finite KL/log-likelihood, selected-test measurability, finite log-mgf, and the one-sided selected-test consequence; the Boucheron equality remains ProofStatus.sourceCited.",
    "LSI/KL/FI backend: SALD.saldLsiKlFiDensityTestContract names rho << pi, Radon-Nikodym density r, zero-density convention, sqrt(r) test admissibility or approximation, entropy identity, finite KL/FI, and Fisher chain rule; probability.lsi_to_kl_fi remains ProofStatus.obligation.",
    "Continuous Fokker--Planck/KL derivative backend: SALD.forwardKlDerivativeCandidateContract, SALD.forwardKlDerivativeSideConditionContract, and SALD.generalMovingTargetDerivativeCandidateContract name law/density regularity, mass conservation, KL differentiation under the integral, SALD/general Fokker--Planck equations, integration by parts, target transport, LSI handoff, and inverse-schedule calculus; the KL derivative blocks remain ProofStatus.obligation.",
    "EM interpolation Fokker--Planck backend: SALD.discreteForwardKlEmInterpolationSideConditionContract, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, SALD.generalMovingTargetDiscreteEmEndpointLawPairHandoff, SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation, and SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation name endpoint laws, regular conditional drift, conditional-law density/absolute-continuity, weak conditional Fokker--Planck, Laplacian split, stitched intervals, and common-space assumptions; the analytic backend remains ProofStatus.obligation."
  ]
  theoremRoute := [
    "1. thm:forward-KL is already routed through the continuous KL derivative, LSI/KL/FI, DV velocity witness, Gronwall, and endpoint schedule obligations.",
    "2. thm:forward-KL-discrete is already routed through EM endpoint/conditional-FP, discrete KL derivative, frozen-delta/LSI, DV velocity, Gronwall accumulation, and accumulated-error obligations.",
    "3. prop:guided_path_residual is already routed through the normalizer derivative and residual identity obligations; it remains contractOnly and feeds only the unified specialization.",
    "4. thm:general-moving-target-SALD is already routed through the continuous general KL derivative, residual DV, sigma-weighted Gronwall, and pure-contraction obligations.",
    "5. thm:unified-forward-KL is already routed as a specialization of thm:general-moving-target-SALD via prop:guided_path_residual, eq:poisson-eq, and the transport bridge.",
    "6. thm:general-moving-target-SALD-discrete is the next lower target: appendix.tex:1354-1387 now has a compiled named-interpolation endpoint-law handoff, while conditional-law density and weak conditional-Fokker--Planck remain obligations before frozen/residual algebra or Gronwall display work continues."
  ]
  modeDiscipline := [
    "faithfulPaper Phase 1 only: preserve the original source statements and constants from main_body.tex and appendix.tex, with sald_version_2.tex excluded.",
    "Do not add endpoint, density, absolute-continuity, finite-log-mgf, smoothness, boundary, or stitched-interval assumptions to theorem statements; record them in obligations.",
    "Do not promote Gronwall, DV, LSI/KL/FI, continuous KL derivative, or EM interpolation Fokker--Planck beyond obligation/sourceCited until a local proof or imported theorem builds.",
    "Keep theorem-level skeleton closure ahead of broad SLT/measure-theory backfill."
  ]
  nonGoals := [
    "No source-index rebaseline beyond the required acceptance command.",
    "No new scalar-only lemma unless it directly discharges the selected EM endpoint/conditional-law backend.",
    "No SLT import or formalized reuse claim for entropy duality, LSI, concentration, or one-step EM analysis in this packet.",
    "No alternate proof route replacing derivative -> LSI -> DV -> Gronwall or the paper EM/frozen-delta path."
  ]
  lowerPacket := [
    "Lower target: SALD.generalMovingTargetDiscreteDerivativeCandidateContract / SALD.generalMovingTargetDiscreteDerivativeObligation / sald.general_moving_target_discrete.kl_derivative.",
    "First sub-slice: appendix.tex:1354-1387, especially endpoint laws for hat rho_s, named-law representations for rho_k^eta and rho_{k+1}^eta, regular conditional drift bar b_{k,s}, density/absolute-continuity, and weak conditional Fokker--Planck.",
    "Use SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation for the named-process endpoint-law bookkeeping once pointwise interpolation identities and law representations are supplied; do not treat it as the Brownian/EM construction or conditional-FP proof.",
    "Preserve the cycle-28 frozen/residual algebra and the two sigma_eta^2/8 Young shares for the next sub-slice after the EM interface is stable."
  ]
  reviewerChecklist := [
    "All five analytic backends have named Lean-facing interfaces and statuses below formalized, except already compiled local algebra helpers.",
    "The six theorem contracts include this cycle-49 readiness obligation while remaining contractOnly where appropriate.",
    "The selected lower packet points to appendix.tex:1354-1387 and not to a source-index rebaseline or broad SLT backfill.",
    "No source theorem statement, coefficient, source label, or theorem proofStatus is changed.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  dependencies := [
    "SALD.cycle44MainSkeletonAnalyticInterfaceLedger",
    "SALD.cycle45ForwardKlSkeletonObligation",
    "SALD.cycle46DiscreteForwardKlSkeletonObligation",
    "SALD.cycle47GuidedGeneralSkeletonObligation",
    "SALD.cycle48UnifiedDiscreteSkeletonObligation",
    "SALD.saldGronwallEndpointCalculusContract",
    "dvVariationalFormulaInterface saldDvVariationSource",
    "SALD.saldLsiKlFiDensityTestContract",
    "SALD.forwardKlDerivativeCandidateContract",
    "SALD.generalMovingTargetDerivativeCandidateContract",
    "SALD.generalMovingTargetDiscreteDerivativeSideConditionContract",
    "SALD.generalMovingTargetDiscreteEmEndpointLawPairHandoff",
    "SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation",
    "SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation"
  ]
  status := ProofStatus.obligation

/-- Cycle-49 upper obligation selecting the next theorem-level backend. -/