AutoSamplingTheory.SALD.cycle49MainSkeletonAnalyticMiddleContract

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 cycle49MainSkeletonAnalyticMiddleContract :
    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 middle: synchronize the post-route analytic readiness ledger with the conversion window, proof obligations, and theorem DAGs; verify that the five slow analytic interfaces are consumed by the six theorem skeletons in source order; and hand off appendix.tex:1354-1387 as the lower-ready 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. appendix.tex:47-79
2. main_body.tex:202-215
3. appendix.tex:168-252
4. appendix.tex:724-951
5. main_body.tex:359-395
6. appendix.tex:1313-1603
7. appendix.tex:1354-1387

analyticInterfaces : List String (explicit)

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

Ordered data items

1. Gronwall is source label lem:gronwall with endpoint-safe differentiability/FTC, interval-integrability, endpoint evaluation, and exponent-rewrite obligations in SALD.saldGronwallEndpointCalculusContract; theorem consumers are the continuous, discrete, continuous-general, and discrete-general Gronwall blocks.
2. DV is source label lem:dv_variation with same-space probability measures, nu << mu, finite KL/log-likelihood, selected-test measurability, finite log-mgf, and alpha-scaling witnesses exposed by dvVariationalFormulaInterface saldDvVariationSource and SALD.saldDvFiniteLogMgfContract; the Boucheron equality remains sourceCited.
3. LSI/KL/FI is source label eq:LSI-KL-FI with density rho << pi, Radon-Nikodym density, zero-set convention, admissible sqrt-density test or approximation, entropy identity, finite KL/FI, and Fisher chain rule exposed by SALD.saldLsiKlFiDensityTestContract.
4. Continuous Fokker--Planck/KL derivative is consumed by thm:forward-KL and thm:general-moving-target-SALD through SALD.forwardKlDerivativeSideConditionContract and SALD.generalMovingTargetDerivativeCandidateContract; density, boundary, integration-by-parts, and inverse-schedule backends stay obligations.
5. EM interpolation Fokker--Planck is consumed by thm:forward-KL-discrete and thm:general-moving-target-SALD-discrete through SALD.discreteForwardKlEmInterpolationSideConditionContract, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, the endpoint-law handoff, the named-interpolation endpoint helper, and the cycle-48 EM endpoint/conditional-law audit.

theoremRoute : List String (explicit)

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

Ordered data items

1. forward-KL: appendix.tex:168-252 routes derivative -> LSI -> DV velocity -> Gronwall; unchanged main_body.tex:240-247 statement remains contractOnly.
2. forward-KL-discrete: appendix.tex:260-592 routes EM conditional-FP -> frozen defect/LSI -> DV velocity -> Gronwall -> accumulated constants; unchanged main_body.tex:301-323 statement remains contractOnly.
3. guided residual: appendix.tex:619-704 routes normalizer derivative and centered residual identity; it remains contractOnly and feeds the unified transport bridge.
4. general moving-target: appendix.tex:724-951 routes continuous general Fokker--Planck/KL derivative -> LSI -> residual DV -> sigma-weighted Gronwall -> pure contraction.
5. unified forward-KL: main_body.tex:359-395 and appendix.tex:949-951 route only through the guided residual/correction-field transport bridge and the continuous general theorem specialization c_t <- u_t.
6. general moving-target discrete: appendix.tex:1313-1603 routes the general EM endpoint/conditional-FP backend -> frozen delta -> KL derivative/LSI -> residual DV -> Gronwall/stitching; appendix.tex:1354-1387 is the immediate lower slice.

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper Phase 1: use only original main_body.tex, appendix.tex, and iteration_complexity.tex; sald_version_2.tex remains excluded.
2. Keep every unproved backend below formalized status; compiled scalar or endpoint-law helpers are dependencies only.
3. Record endpoint, density, absolute-continuity, finite-KL/FI, finite-log-mgf, boundary, conditional-law, and stitched-interval facts as obligations rather than hidden theorem assumptions.
4. Do not start broad SLT or SDE library backfill until the theorem skeleton route and this middle audit remain green.

nonGoals : List String (explicit)

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

Ordered data items

