AutoSamplingTheory.SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract

Data definition / provenance and workflow record

Meaning and type

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

def generalMovingTargetDiscreteWeakConditionalFpSourceSignContract :
    GeneralMovingTargetDiscreteWeakConditionalFpSourceSignContract

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.saldGeneralMovingTargetDiscreteWeakFpSource — audited data reference, not expanded and not a compiled dependency edge

parentInterface : String (explicit)

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

sald.general_moving_target_discrete.em_interpolation_fp / appendix.tex:1358-1387

fixedInterval : String (explicit)

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

Fix k and s in [s_k,s_{k+1}] after hat rho_s=Law(hat X_s) and the endpoint-to-conditional marginal compatibility have been aligned.

namedLaw : String (explicit)

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

The weak equation is for the same named interpolation law hat rho_s that appears in partial_s hat rho_s and in the conditional-kernel marginal from cycle 71.

conditionalDrift : String (explicit)

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

The drift field is the cycle-70/71 selected bar b_{k,s}(x)=E[dot t_k*c_{t_k}(X_k^eta)+(sigma_eta^2/2)*nabla log pi_{t_k}(X_k^eta)|hat X_s=x], with measurability and integrability supplied explicitly.

weakTestClass : String (explicit)

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

Use a smooth compactly supported or otherwise admissible weak-test class for which partial_s hat rho_s, div(hat rho_s*bar b_{k,s}), and Delta hat rho_s are all meaningful distributions.

weakEquation : String (explicit)

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

For every admissible test phi, the supplied weak-FP identity must represent partial_s hat rho_s as -div(hat rho_s*bar b_{k,s}) plus (sigma_eta^2/2)*Delta hat rho_s; SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorHandoff splits that input into a supplied generator/time-derivative identity and a supplied generator source expansion, while SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorPiecesHandoff further splits the source expansion into drift and diffusion actions under explicit conditional-law, density, test, and boundary hypotheses. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff and SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff compile the test-indexed source-sign/coefficient packaging once the analytic identity is supplied, and SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSigns consumes the normalized source signs at the log-ratio test.

driftSignConvention : String (explicit)

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

The divergence term is negative exactly as in appendix.tex:1384: -nabla dot (hat rho_s bar b_{k,s}).

diffusionSignConvention : String (explicit)

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

The Laplacian term is positive exactly as in appendix.tex:1385-1386: +(sigma_eta^2/2) Delta hat rho_s.

explicitHypotheses : List String (explicit)

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

Ordered data items

1. common probability space and joint law of (X_k^eta,hat X_s)
2. regular conditional kernel compatible with the named hat rho_s marginal
3. bar b_{k,s} measurability and local integrability against hat rho_s
4. density/absolute-continuity and time regularity for hat rho_s on the fixed EM interval
5. admissible weak-test class with integration-by-parts and Laplacian dual actions
6. generator identity for the frozen EM interpolation on admissible tests
7. source expansion of that generator as -div(hat rho_s*bar b_{k,s}) plus sigmaCoeff*Delta hat rho_s
8. optional component split of the source expansion into separate drift and diffusion actions
9. diffusion coefficient identified with sigma_eta^2/2

downstreamHandoffs : List String (explicit)

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

Ordered data items

1. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorHandoff
2. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorPiecesHandoff
3. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff
4. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff
5. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract
6. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSigns
7. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns
8. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces
9. SALD.generalMovingTargetDiscreteConditionalFpSourceSignsHandoff
10. SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff
11. sald.general_moving_target_discrete.kl_derivative

exclusions : List String (explicit)

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

Ordered data items

1. Do not construct the Brownian/EM law or regular conditional kernel in this contract.
2. Do not prove density, absolute-continuity, or integration-by-parts side conditions here.
3. Do not prove the KL derivative, LSI/KL/FI, DV, Gronwall, or theorem closure.
4. Do not promote sald.general_moving_target_discrete.em_interpolation_fp above ProofStatus.obligation.

dependencies : List String (explicit)

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

Ordered data items

1. eq:general_moving_target_SALD_frozen_interp
2. SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract
3. SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract
4. SALD.generalMovingTargetDiscreteNamedConditionalDriftComponents
5. SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityOfComponents
6. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorHandoff
7. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorPiecesHandoff
8. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff
9. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff
10. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract
11. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffScalar
12. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSigns
13. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns
14. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces
15. SALD.generalMovingTargetDiscreteConditionalFpSourceSignsHandoff
16. SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff
17. sald.general_moving_target_discrete.em_interpolation_fp

sourceGaps : List String (explicit)

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

Ordered data items

