AutoSamplingTheory.SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract

Data definition / provenance and workflow record

Meaning and type

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

def generalMovingTargetDiscreteEndpointConditionalCompatibilityContract :
    GeneralMovingTargetDiscreteEndpointConditionalCompatibilityContract

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

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

commonSpace : String (explicit)

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

For fixed k and s in [s_k,s_{k+1}], use the common probability space carrying X_k^eta and hat X_s. The joint law is represented as Measure.map (fun omega => (X_k^eta omega, hat X_s omega)) P.

jointLawRepresentation : String (explicit)

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

The conditional kernel for X_k^eta given hat X_s=x must be compatible with this joint law, not with an unrelated copy of the state space.

hatRhoMarginal : String (explicit)

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

The second marginal of the joint law is the named interpolation law hat rho_s=Law(hat X_s). SALD.generalMovingTargetDiscreteHatRhoMarginalOfJointMap compiles this Measure.map projection from explicit measurability and the named-law equality.

conditionalKernelCompatibility : String (explicit)

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

A future analytic backend must supply a kernel/disintegration predicate for the joint law and its second marginal before conditional expectations of the two frozen drift summands are formed.

compatibilityTransport : String (explicit)

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

SALD.generalMovingTargetDiscreteConditionalKernelCompatibilityOfJointMapMarginal compiles equality transport from the joint law's Measure.map Prod.snd marginal to the named hat rho_s marginal under a supplied congruence rule, while SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityOfJointMap packages the common lower use case directly as marginal equality plus transported kernel compatibility.

weakFpUse : String (explicit)

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

The weak Fokker-Planck statement recorded by SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract may consume the kernel only after this marginal compatibility is aligned with the same hat rho_s that appears in partial_s hat rho_s.

exclusions : List String (explicit)

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

Ordered data items

1. Do not treat this as a proof of existence of a regular conditional probability.
2. Do not prove conditional expectation linearity, measurability, integrability, density, absolute-continuity, or weak Fokker-Planck here.
3. Do not promote sald.general_moving_target_discrete.em_interpolation_fp or any theorem contract to formalized status.
4. Do not import or claim an SLT disintegration theorem.

dependencies : List String (explicit)

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

Ordered data items

1. SALD.generalMovingTargetDiscreteHatRhoMarginalOfJointMap
2. SALD.generalMovingTargetDiscreteConditionalKernelCompatibilityOfJointMapMarginal
3. SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityOfJointMap
4. AutoSamplingTheory.lawMapProdSnd
5. SALD.generalMovingTargetDiscreteEmJointEndpointMeasureMapOfNamedInterpolation
6. SALD.generalMovingTargetDiscreteEmJointEndpointMarginalLawsOfNamedInterpolation
7. SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract
8. SALD.generalMovingTargetDiscreteConditionalDriftContract
9. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract
10. 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:1368-1377 defines the conditional drift but does not spell out the disintegration theorem or marginal compatibility proof.
2. appendix.tex:1379-1387 invokes the associated Fokker-Planck equation immediately after the conditional drift definition.
3. The local Lean work proves only Measure.map marginal bookkeeping and predicate transport, not the analytic conditional-law backend.

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 generalMovingTargetDiscreteEndpointConditionalCompatibilityContract :
    GeneralMovingTargetDiscreteEndpointConditionalCompatibilityContract where
  sourceBlock := saldGeneralMovingTargetDiscreteDerivativeSource
  parentInterface := "sald.general_moving_target_discrete.em_interpolation_fp / appendix.tex:1358-1387"
  commonSpace := "For fixed k and s in [s_k,s_{k+1}], use the common probability space carrying X_k^eta and hat X_s. The joint law is represented as Measure.map (fun omega => (X_k^eta omega, hat X_s omega)) P."
  jointLawRepresentation := "The conditional kernel for X_k^eta given hat X_s=x must be compatible with this joint law, not with an unrelated copy of the state space."
  hatRhoMarginal := "The second marginal of the joint law is the named interpolation law hat rho_s=Law(hat X_s). SALD.generalMovingTargetDiscreteHatRhoMarginalOfJointMap compiles this Measure.map projection from explicit measurability and the named-law equality."
  conditionalKernelCompatibility := "A future analytic backend must supply a kernel/disintegration predicate for the joint law and its second marginal before conditional expectations of the two frozen drift summands are formed."
  compatibilityTransport := "SALD.generalMovingTargetDiscreteConditionalKernelCompatibilityOfJointMapMarginal compiles equality transport from the joint law's Measure.map Prod.snd marginal to the named hat rho_s marginal under a supplied congruence rule, while SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityOfJointMap packages the common lower use case directly as marginal equality plus transported kernel compatibility."
  weakFpUse := "The weak Fokker-Planck statement recorded by SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract may consume the kernel only after this marginal compatibility is aligned with the same hat rho_s that appears in partial_s hat rho_s."
  exclusions := [
    "Do not treat this as a proof of existence of a regular conditional probability.",
    "Do not prove conditional expectation linearity, measurability, integrability, density, absolute-continuity, or weak Fokker-Planck here.",
    "Do not promote sald.general_moving_target_discrete.em_interpolation_fp or any theorem contract to formalized status.",
    "Do not import or claim an SLT disintegration theorem."
  ]
  dependencies := [
    "SALD.generalMovingTargetDiscreteHatRhoMarginalOfJointMap",
    "SALD.generalMovingTargetDiscreteConditionalKernelCompatibilityOfJointMapMarginal",
    "SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityOfJointMap",
    "AutoSamplingTheory.lawMapProdSnd",
    "SALD.generalMovingTargetDiscreteEmJointEndpointMeasureMapOfNamedInterpolation",
    "SALD.generalMovingTargetDiscreteEmJointEndpointMarginalLawsOfNamedInterpolation",
    "SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract",
    "SALD.generalMovingTargetDiscreteConditionalDriftContract",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract",
    "sald.general_moving_target_discrete.em_interpolation_fp"
  ]
  sourceGaps := [
    "appendix.tex:1368-1377 defines the conditional drift but does not spell out the disintegration theorem or marginal compatibility proof.",
    "appendix.tex:1379-1387 invokes the associated Fokker-Planck equation immediately after the conditional drift definition.",
    "The local Lean work proves only Measure.map marginal bookkeeping and predicate transport, not the analytic conditional-law backend."
  ]
  status := ProofStatus.obligation