AutoSamplingTheory.SALD.cycle90DiscreteForwardKlMassConservationUpperPacket

Data definition / provenance and workflow record

Meaning and type

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

def cycle90DiscreteForwardKlMassConservationUpperPacket :
    DiscreteForwardKlUpperPacket

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.

objective : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

Global phase judgment: cycle 89 passed reviewer/build and needs no recovery; Phase 1 theorem-skeleton translation is stable enough for cited-theory backfill; the active EM backend still targets sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387, but the reviewer identified a theorem-route blocker after the pressure test. The single lower packet that now reduces the largest proof risk is the mass-conservation sub-boundary hmass : massTerm = 0 inside SALD.discreteForwardKlDerivativeObligation / sald.discrete_forward_kl.kl_derivative, sourced at eq:KL-derivative-0-discrete and appendix.tex:338-388, before the remaining hfirst and htarget IBP/FI identities.

sourceLabels : List String (explicit)

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

Ordered data items

1. thm:forward-KL-discrete
2. proof:thm:forward-KL-discrete
3. proof:thm:forward-KL-discrete:derivative
4. eq:KL-derivative-0-discrete
5. eq:KL-derivative-1-discrete
6. eq:KL-derivative-2-discrete
7. eq:general_KL_derivative_0_discrete
8. SALD.discreteForwardKlDerivativeObligation
9. SALD.discreteForwardKlDerivativeSplitOfRawIbpsScalar
10. SALD.discreteForwardKlPostLsiDerivativeBoundOfRawIbpsScalar
11. sald.discrete_forward_kl.kl_derivative
12. sald.general_moving_target_discrete.em_interpolation_fp

modeDiscipline : List String (explicit)

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

Ordered data items

1. faithfulPaper Phase 1 only: keep main_body.tex:299-323, appendix.tex:260-592, and sald_version_2.tex exclusion fixed.
2. Active-backend check: the shared EM packet remains sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387; cycle 90 leaves it only because the cycle-89 reviewer identified hmass/hfirst/htarget as the next theorem-route blocker.
3. Do not add assumptions to thm:forward-KL-discrete or replace the paper derivative route. The selected work is the source statement since integral partial_s hat rho_s dx = 0 in eq:KL-derivative-0-discrete.
4. Use Mathlib probability-measure, Measure.map, and derivative-under-integral APIs as local candidates; lean-stat-learning-theory remains a style reference only and is not imported.

nonGoals : List String (explicit)

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

Ordered data items

1. Do not mark thm:forward-KL-discrete, sald.discrete_forward_kl.kl_derivative, the EM interpolation backend, LSI, DV, or Gronwall formalized.
2. Do not start the broader hfirst divergence IBP/FI identity or htarget target-transport IBP unless the mass-conservation theorem is discharged or precisely blocked.
3. Do not spend this cycle on a broad LSI/DV/Gronwall fallback; no named active-EM Mathlib blocker requires that fallback after the cycle-89 reviewer route.
4. Do not add a wrapper that merely renames hmass. Either remove the supplied hmass hypothesis from a local route or name the smaller missing theorem with imports and hypotheses.

lowerPacket : List String (explicit)

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

Ordered data items

