AutoSamplingTheory.SALD.cycle85GeneralMovingTargetDiscreteConditionalKernelBoundaryUpperPacket

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 cycle85GeneralMovingTargetDiscreteConditionalKernelBoundaryUpperPacket :
    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.saldGeneralMovingTargetDiscreteConditionalDriftSource — 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.

Global phase judgment: cycle 84 passed reviewer/build and needs no recovery; Phase 1 theorem-skeleton translation is stable enough for cited-theory backfill; the single lower packet that now reduces the largest proof risk is the conditional-kernel/conditional-expectation theorem boundary inside sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387, specifically appendix.tex:1368-1377. Lower must either discharge one supplied conditional-law hypothesis using Mathlib-style ingredients, or record one exact missing condDistrib/condExpKernel theorem with imports and hypotheses.

sourceLabels : List String (explicit)

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

Ordered data items

1. proof:thm:general-moving-target-SALD-discrete:conditional-drift
2. proof:thm:general-moving-target-SALD-discrete:weak-conditional-fp
3. sald.general_moving_target_discrete.em_interpolation_fp
4. sald.general_moving_target_discrete.cycle85_conditional_kernel_boundary_upper
5. Mathlib.Probability.Kernel.CondDistrib
6. Mathlib.Probability.Kernel.Condexp
7. ProbabilityTheory.condExpKernel
8. thm:forward-KL-discrete
9. 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. The active lower packet still targets sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387; reviewer found no theorem-route blocker and no source-index defect requiring rebaseline.
2. Cycle 84 accepted a compiled endpoint/log-action wrapper but left the real analytic boundary unchanged: instantiate the conditional kernel for X_k^eta | hat X_s=x, name hat rho_s=Law(hat X_s), produce component conditional-integral fields, and prove measurability/integrability of bar b_{k,s}.
3. Cycle 85 lower classification is discharges-supplied-hypothesis if it proves a local theorem that removes an existing supplied conditional-kernel, marginal, conditional-integral, measurability, or integrability hypothesis.
4. Cycle 85 lower classification is narrows-source-cited-boundary if proof is blocked but the packet records one exact missing theorem, import list, and hypotheses for condDistrib/condExpKernel orientation or vector-valued conditional expectation.
5. Any new wrapper that only repackages existing supplied hypotheses without removing one or naming a smaller missing theorem is rejected-wrapper-churn.

theoremRoute : List String (explicit)

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

Ordered data items

1. 1. Stay inside appendix.tex:1368-1377 as the active sub-slice of appendix.tex:1358-1387.
2. 2. Align Mathlib's conditional-kernel orientation with the paper's conditioning X_k^eta | hat X_s=x; the named marginal consumed by the kernel must be hat rho_s=Law(hat X_s).
3. 3. Connect the conditional kernel to the two component conditional-integral fields for dot t_k*c_{t_k}(X_k^eta) and (sigma_eta^2/2)*nabla log pi_{t_k}(X_k^eta).
4. 4. Reduce the supplied hypotheses behind SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfComponents, SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfSwappedComponents, or SALD.generalMovingTargetDiscreteEndpointConditionalDriftRegularityHandoff.
5. 5. Keep weak FP source signs, KL/log-ratio substitution, density/AC, integration by parts, FI, LSI/KL/FI, DV, Gronwall, and theorem closure as downstream consumers.

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper Phase 1 only: preserve appendix.tex:1368-1377, the paper's bar b_{k,s} definition, the EM backend source labels, and both discrete theorem statements.
2. Do not add new assumptions to thm:forward-KL-discrete or thm:general-moving-target-SALD-discrete; any standard-Borel, probability, integrability, measurability, or finite-measure hypotheses belong only inside the local backend theorem boundary.
3. Use lean-stat-learning-theory only as a local proof-engineering reference for Mathlib measure/probability patterns; do not import it, change Lake dependencies, or mark any SLT theorem formalized.

nonGoals : List String (explicit)

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

Ordered data items