1. appendix.tex:1379-1387 invokes the Fokker--Planck equation associated with the frozen interpolation but does not state the weak-test theorem or its regularity hypotheses.
2. The generator-level theorem that turns the frozen EM interpolation into the weak time derivative of hat rho_s is still supplied as an analytic hypothesis.
3. The source does not spell out the density, local integrability, or boundary/integration-by-parts assumptions required to interpret the divergence and Laplacian terms distributionally.
4. The source passes immediately from this FP equation to the Laplacian split and KL derivative handoff.

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 generalMovingTargetDiscreteWeakConditionalFpSourceSignContract :
    GeneralMovingTargetDiscreteWeakConditionalFpSourceSignContract where
  sourceBlock := saldGeneralMovingTargetDiscreteWeakFpSource
  parentInterface := "sald.general_moving_target_discrete.em_interpolation_fp / appendix.tex:1358-1387"
  fixedInterval := "Fix k and s in [s_k,s_{k+1}] after hat rho_s=Law(hat X_s) and the endpoint-to-conditional marginal compatibility have been aligned."
  namedLaw := "The weak equation is for the same named interpolation law hat rho_s that appears in partial_s hat rho_s and in the conditional-kernel marginal from cycle 71."
  conditionalDrift := "The drift field is the cycle-70/71 selected bar b_{k,s}(x)=E[dot t_k*c_{t_k}(X_k^eta)+(sigma_eta^2/2)*nabla log pi_{t_k}(X_k^eta)|hat X_s=x], with measurability and integrability supplied explicitly."
  weakTestClass := "Use a smooth compactly supported or otherwise admissible weak-test class for which partial_s hat rho_s, div(hat rho_s*bar b_{k,s}), and Delta hat rho_s are all meaningful distributions."
  weakEquation := "For every admissible test phi, the supplied weak-FP identity must represent partial_s hat rho_s as -div(hat rho_s*bar b_{k,s}) plus (sigma_eta^2/2)*Delta hat rho_s; SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorHandoff splits that input into a supplied generator/time-derivative identity and a supplied generator source expansion, while SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorPiecesHandoff further splits the source expansion into drift and diffusion actions under explicit conditional-law, density, test, and boundary hypotheses. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff and SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff compile the test-indexed source-sign/coefficient packaging once the analytic identity is supplied, and SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSigns consumes the normalized source signs at the log-ratio test."
  driftSignConvention := "The divergence term is negative exactly as in appendix.tex:1384: -nabla dot (hat rho_s bar b_{k,s})."
  diffusionSignConvention := "The Laplacian term is positive exactly as in appendix.tex:1385-1386: +(sigma_eta^2/2) Delta hat rho_s."
  explicitHypotheses := [
    "common probability space and joint law of (X_k^eta,hat X_s)",
    "regular conditional kernel compatible with the named hat rho_s marginal",
    "bar b_{k,s} measurability and local integrability against hat rho_s",
    "density/absolute-continuity and time regularity for hat rho_s on the fixed EM interval",
    "admissible weak-test class with integration-by-parts and Laplacian dual actions",
    "generator identity for the frozen EM interpolation on admissible tests",
    "source expansion of that generator as -div(hat rho_s*bar b_{k,s}) plus sigmaCoeff*Delta hat rho_s",
    "optional component split of the source expansion into separate drift and diffusion actions",
    "diffusion coefficient identified with sigma_eta^2/2"
  ]
  downstreamHandoffs := [
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorHandoff",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorPiecesHandoff",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSigns",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces",
    "SALD.generalMovingTargetDiscreteConditionalFpSourceSignsHandoff",
    "SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff",
    "sald.general_moving_target_discrete.kl_derivative"
  ]
  exclusions := [
    "Do not construct the Brownian/EM law or regular conditional kernel in this contract.",
    "Do not prove density, absolute-continuity, or integration-by-parts side conditions here.",
    "Do not prove the KL derivative, LSI/KL/FI, DV, Gronwall, or theorem closure.",
    "Do not promote sald.general_moving_target_discrete.em_interpolation_fp above ProofStatus.obligation."
  ]
  dependencies := [
    "eq:general_moving_target_SALD_frozen_interp",
    "SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract",
    "SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract",
    "SALD.generalMovingTargetDiscreteNamedConditionalDriftComponents",
    "SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityOfComponents",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorHandoff",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsOfGeneratorPiecesHandoff",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffScalar",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSigns",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces",
    "SALD.generalMovingTargetDiscreteConditionalFpSourceSignsHandoff",
    "SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff",
    "sald.general_moving_target_discrete.em_interpolation_fp"
  ]
  sourceGaps := [
    "appendix.tex:1379-1387 invokes the Fokker--Planck equation associated with the frozen interpolation but does not state the weak-test theorem or its regularity hypotheses.",
    "The generator-level theorem that turns the frozen EM interpolation into the weak time derivative of hat rho_s is still supplied as an analytic hypothesis.",
    "The source does not spell out the density, local integrability, or boundary/integration-by-parts assumptions required to interpret the divergence and Laplacian terms distributionally.",
    "The source passes immediately from this FP equation to the Laplacian split and KL derivative handoff."
  ]
  status := ProofStatus.obligation