1. Do not restate theorem displays, source constants, alpha ranges, slowdown assumptions, or source labels.
2. Do not replace the derivative -> LSI -> DV -> Gronwall route or the paper EM/frozen-delta route.
3. Do not add scalar-only sublemmas unless they directly discharge appendix.tex:1354-1387 endpoint or conditional-law obligations.
4. Do not mark the EM endpoint-law handoff as a Brownian construction, regular conditional drift, density, or weak Fokker--Planck proof.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.generalMovingTargetDiscreteDerivativeCandidateContract / SALD.generalMovingTargetDiscreteDerivativeObligation / sald.general_moving_target_discrete.kl_derivative.
2. First lower sub-slice: appendix.tex:1354-1387, with named-law representations for hat rho_s, rho_k^eta, and rho_{k+1}^eta; endpoint-law equalities; common-space and absolute-continuity assumptions for hat rho_s and tilde pi_s; regular conditional drift bar b_{k,s}; and the weak conditional Fokker--Planck equation.
3. Use SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation only after the concrete named-process law representations and pointwise endpoint identities are supplied; it is not the stochastic construction or conditional-FP proof.
4. Keep appendix.tex:1469-1511 frozen/residual algebra and the two sigma_eta^2/8 Young shares as the next sub-slice after the endpoint/conditional-law interface is stable.
5. Local SLT material may guide disintegration or one-step patterns as reference only; do not import or promote SLT results.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD.cycle49MainSkeletonAnalyticMiddleObligation is listed by all six theorem contracts and the cycle-49 DAG pane.
2. The conversion window and proof-obligation ledger contain the cycle-49 middle route audit and the appendix.tex:1354-1387 lower packet.
3. The five analytic backends remain sourceCited or obligation-level, with no theorem proofStatus promoted.
4. No source theorem statement, coefficient, source label, theorem route, or external reuse status 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.cycle49MainSkeletonAnalyticReadinessLedger
2. SALD.cycle49MainSkeletonAnalyticReadinessObligation
3. SALD.cycle44MainSkeletonAnalyticInterfaceObligation
4. SALD.cycle45ForwardKlSkeletonMiddleObligation
5. SALD.cycle46DiscreteForwardKlSkeletonMiddleObligation
6. SALD.cycle47GuidedGeneralSkeletonMiddleObligation
7. SALD.cycle48UnifiedDiscreteSkeletonMiddleObligation
8. SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation
9. SALD.generalMovingTargetDiscreteEmEndpointLawPairHandoff
10. SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation
11. sald.general_moving_target_discrete.em_interpolation_fp
12. sald.general_moving_target_discrete.kl_derivative

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 cycle49MainSkeletonAnalyticMiddleContract :
    MainSkeletonAnalyticInterfaceLedger where
  sourceBlock := saldGeneralMovingTargetDiscreteDerivativeSource
  objective := "Cycle 49 middle: synchronize the post-route analytic readiness ledger with the conversion window, proof obligations, and theorem DAGs; verify that the five slow analytic interfaces are consumed by the six theorem skeletons in source order; and hand off appendix.tex:1354-1387 as the lower-ready EM endpoint/conditional-law/Fokker--Planck slice."
  sourceLabels := [
    "appendix.tex:47-79",
    "main_body.tex:202-215",
    "appendix.tex:168-252",
    "appendix.tex:724-951",
    "main_body.tex:359-395",
    "appendix.tex:1313-1603",
    "appendix.tex:1354-1387"
  ]
  analyticInterfaces := [
    "Gronwall is source label lem:gronwall with endpoint-safe differentiability/FTC, interval-integrability, endpoint evaluation, and exponent-rewrite obligations in SALD.saldGronwallEndpointCalculusContract; theorem consumers are the continuous, discrete, continuous-general, and discrete-general Gronwall blocks.",
    "DV is source label lem:dv_variation with same-space probability measures, nu << mu, finite KL/log-likelihood, selected-test measurability, finite log-mgf, and alpha-scaling witnesses exposed by dvVariationalFormulaInterface saldDvVariationSource and SALD.saldDvFiniteLogMgfContract; the Boucheron equality remains sourceCited.",
    "LSI/KL/FI is source label eq:LSI-KL-FI with density rho << pi, Radon-Nikodym density, zero-set convention, admissible sqrt-density test or approximation, entropy identity, finite KL/FI, and Fisher chain rule exposed by SALD.saldLsiKlFiDensityTestContract.",
    "Continuous Fokker--Planck/KL derivative is consumed by thm:forward-KL and thm:general-moving-target-SALD through SALD.forwardKlDerivativeSideConditionContract and SALD.generalMovingTargetDerivativeCandidateContract; density, boundary, integration-by-parts, and inverse-schedule backends stay obligations.",
    "EM interpolation Fokker--Planck is consumed by thm:forward-KL-discrete and thm:general-moving-target-SALD-discrete through SALD.discreteForwardKlEmInterpolationSideConditionContract, SALD.generalMovingTargetDiscreteDerivativeSideConditionContract, the endpoint-law handoff, the named-interpolation endpoint helper, and the cycle-48 EM endpoint/conditional-law audit."
  ]
  theoremRoute := [
    "forward-KL: appendix.tex:168-252 routes derivative -> LSI -> DV velocity -> Gronwall; unchanged main_body.tex:240-247 statement remains contractOnly.",
    "forward-KL-discrete: appendix.tex:260-592 routes EM conditional-FP -> frozen defect/LSI -> DV velocity -> Gronwall -> accumulated constants; unchanged main_body.tex:301-323 statement remains contractOnly.",
    "guided residual: appendix.tex:619-704 routes normalizer derivative and centered residual identity; it remains contractOnly and feeds the unified transport bridge.",
    "general moving-target: appendix.tex:724-951 routes continuous general Fokker--Planck/KL derivative -> LSI -> residual DV -> sigma-weighted Gronwall -> pure contraction.",
    "unified forward-KL: main_body.tex:359-395 and appendix.tex:949-951 route only through the guided residual/correction-field transport bridge and the continuous general theorem specialization c_t <- u_t.",
    "general moving-target discrete: appendix.tex:1313-1603 routes the general EM endpoint/conditional-FP backend -> frozen delta -> KL derivative/LSI -> residual DV -> Gronwall/stitching; appendix.tex:1354-1387 is the immediate lower slice."
  ]
  modeDiscipline := [
    "faithfulPaper Phase 1: use only original main_body.tex, appendix.tex, and iteration_complexity.tex; sald_version_2.tex remains excluded.",
    "Keep every unproved backend below formalized status; compiled scalar or endpoint-law helpers are dependencies only.",
    "Record endpoint, density, absolute-continuity, finite-KL/FI, finite-log-mgf, boundary, conditional-law, and stitched-interval facts as obligations rather than hidden theorem assumptions.",
    "Do not start broad SLT or SDE library backfill until the theorem skeleton route and this middle audit remain green."
  ]
  nonGoals := [
    "Do not restate theorem displays, source constants, alpha ranges, slowdown assumptions, or source labels.",
    "Do not replace the derivative -> LSI -> DV -> Gronwall route or the paper EM/frozen-delta route.",
    "Do not add scalar-only sublemmas unless they directly discharge appendix.tex:1354-1387 endpoint or conditional-law obligations.",
    "Do not mark the EM endpoint-law handoff as a Brownian construction, regular conditional drift, density, or weak Fokker--Planck proof."
  ]
  lowerPacket := [
    "Target exactly SALD.generalMovingTargetDiscreteDerivativeCandidateContract / SALD.generalMovingTargetDiscreteDerivativeObligation / sald.general_moving_target_discrete.kl_derivative.",
    "First lower sub-slice: appendix.tex:1354-1387, with named-law representations for hat rho_s, rho_k^eta, and rho_{k+1}^eta; endpoint-law equalities; common-space and absolute-continuity assumptions for hat rho_s and tilde pi_s; regular conditional drift bar b_{k,s}; and the weak conditional Fokker--Planck equation.",
    "Use SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation only after the concrete named-process law representations and pointwise endpoint identities are supplied; it is not the stochastic construction or conditional-FP proof.",
    "Keep appendix.tex:1469-1511 frozen/residual algebra and the two sigma_eta^2/8 Young shares as the next sub-slice after the endpoint/conditional-law interface is stable.",
    "Local SLT material may guide disintegration or one-step patterns as reference only; do not import or promote SLT results."
  ]
  reviewerChecklist := [
    "SALD.cycle49MainSkeletonAnalyticMiddleObligation is listed by all six theorem contracts and the cycle-49 DAG pane.",
    "The conversion window and proof-obligation ledger contain the cycle-49 middle route audit and the appendix.tex:1354-1387 lower packet.",
    "The five analytic backends remain sourceCited or obligation-level, with no theorem proofStatus promoted.",
    "No source theorem statement, coefficient, source label, theorem route, or external reuse status is changed.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  dependencies := [
    "SALD.cycle49MainSkeletonAnalyticReadinessLedger",
    "SALD.cycle49MainSkeletonAnalyticReadinessObligation",
    "SALD.cycle44MainSkeletonAnalyticInterfaceObligation",
    "SALD.cycle45ForwardKlSkeletonMiddleObligation",
    "SALD.cycle46DiscreteForwardKlSkeletonMiddleObligation",
    "SALD.cycle47GuidedGeneralSkeletonMiddleObligation",
    "SALD.cycle48UnifiedDiscreteSkeletonMiddleObligation",
    "SALD.cycle48GeneralMovingTargetDiscreteEmEndpointFpAuditObligation",
    "SALD.generalMovingTargetDiscreteEmEndpointLawPairHandoff",
    "SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation",
    "sald.general_moving_target_discrete.em_interpolation_fp",
    "sald.general_moving_target_discrete.kl_derivative"
  ]
  status := ProofStatus.obligation

/-- Cycle-49 middle obligation tying the analytic-readiness audit to lower
work and the Markdown conversion window. -/