1. Classification target: discharges-supplied-hypothesis if lower compiles a local theorem proving the mass term is zero and consumes it in the cycle-89 raw derivative route; otherwise narrows-source-cited-boundary with one exact missing theorem. Wrapper-only output is rejected-wrapper-churn.
2. Lower should target exactly hmass : massTerm = 0 in SALD.discreteForwardKlDerivativeSplitOfRawIbpsScalar / SALD.discreteForwardKlPostLsiDerivativeBoundOfRawIbpsScalar and the source line since int partial_s hat rho_s dx = 0 in eq:KL-derivative-0-discrete.
3. The intended theorem boundary is: from hat rho_s = Law(hat X_s), probability mass one for each s, differentiability of the density/law pairing, and admissible constant test 1, prove integral partial_s hat rho_s dx = 0 without changing signs or constants.
4. If Mathlib blocks the proof, middle/lower must name the exact missing API, for example derivative of total mass for a differentiable family of probability laws, differentiation under an integral for the constant weak test, or density-to-measure mass preservation.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. Check that the packet records all three upper decisions: no cycle-89 recovery, Phase 1 stable, and hmass mass conservation is the single lower packet after the reviewed pressure test.
2. Check the explicit active-backend exception: sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387 remains active, but reviewer identified the theorem-route blocker hmass/hfirst/htarget.
3. Reject any LSI, DV, Gronwall, display algebra, accumulated-error, or broad theorem-route work unless the mass-conservation boundary is first discharged or exactly blocked.
4. Reject a supplied-hypothesis wrapper unless it removes the older hmass input or exposes a strictly smaller missing theorem with source, imports, and hypotheses.
5. No source constants, theorem statements, statuses, SLT imports, Lake dependencies, or source labels may change; source-index and ASTIS check must pass.

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 cycle90DiscreteForwardKlMassConservationUpperPacket :
    DiscreteForwardKlUpperPacket where
  objective := "Global phase judgment: cycle 89 passed reviewer/build and needs no recovery; Phase 1 theorem-skeleton translation is stable enough for cited-theory backfill; the active EM backend still targets sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387, but the reviewer identified a theorem-route blocker after the pressure test. The single lower packet that now reduces the largest proof risk is the mass-conservation sub-boundary hmass : massTerm = 0 inside SALD.discreteForwardKlDerivativeObligation / sald.discrete_forward_kl.kl_derivative, sourced at eq:KL-derivative-0-discrete and appendix.tex:338-388, before the remaining hfirst and htarget IBP/FI identities."
  sourceLabels := [
    "thm:forward-KL-discrete",
    "proof:thm:forward-KL-discrete",
    "proof:thm:forward-KL-discrete:derivative",
    "eq:KL-derivative-0-discrete",
    "eq:KL-derivative-1-discrete",
    "eq:KL-derivative-2-discrete",
    "eq:general_KL_derivative_0_discrete",
    "SALD.discreteForwardKlDerivativeObligation",
    "SALD.discreteForwardKlDerivativeSplitOfRawIbpsScalar",
    "SALD.discreteForwardKlPostLsiDerivativeBoundOfRawIbpsScalar",
    "sald.discrete_forward_kl.kl_derivative",
    "sald.general_moving_target_discrete.em_interpolation_fp"
  ]
  modeDiscipline := [
    "faithfulPaper Phase 1 only: keep main_body.tex:299-323, appendix.tex:260-592, and sald_version_2.tex exclusion fixed.",
    "Active-backend check: the shared EM packet remains sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387; cycle 90 leaves it only because the cycle-89 reviewer identified hmass/hfirst/htarget as the next theorem-route blocker.",
    "Do not add assumptions to thm:forward-KL-discrete or replace the paper derivative route.  The selected work is the source statement since integral partial_s hat rho_s dx = 0 in eq:KL-derivative-0-discrete.",
    "Use Mathlib probability-measure, Measure.map, and derivative-under-integral APIs as local candidates; lean-stat-learning-theory remains a style reference only and is not imported."
  ]
  nonGoals := [
    "Do not mark thm:forward-KL-discrete, sald.discrete_forward_kl.kl_derivative, the EM interpolation backend, LSI, DV, or Gronwall formalized.",
    "Do not start the broader hfirst divergence IBP/FI identity or htarget target-transport IBP unless the mass-conservation theorem is discharged or precisely blocked.",
    "Do not spend this cycle on a broad LSI/DV/Gronwall fallback; no named active-EM Mathlib blocker requires that fallback after the cycle-89 reviewer route.",
    "Do not add a wrapper that merely renames hmass.  Either remove the supplied hmass hypothesis from a local route or name the smaller missing theorem with imports and hypotheses."
  ]
  lowerPacket := [
    "Classification target: discharges-supplied-hypothesis if lower compiles a local theorem proving the mass term is zero and consumes it in the cycle-89 raw derivative route; otherwise narrows-source-cited-boundary with one exact missing theorem.  Wrapper-only output is rejected-wrapper-churn.",
    "Lower should target exactly hmass : massTerm = 0 in SALD.discreteForwardKlDerivativeSplitOfRawIbpsScalar / SALD.discreteForwardKlPostLsiDerivativeBoundOfRawIbpsScalar and the source line since int partial_s hat rho_s dx = 0 in eq:KL-derivative-0-discrete.",
    "The intended theorem boundary is: from hat rho_s = Law(hat X_s), probability mass one for each s, differentiability of the density/law pairing, and admissible constant test 1, prove integral partial_s hat rho_s dx = 0 without changing signs or constants.",
    "If Mathlib blocks the proof, middle/lower must name the exact missing API, for example derivative of total mass for a differentiable family of probability laws, differentiation under an integral for the constant weak test, or density-to-measure mass preservation."
  ]
  reviewerChecklist := [
    "Check that the packet records all three upper decisions: no cycle-89 recovery, Phase 1 stable, and hmass mass conservation is the single lower packet after the reviewed pressure test.",
    "Check the explicit active-backend exception: sald.general_moving_target_discrete.em_interpolation_fp over appendix.tex:1358-1387 remains active, but reviewer identified the theorem-route blocker hmass/hfirst/htarget.",
    "Reject any LSI, DV, Gronwall, display algebra, accumulated-error, or broad theorem-route work unless the mass-conservation boundary is first discharged or exactly blocked.",
    "Reject a supplied-hypothesis wrapper unless it removes the older hmass input or exposes a strictly smaller missing theorem with source, imports, and hypotheses.",
    "No source constants, theorem statements, statuses, SLT imports, Lake dependencies, or source labels may change; source-index and ASTIS check must pass."
  ]
  status := ProofStatus.obligation

/-- Cycle-90 obligation selecting the mass-conservation lower boundary. -/