1. No theorem-route audit, broad source-index rebaseline, display algebra, Gronwall/DV/LSI/frozen-delta work, generator-to-law weak-FP work, KL/log-ratio work, reusable API redesign, or project-article export.
2. No new supplied-hypothesis wrapper unless it removes an older supplied hypothesis, exposes a strictly smaller missing theorem, or compiles a genuinely local proof.
3. No status promotion for sald.general_moving_target_discrete.em_interpolation_fp, sald.discrete_forward_kl.em_interpolation_fp, either discrete theorem contract, SLT reuse, or Lake dependencies.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387, narrowed to the conditional-kernel theorem boundary at appendix.tex:1368-1377.
2. Preferred product: a compiled local theorem from Mathlib-style ingredients that discharges one supplied hypothesis behind conditional-kernel compatibility, hat rho_s marginal orientation, component conditional-integral fields, or measurability/integrability of bar b_{k,s}.
3. Allowed blocked product: one precise source-cited missing theorem naming the Mathlib imports, theorem shape, and hypotheses for condDistrib/condExpKernel orientation or vector-valued conditional expectation.
4. Classification required in the lower handoff: discharges-supplied-hypothesis, narrows-source-cited-boundary, or rejected-wrapper-churn.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. The active packet still targets sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387 and the sub-slice appendix.tex:1368-1377.
2. Reject any packet classified as a wrapper unless it removes an existing supplied hypothesis or names a smaller missing theorem with imports and hypotheses.
3. The named marginal is hat rho_s=Law(hat X_s), and the conditional kernel orientation is explicitly reconciled with X_k^eta | hat X_s=x.
4. The lower result is classified as discharges-supplied-hypothesis or narrows-source-cited-boundary; rejected-wrapper-churn is not accepted as progress.
5. No theorem status, EM backend status, SLT status, or Lake dependency is promoted; no source sign or constant is changed.
6. 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.cycle84GeneralMovingTargetDiscreteActiveEmBackendLowerObligation
2. SALD.cycle80GeneralMovingTargetDiscreteConditionalLawMeasurabilityMiddleObligation
3. SALD.cycle80GeneralMovingTargetDiscreteConditionalLawMeasurabilityLowerObligation
4. SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillMiddleObligation
5. SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillLowerObligation
6. SALD.cycle74GeneralMovingTargetDiscreteConditionalKernelMeasureInterface
7. SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract
8. SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract
9. SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfComponents
10. SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfSwappedComponents
11. SALD.generalMovingTargetDiscreteEndpointConditionalDriftRegularityHandoff
12. Mathlib.Probability.Kernel.Condexp
13. Mathlib.Probability.Kernel.CondDistrib
14. sald.general_moving_target_discrete.em_interpolation_fp
15. sald.discrete_forward_kl.em_interpolation_fp

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 cycle85GeneralMovingTargetDiscreteConditionalKernelBoundaryUpperPacket :
    MainSkeletonAnalyticInterfaceLedger where
  sourceBlock := saldGeneralMovingTargetDiscreteConditionalDriftSource
  objective := "Global phase judgment: cycle 84 passed reviewer/build and needs no recovery; Phase 1 theorem-skeleton translation is stable enough for cited-theory backfill; the single lower packet that now reduces the largest proof risk is the conditional-kernel/conditional-expectation theorem boundary inside sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387, specifically appendix.tex:1368-1377. Lower must either discharge one supplied conditional-law hypothesis using Mathlib-style ingredients, or record one exact missing condDistrib/condExpKernel theorem with imports and hypotheses."
  sourceLabels := [
    "proof:thm:general-moving-target-SALD-discrete:conditional-drift",
    "proof:thm:general-moving-target-SALD-discrete:weak-conditional-fp",
    "sald.general_moving_target_discrete.em_interpolation_fp",
    "sald.general_moving_target_discrete.cycle85_conditional_kernel_boundary_upper",
    "Mathlib.Probability.Kernel.CondDistrib",
    "Mathlib.Probability.Kernel.Condexp",
    "ProbabilityTheory.condExpKernel",
    "thm:forward-KL-discrete",
    "thm:general-moving-target-SALD-discrete"
  ]
  analyticInterfaces := [
    "The active lower packet still targets sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387; reviewer found no theorem-route blocker and no source-index defect requiring rebaseline.",
    "Cycle 84 accepted a compiled endpoint/log-action wrapper but left the real analytic boundary unchanged: instantiate the conditional kernel for X_k^eta | hat X_s=x, name hat rho_s=Law(hat X_s), produce component conditional-integral fields, and prove measurability/integrability of bar b_{k,s}.",
    "Cycle 85 lower classification is discharges-supplied-hypothesis if it proves a local theorem that removes an existing supplied conditional-kernel, marginal, conditional-integral, measurability, or integrability hypothesis.",
    "Cycle 85 lower classification is narrows-source-cited-boundary if proof is blocked but the packet records one exact missing theorem, import list, and hypotheses for condDistrib/condExpKernel orientation or vector-valued conditional expectation.",
    "Any new wrapper that only repackages existing supplied hypotheses without removing one or naming a smaller missing theorem is rejected-wrapper-churn."
  ]
  theoremRoute := [
    "1. Stay inside appendix.tex:1368-1377 as the active sub-slice of appendix.tex:1358-1387.",
    "2. Align Mathlib's conditional-kernel orientation with the paper's conditioning X_k^eta | hat X_s=x; the named marginal consumed by the kernel must be hat rho_s=Law(hat X_s).",
    "3. Connect the conditional kernel to the two component conditional-integral fields for dot t_k*c_{t_k}(X_k^eta) and (sigma_eta^2/2)*nabla log pi_{t_k}(X_k^eta).",
    "4. Reduce the supplied hypotheses behind SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfComponents, SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfSwappedComponents, or SALD.generalMovingTargetDiscreteEndpointConditionalDriftRegularityHandoff.",
    "5. Keep weak FP source signs, KL/log-ratio substitution, density/AC, integration by parts, FI, LSI/KL/FI, DV, Gronwall, and theorem closure as downstream consumers."
  ]
  modeDiscipline := [
    "faithfulPaper Phase 1 only: preserve appendix.tex:1368-1377, the paper's bar b_{k,s} definition, the EM backend source labels, and both discrete theorem statements.",
    "Do not add new assumptions to thm:forward-KL-discrete or thm:general-moving-target-SALD-discrete; any standard-Borel, probability, integrability, measurability, or finite-measure hypotheses belong only inside the local backend theorem boundary.",
    "Use lean-stat-learning-theory only as a local proof-engineering reference for Mathlib measure/probability patterns; do not import it, change Lake dependencies, or mark any SLT theorem formalized."
  ]
  nonGoals := [
    "No theorem-route audit, broad source-index rebaseline, display algebra, Gronwall/DV/LSI/frozen-delta work, generator-to-law weak-FP work, KL/log-ratio work, reusable API redesign, or project-article export.",
    "No new supplied-hypothesis wrapper unless it removes an older supplied hypothesis, exposes a strictly smaller missing theorem, or compiles a genuinely local proof.",
    "No status promotion for sald.general_moving_target_discrete.em_interpolation_fp, sald.discrete_forward_kl.em_interpolation_fp, either discrete theorem contract, SLT reuse, or Lake dependencies."
  ]
  lowerPacket := [
    "Target exactly sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387, narrowed to the conditional-kernel theorem boundary at appendix.tex:1368-1377.",
    "Preferred product: a compiled local theorem from Mathlib-style ingredients that discharges one supplied hypothesis behind conditional-kernel compatibility, hat rho_s marginal orientation, component conditional-integral fields, or measurability/integrability of bar b_{k,s}.",
    "Allowed blocked product: one precise source-cited missing theorem naming the Mathlib imports, theorem shape, and hypotheses for condDistrib/condExpKernel orientation or vector-valued conditional expectation.",
    "Classification required in the lower handoff: discharges-supplied-hypothesis, narrows-source-cited-boundary, or rejected-wrapper-churn."
  ]
  reviewerChecklist := [
    "The active packet still targets sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387 and the sub-slice appendix.tex:1368-1377.",
    "Reject any packet classified as a wrapper unless it removes an existing supplied hypothesis or names a smaller missing theorem with imports and hypotheses.",
    "The named marginal is hat rho_s=Law(hat X_s), and the conditional kernel orientation is explicitly reconciled with X_k^eta | hat X_s=x.",
    "The lower result is classified as discharges-supplied-hypothesis or narrows-source-cited-boundary; rejected-wrapper-churn is not accepted as progress.",
    "No theorem status, EM backend status, SLT status, or Lake dependency is promoted; no source sign or constant is changed.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  dependencies := [
    "SALD.cycle84GeneralMovingTargetDiscreteActiveEmBackendLowerObligation",
    "SALD.cycle80GeneralMovingTargetDiscreteConditionalLawMeasurabilityMiddleObligation",
    "SALD.cycle80GeneralMovingTargetDiscreteConditionalLawMeasurabilityLowerObligation",
    "SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillMiddleObligation",
    "SALD.cycle75GeneralMovingTargetDiscreteConditionalLawBackfillLowerObligation",
    "SALD.cycle74GeneralMovingTargetDiscreteConditionalKernelMeasureInterface",
    "SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract",
    "SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract",
    "SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfComponents",
    "SALD.generalMovingTargetDiscreteConditionalKernelRegularityOfSwappedComponents",
    "SALD.generalMovingTargetDiscreteEndpointConditionalDriftRegularityHandoff",
    "Mathlib.Probability.Kernel.Condexp",
    "Mathlib.Probability.Kernel.CondDistrib",
    "sald.general_moving_target_discrete.em_interpolation_fp",
    "sald.discrete_forward_kl.em_interpolation_fp"
  ]
  status := ProofStatus.obligation

/-- Cycle-85 upper obligation selecting the conditional-kernel theorem
boundary instead of another supplied-hypothesis wrapper. -/